PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_common

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import Decidable.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import All_In.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Ring_topology.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Self_Stabilization.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

Proof of self-stabilization and specification
Proof of a complexity bound in steps
Proof that this complexity bound is exact (by building a worst case prefix of execution)

Common Results

/contains:/ Common Definitions and Results about Dijkstra Token Ring Circulation

/assumes:/ Parameter k>1; the network is a unidirectional rooted ring

Definition of the network assumption: it checks that the read-only variable of the state of each process exactly represents the ring topology defined by the network (channels coincide with Pred and Boolean values with the unique root).
Predicate Token (on a configuration and a node) holds when the node holds a token. The predicate is proven compatible and decidable. It holds at a node iff the node is enabled. We also prove that for every configuration, there exists at least a node that holds a token (i.e., there exists at least one token in the ring). It follows directly that in any configuration, the algorithm can perform a step of computation. Hence, no configuration is terminal.
Legtimate Configurations: configurations with a unique token. As there always exists a token in the network, the legitimate configuration predicate, only checks token uniqueness. This predicate is compatible and weakly decidable. We characterize legitimate configurations (Lemma ls_charac): a configuration g is legitimate iff
- either the root is the unique token holder and g contains only one value; or
- every node in the slice from the root to the predecessor of the token holder has the same value and another value covers all remaining nodes.
Degenerated rings (1 or 2 nodes): every configuration is legitimate.

The file also contains many utilitaries and intermediary results to simplify the proofs. The most important ones among them are:

When a node obtains a token during a step (meaning it did not own one before the step), this means that its predecessor moves during the step (Lemma token_obtained)
When a node moves, and then still holds a token, its predecessor has also moved in the same step (Lemma two_tokens_move).

Common Definitions and Results about Dijkstra Token Ring Circulation

Section Common_defs.

  Context {Chans: Channels}
          {Net: Network}
          {RURN: Rooted_Unidirectional_Ring_Network Net}
          {DP: Dijkstra_parameters}.

  Notation Algo := Dijkstra_algo.
  Notation Root := (RURN_root (Net := Net)).
  Notation Ring := (URN_topo (Net := Net)).
  Notation Env := (Env (Net := Net) (Algo := Dijkstra_algo)).

  Notation N := (Ring_size Root).
  Hypothesis HNk: N <= k.

Assumption for the Dijkstra algorithm

Given by Ring_Network_assumption

Checks that the read-only variable (channel, bool) exactly represents the ring topology defined by RURN; channel coincides with Pred and bool with the unique root.

  Existing Instance Dijkstra_Stable.
#[refine] Instance Dijkstra_RO_assumption: Stable_Assumption (Algo := Dijkstra_algo)
                                                     (Net := Net)
    := {|
      Assume_RO :=
                (fun ro: Node -> Dijkstra_ROState =>
                   Ring_Network_assumption RURN
                                           (fun n: Node => root (ro n))
                                           (fun n: Node => predc (ro n))
                )|}.

A simplification lemma: the RUN/run function can be replaced by simple_run and the direct use of information from the topology using Pred.

  Lemma RUN_simpl:
    forall g n, Proper pequiv g -> Assume_RO (ROEnv_part g) ->
                RUN (Algo:=Algo) g n == simple_run (g n) (g (Pred n)).

Token

This predicate expresses the fact that the node owns a token:

either the node is the Root and its value is the same as its predecessor
or else its value differs from the one of its predecessor

Note that this exactly coincides with the fact that the node is enabled (see Lemma enabled_Token above).

  Section Token.

    Definition Token (g: Env) (n: Node): Prop :=
      (Root == n /\ (v (g n) = v (g (Pred n))))
      \/
      (~Root == n /\ (v (g n) <> v (g (Pred n)))).

    Lemma Token_compat: Proper fequiv Token.

Deciding whether a node holds a token or not is decidable!

Lemma Token_dec: forall g n, { Token g n } + { ~Token g n }.

A node holds a token iff it is enabled in the algorithm

    Lemma enabled_Token:
      N > 1 -> forall (g: Env),
          Proper fequiv g -> Assume g ->
          forall (n: Node), enabled g n <-> Token g n.

In any configuration, there exists at least one token

Lemma Token_exists:
forall g, Proper fequiv g -> exists n , Token g n.

It follows directly that in any configuration, the algorithm can perform a step of computation.

    Lemma Step_exists:
      N > 1 -> forall (g: Env), Assume g -> Proper fequiv g ->
                                exists y , Step y g.

    Lemma has_moved_true_Token:
      N > 1 -> forall g (ass: Assume g) g' (step: Step g' g) n,
          has_moved_b g' g n = true -> Token g n.

Hence, no configuration is terminal

    Lemma no_terminal:
      N > 1 -> forall (g: Env), Proper fequiv g -> Assume g ->
                                ~terminal g.

Constant Slice

