PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_common

A Framework for Certified Self-Stabilization
PADEC Coq Library


Global Imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.
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

Common Results

/contains:/ Common Definitions and Results about Dijkstra Token Ring Circulation
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring
The file also contains many utilitaries and intermediary results to simplify the proofs. The most important ones among them are:

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)).

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.

  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:
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:
      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:
      forall (g: Env), Assume g -> Proper fequiv g -> exists y, Step y g.

    Lemma has_moved_true_Token:
      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:
      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).

    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':
      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:
      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:
      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

Every configuration is legitimate, hence the stabilization time is 0
    Lemma Single_Node_Legitimate:
      Ring_size Root = 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:
      Ring_size Root = 2 -> forall g, Proper pequiv g -> Leg_state g.

The ring is not degenerated

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

    Lemma Non_degen3:
      Ring_size Root >= 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.