PADEC - Coq Library

Library Padec.Model.Self_Stabilization

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

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

Local Imports

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.
From Padec Require Import Fairness.

Set Implicit Arguments.
Open Scope signature_scope.

Specifications for self-stabilizing algorithms and

silent self-stabilizing algorithms

Section Self_Stabilization.

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

Assumption made on read-only variables of the algorithm

Hypothesis assume: Stable_Assumption.

In the sequel, we use:

Daemon_fairness: Exec -> Prop = specification of the Daemon Fairness

(e.g. unfair daemon, weakly fair daemon, synchronous daemon ...)

SPEC: Exec -> Prop = specification of the algorithm
LEG_STATE: Env -> Prop = legitimate states for stelf-stabilization

Self-stabilization: Closure w.r.t. legitimate states Definition closure (LEG_STATE: Env -> Prop): Prop := forall (env env': Env), Assume env -> LEG_STATE env -> Step env' env -> LEG_STATE env'.

  Definition closure (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop): Prop :=
    forall (e: Exec),
      Assume (s_hd e) -> is_exec e -> Daemon_fairness e ->
      LEG_STATE (s_hd e) -> Always (fun e => LEG_STATE (s_hd e)) e.

Self-stabilization: Convergence to legitimate states

  Definition convergence (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop): Prop :=
    forall (e: Exec),
      Assume (s_hd e) -> is_exec e -> Daemon_fairness e ->
      Eventually (fun suf: Exec => LEG_STATE (s_hd suf)) e.

Self-stabilization: Meets specification when initialized in legitimate states

  Definition spec_ok (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop) (SPEC: Exec -> Prop): Prop :=
    forall (e: Exec),
      Assume (s_hd e) -> is_exec e -> Daemon_fairness e ->
      LEG_STATE (s_hd e) -> SPEC e.

Self-stabilization: full property

  Definition self_stab (Daemon_fairness: Exec -> Prop)
             (LEG_STATE: Env -> Prop) (SPEC: Exec -> Prop): Prop :=
    closure Daemon_fairness LEG_STATE /\ convergence Daemon_fairness LEG_STATE
    /\ spec_ok Daemon_fairness LEG_STATE SPEC.

  Definition self_stabilization (Daemon_fairness: Exec -> Prop)
             (SPEC: Exec -> Prop): Prop :=
    exists (LEG_STATE: Env -> Prop), self_stab Daemon_fairness LEG_STATE SPEC.

  Lemma self_stabilization_alt:
    forall Daemon_fairness SPEC LEG_STATE,
      self_stab Daemon_fairness LEG_STATE SPEC <->
      forall e, Assume (s_hd e) -> is_exec e -> Daemon_fairness e ->
                ( LEG_STATE (s_hd e) ->
                  Always (fun e => LEG_STATE (s_hd e)) e )

                /\
                Eventually (fun suf: Exec => LEG_STATE (s_hd suf)) e

                /\
                ( LEG_STATE (s_hd e) -> SPEC e ) .

  Section Silence.

Self-stabilization for Silent Algorithm

Silent Algorithm: an algorithm for which any execution is finite is equivalent to: an algorithm converges to terminal configuration

    Definition silence (Daemon_fairness: Exec -> Prop): Prop :=
      forall (e: Exec), Assume (s_hd e) -> is_exec e ->
                        Daemon_fairness e -> finite_exec e.

    Lemma convergence_silence (Daemon_fairness: Exec -> Prop):
      convergence Daemon_fairness terminal <-> silence Daemon_fairness.

    Lemma self_stabilization_for_silence (Daemon_fairness: Exec -> Prop)
          (SPEC: Exec -> Prop):
      silence Daemon_fairness ->
      ( self_stabilization Daemon_fairness SPEC <->
        spec_ok Daemon_fairness (fun g => terminal g) SPEC ).

    Lemma silence_unfair_weakly_fair:
      silence unfair_daemon ->
      forall e, Assume (s_hd e) -> is_exec e ->
                unfair_daemon e -> weakly_fair e.

Partial Correctness

Any terminal configuration satisfies the specification.

    Definition P_correctness (SPEC_env: Env -> Prop): Prop :=
      forall (g: Env), Assume g -> terminal g -> SPEC_env g.

    Definition only_one (SPEC_env: Env -> Prop) (ex: Exec): Prop :=
      match ex with
      | s_one g => SPEC_env g
      | s_cons _ _ => False
      end.

Self-Stabilization for Silent Algorithm

    Theorem silent_self_stabilization
            (Daemon_fairness: Exec -> Prop) (SPEC_env: Env -> Prop):
      silence Daemon_fairness -> P_correctness SPEC_env ->
      self_stabilization Daemon_fairness (only_one SPEC_env).

    Lemma silent_terminal_SPEC
          (Daemon_fairness: Exec -> Prop) (SPEC_env: Env -> Prop):
      (forall g, Assume g -> terminal g -> Daemon_fairness (s_one g))
      -> silence Daemon_fairness ->
      self_stabilization Daemon_fairness (only_one SPEC_env) ->
      P_correctness SPEC_env.

  End Silence.

Proving convergence to a set of legitimate configurations can be done

using Acc and well-foundedness. Namely, if from any configuration with assumption met the transitive closure of Step started from a non legitimate configuration is Acc (well-founded) then the execution starting from this configuration converges to Leg_State.

Note that this property is made to be used with the weakest daemon fairness assumption, i.e. the unfair daemon (True).

  Section Convergence.

    Variable (Leg_State: Env -> Prop)
             (Leg_State_compat: Proper fequiv Leg_State)
             (Leg_State_dec:
                forall g, Proper pequiv g -> Assume g ->
                          {Leg_State g } + {~Leg_State g }).

    Hypothesis (term_is_leg:
                  forall g, Proper pequiv g -> Assume g ->
                            terminal g -> Leg_State g).

    Lemma Convergence_to_Legitimate':
      forall (g: Env),
        Acc (fun g' g => ~Leg_State g /\ Step g' g) g ->
        forall (e: Exec) (ise: is_exec e) (assume: Assume (s_hd e)),
          s_hd e = g -> Eventually (fun suf: Exec => Leg_State (s_hd suf)) e.

    Lemma Convergence_to_Legitimate:
      (forall (g: Env) (pg: Proper pequiv g) (assume: Assume g),
          Acc (fun g' g => ~Leg_State g /\ Step g' g) g ) ->
      convergence unfair_daemon Leg_State.

Note on Acc:

  Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
        Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x

  Acc ~Leg_State/\Step g0: given by
    forall g1, ~Leg_State g0 /\ Step g1 g0 (g0->g1) -> Acc g1
    ... becomes true iff no configuration g satisfies: 
             ~Leg_State gn /\ Step g gn
        namely when gn is Leg_State or
                    gn is a terminal configuration 
                    (and hence Leg_State, due to [term_is_leg]

  Namely, any execution from g0 reaches Leg_State.

End Convergence.

Termination

Any configuration that is reachable from an initial configuration g satisfying the assumptions can be reached within a finite number of steps

(i.e., using Step a finite number of times)

Note that this property is made to be used with the weakest daemon fairness assumption, i.e. the unfair daemon (True).

  Definition termination: Prop :=
    forall (g: Env), Assume g -> Proper pequiv g -> Acc Step g.

  Lemma termination_is_silence: termination -> convergence unfair_daemon terminal.

End Self_Stabilization.

Close Scope signature_scope.
Unset Implicit Arguments.