As long as there is no token between the Root and a given node n, the values of v between Root and n are all equal (to the value of, e.g., Root).

    Lemma constant_slice:
      forall (g: Env),
        Proper fequiv g ->
        forall n, ~n == Root ->
                  (forall n', Between (Succ Root) n' n -> ~ Token g n') ->
                  v (g n) = v (g Root).

  End Token.

Enbled:

We provide small Lemmas to simplify the use of run_algorithm about enabled nodes.

  Section Enabled.

    Variable (g: Env) (pg: Proper fequiv g) (Assume_g: Assume g).
    Hypothesis HN1: N > 1.

    Lemma enabled_Root:
      forall n, Root == n ->
                (enabled g n <-> v (g n) = v (g (Pred n))).

    Lemma enabled_non_Root:
      forall n, ~Root == n ->
                (enabled g n <-> v (g n) <> v (g (Pred n))).

  End Enabled.

Move:

We provide Lemmas to simplify the use of run_algorithm about moving nodes.

  Section Move.

    Variable (g: Env) (Assume_g: Assume g) (g': Env) (step: Step g' g).

    Lemma has_moved_v_change:
      forall n, has_moved_b g' g n = true <-> v (g n) <> v (g' n).

    Lemma has_moved_v_Root:
      forall n, Root == n ->
                has_moved_b g' g n = true ->
                v (g' n) = (v (g (Pred n)) + 1) mod k.

    Lemma has_moved_v_Root':
      N > 1 -> forall n, Root == n ->
                         has_moved_b g' g n = true ->
                         v (g (Pred n)) <> v (g' n).

    Lemma has_moved_v_non_Root:
      forall n, ~ Root == n ->
                has_moved_b g' g n = true -> v (g' n) = v (g (Pred n)).

When a node moves, and then still holds a token, its predecessor has also moved in the same step.

    Lemma two_tokens_move:
      N > 1 -> forall n, has_moved_b g' g n = true ->
                         Token g' n ->
                         has_moved_b g' g (Pred n) = true.

When a node obtains a token during a step (meaning it did not own one before the step), this means that its predecessor moves during the step.

    Lemma token_obtained:
      N > 1 -> forall n, ~Token g n -> Token g' n ->
                         has_moved_b g' g (Pred n) = true.

  End Move.

Legitimate Configurations

Configurations with a unique token (see Leg_State).

As there always exists a token in the network (see Lemma Token_exists), assuming token uniqueness is enough.

  Section Legitimate_Configuration.

    Definition Leg_state (g: Env): Prop :=
      forall n1 n2, Token g n1 -> Token g n2 -> n1 == n2.

    Instance Leg_state_compat: Proper (fequiv ==> iff) Leg_state.

Deciding whether a configuration is legitimate or not is weakly decidable

Lemma Leg_state_dec:
forall g, {Proper fequiv g -> Leg_state g } + {~Leg_state g }.

Charaterization of Legitimate

    Lemma about_ls1:
      forall g (pg: Proper pequiv g),
        Leg_state g ->
        exists n , Token g n /\
                  (forall n', Between Root n' (Pred n) ->
                              v (g Root) = v (g n')) /\
                  forall n', Between n n' (Pred Root) ->
                             v (g (Pred Root)) = v (g n').

    Lemma about_ls2:
      forall g (pg: Proper pequiv g),
        (exists n , Token g n /\
                   (forall n', Between Root n' (Pred n) ->
                               v (g Root) = v (g n')) /\
                   forall n', Between n n' (Pred Root) ->
                              v (g (Pred Root)) = v (g n'))
        -> Leg_state g.

    Lemma ls_charac:
      forall g (pg: Proper pequiv g),
        Leg_state g <->
        (exists n , Token g n /\
                   (forall n', Between Root n' (Pred n) ->
                               v (g Root) = v (g n')) /\
                   forall n', Between n n' (Pred Root) ->
                              v (g (Pred Root)) = v (g n')).

In a legitimate configuration, the node preceding the token holder has the same value as the root. (This is due to the convex_part Lemma and to the fact that the token holder is unique.)

    Lemma legit_convex:
      forall g, Proper fequiv g -> Leg_state g ->
                forall n, Token g n -> v (g (Pred n)) = v (g Root).

  End Legitimate_Configuration.

  Section Degenerated_Rings.

Particular case: the ring contains a unique node

The root has a token. Every configuration is legitimate, hence the stabilization time is 0

    Lemma Single_Node_has_token:
      N = 1 -> forall g n, Proper pequiv g -> Token g n.

    Lemma Single_Node_Legitimate:
      N = 1 -> forall g, Proper pequiv g -> Leg_state g.

Particular case: the ring contains only two nodes

Every configuration is legitimate, hence the stabilization time is 0

Lemma Two_Nodes_Legitimate:
N = 2 -> forall g, Proper pequiv g -> Leg_state g.

The ring is not degenerated

    Lemma Non_degen2:
      N >= 2 -> forall x, ~ Succ x == x.

    Lemma Non_degen3:
      N >= 3 -> forall x, ~ Succ (Succ x) == x.

  End Degenerated_Rings.

  Section Costs.

    Definition Dijkstra_exact_bound (N: nat): nat :=
      3 * (N * (N - 1) / 2) - N - 1.

  End Costs.

End Common_defs.

Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature_scope.