PADEC - Coq Library

Library Padec.Model.Fairness

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.

Local Imports

From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Exec.

Open Scope signature_scope.
Set Implicit Arguments.

Section Fairness.

Context {Chans: Channels}
{Net: Network} {Algo: Algorithm}.

Unfair Daemon: the most permissive daemon

Definition unfair_daemon (e: Exec): Prop := True.

Weakly Fair Execution

Section Weakly_Fair.

“Weakly fair” means that there is no infinite suffix of execution in which a process p is continuously enabled without ever being selected by the daemon.

In a weakly fair execution, processes are fairly activated, i.e., if a process is continuously enabled, then it eventually executes one of its enabled actions.

Definition

    Definition weakly_fair (e: Exec): Prop :=
      forall (n: Node),
        Always (fun e' => EN n e' -> Eventually (AN n) e') e.

    Lemma weakly_fair_inv:
      forall g e, weakly_fair (s_cons g e) -> weakly_fair e.

    Lemma weakly_fair_Always:
      forall e, weakly_fair e -> Always weakly_fair e.

Finite Executions are weakly fair

    Lemma WF_finite_exec':
      forall (e: Exec), is_exec e -> finite_exec e ->
                        forall (n: Node),
                          Always (Eventually (EN n)) e -> False.

    Lemma WF_finite_exec:
      forall (e: Exec), is_exec e -> finite_exec e ->
                        forall (n: Node), EN n e -> Eventually (AN n) e.

    Lemma WF_finite_exec'':
      forall (e: Exec), is_exec e -> finite_exec e ->
                        forall (n: Node),
                          ~Always (fun e' : Exec => EN n e' /\ ~ AN n e') e.

    Lemma weakly_fair_finite_exec:
      forall (e: Exec), is_exec e -> finite_exec e -> weakly_fair e.

    Lemma en_E_A:
      forall (e: Exec), is_exec e ->
                        forall (n: Node), EN n e -> WUntil (EN n) (AN n) e.

Necessary conditions for weakly fair

    Lemma WF_NC1:
      forall (e: Exec), weakly_fair e ->
                        forall (n: Node), Always (Eventually (EN n)) e ->
                                          Always (Eventually (AN n)) e.

Note that the converse cannot be proven: It would require:

EN n e -> Eventually (AN n) e \/ Always (EN n) e

namely, decide wether becomes AN forever or remains EN forever it seems like halting problem...

Actually, we have:

EN n e -> (EN n) UNTIL (AN n) e

but no more...

    Lemma WF_NC2:
      forall (e: Exec), weakly_fair e ->
                        forall (n: Node),
                          ~Eventually (Always (fun e' =>
                                                 EN n e' /\ ~ AN n e')) e.

We do not succeed in proving the converse. It would require:

~Eventually (Always (fun e' : Exec => EN n e' /\ ~ AN n e')) e
- > EN n e -> Eventually (AN n) e

Compatibility

Global Instance weakly_fair_compat: Proper fequiv weakly_fair.

End Weakly_Fair.

Suffix of Execution

Section Suffix.

Properties

    Lemma suffix_is_exec:
      forall (e: Exec), is_exec e ->
                        forall (e_suf: Exec),
                          is_suffix e e_suf -> is_exec e_suf.

    Lemma suffix_weakly_fair:
      forall (e: Exec), weakly_fair e ->
                        forall (e_suf: Exec),
                          is_suffix e e_suf -> weakly_fair e_suf.
    Lemma suffix_finite_exec:
      forall (e e_suf: Exec) (is_suf: is_suffix e e_suf),
        finite_exec e <-> finite_exec e_suf.

  End Suffix.

  Section Strongly_Fair.

    Definition strongly_fair (e: Exec): Prop :=
      forall (n: Node), Always (Eventually (EN n)) e ->
                        Always (Eventually (ACT n)) e.

  End Strongly_Fair.

  Section Weakly_Fair_Unfair.

    Lemma weakly_fair_unfair:
      forall e, weakly_fair e -> unfair_daemon e.

  End Weakly_Fair_Unfair.

End Fairness.

Close Scope signature_scope.
Unset Implicit Arguments.