PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_convergence_alt

A Framework for Certified SelfStabilization
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.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import Count.
From Padec Require Import All_In.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import P_Q_Termination.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import Ring_topology.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_Z.
From Padec Require Import Dijkstra_sum_dist.

Open Scope nat_scope.
Set Implicit Arguments.

Convergence

i.e. eventually a legitimate configuration is reached i.e. eventually there exists a unique token in the ring.

Section Dijkstra_Convergence.

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

  Existing Instance Dijkstra_RO_assumption.

  Notation N := (Ring_size Root).
  Hypothesis HN1: N > 1.

This part of the proof using Type using Type using Type using Type using Type using Type using Type using Type requires the additional property that the number of nodes in the ring is smaller than or equal to k.

  Hypothesis (HNk: N <= k).

  Notation Mset := (MultisetNat.MSetCore.Multiset).
  Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
  Notation eqM := MultisetNat.MSetCore.meq.

Convergence proof is done within nonlegitimate configurations and is split into convergence to legitimate configurations of steps where the Root moves convergence to legitimate configurations of steps where the Root does not execute

In the proof, we only consider configurations which are not legitimate and steps between those nonlegitimate configurations.

Notation Safe := (fun g => Assume g /\ ~Leg_state g).

safeEnv := {g | Assume g /\ ~ Leg_state g}

  Notation safeEnv := (sig Safe).
  Notation getEnv := (fun sg: safeEnv => proj1_sig sg).
  Notation getSafe := (fun sg: safeEnv => proj2_sig sg).

Step where the root moves: Trans_with_root is a relation between safeEnv

  Definition QTrans_with_root (g' g: safeEnv) :=
    v (getEnv g' Root) <> v (getEnv g Root).

  Definition Trans_with_root := safeQStep QTrans_with_root.

Step where the root does not move.

  Definition QTrans_without_root (g' g: safeEnv) :=
    v (getEnv g' Root) = v (getEnv g Root).

  Definition Trans_without_root := safeQStep QTrans_without_root.

Convergence When Root Moves: Z potential decreases at

each step the root moves. Potential Z on safeEnv.

  Definition Z_pot :=
    (fun sg: safeEnv => Z (getEnv sg)).

  Lemma Z_pot_decreases:
    forall sg sg',
      Trans_with_root sg' sg -> Z_pot sg' < Z_pot sg.

Convergence when Root does not move

For this part of the proof of convergence, we use the criteria given by the Deshowitz-Manna order expressed in the library P_Q_Termination.

Section Root_does_not_move.

Potential when Root does not move

for a node: equals 0 when the node is disabled, is equal to the distance from the node to the root otherwise.

    Definition pot_without_Root (g: Env) (n: Node) :=
      if Token_dec g n then (Dist n Root) else 0.

    Definition Pot_without_Root :=
      (@Pot _ Net Dijkstra_algo Safe
            (fun sg: safeEnv => pot_without_Root (getEnv sg))).

    Instance pot_without_Root_compat:
      Proper fequiv pot_without_Root.

Common Result to Both Criteria:

When a node n moves and still holds a token afterwards, this means that there exists a node n' such that n' holds a token in g has lost it in g' and n' is closer to the Root than n (using Succ) This is proven using induction on the Ring traversal (with Succ). The node n' cannot be the Root (since it moves); in either case, the property relies on 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 moves and still holds the token afterwards, this means that it predecessor also moves). As the root does not move in this context, we have the property.

    Lemma both_criteria:
      forall g g',
        Assume g -> Step g' g -> v (g' Root) = v (g Root) ->
        forall n, has_moved_b g' g n = true -> Token g' n
                  ->
                  exists n', Token g n' /\ ~Token g' n' /\
                             Dist n' Root > Dist n Root.

Local Criteria:

When a node n, which is not the root, does not hold a token in g but obtains one in g', this means that there exists a node n' such that n' holds a token in g has lost it in g' and n' is closer to the Root than n (using Succ)

Note that the predecessor of n moves: if it loses its token in g', then n' is (Pred n) otherwise, we apply both_criteria to (Pred n) and obtains the result.

    Lemma local_criterion_without_Root:
      forall (g g': Env),
        Assume g -> Step g' g -> v (g' Root) = v (g Root) ->
        forall n, ~ Root == n -> ~ Token g n -> Token g' n ->
                  exists n', Token g n' /\ ~Token g' n' /\
                             Dist n' Root > Dist n Root.

    Lemma local_criterion_without_Root':
      forall g g': safeEnv,
        safeStep g' g /\ v (getEnv g' Root) = v (getEnv g Root) ->
        forall n,
          pot_without_Root (getEnv g') n > pot_without_Root (getEnv g) n ->
          exists n',
            pot_without_Root (getEnv g) n' <>
            pot_without_Root (getEnv g') n' /\
            pot_without_Root (getEnv g) n' > pot_without_Root (getEnv g') n.

Global Criteria

There exists a node (different from the root) which loses a token from g to g'.

The step from g to g' provides a node which moves (hence it is not the root and holds a token). If this node loses its token in g', we are done, otherwise, we apply both_criteria to n and obtains the result.

    Lemma global_criterion_without_Root:
      forall (g g': Env),
        Assume g -> Step g' g -> v (g' Root) = v (g Root) ->
        exists n , ~ Root == n /\ Token g n /\ ~Token g' n.
    Lemma global_criterion_without_Root':
      forall (g g' : safeEnv),
        safeStep g' g /\ v (getEnv g' Root) = v (getEnv g Root) ->
        exists n , pot_without_Root (getEnv g') n <>
                  pot_without_Root (getEnv g) n.

We obtain the relation that corresponds to steps where the root does not move is wellfounded.

    Lemma Trans_without_root_wf:
      well_founded (safeQStep QTrans_without_root).

  End Root_does_not_move.

Steps with and without Root moves are combined using a lexicographic ordering

Again, to show that potential in g' is less than or equal to potential in g, we rewrite potentials as minimum (using pot_with_Root_min) and applies Lemma is_minimum_le that says that if M1 (resp. M2) is minimum of some set A1 (resp. A2) and if for every value in A1, there exists a smaller or equal value in A2, then M2 is smaller than or equal to M1.

We first restrict to values smaller than k in M1 (i.e. values x such that (convex g ((v (g Root) + x) mod k)) holds). If x is 0, we prove that (convex g' (v (g Root))): since the value is copied from the predecessor when a node moves, this cannot break the convex property for (v (g Root)).

If x <> 0 then, no node in the ring holds value ((v (g Root) + x) mod k) = ((v (g' Root) + x) mod k). As no new value appears in the step, (convex g ((v (g Root) + x) mod k)) holds.

  Lemma values_do_not_appear_non_Root:
    forall (g g': Env),
      Assume g -> Step g' g ->
      v (g' Root) = v (g Root) -> Z g' <= Z g.

Step between non legitimate configurations is a wellfounded

relation This is proven splitting the relation into steps where the root moves steps where the root does not move. Those two set of steps are composed using Lexicographic order: the Lexicographic order propery is given Lemma values_do_not_appear_non_Root; the fact that steps where the root moves are wellfounded is given directly by the corresponding potential decreasing; the fact that steps where the root does not move are wellfounded is given directly by applying the DershowitzManna criteria given by local and global criteria.

  Lemma Wf_safe:
    well_founded (fun a b: safeEnv => Step (getEnv a) (getEnv b)).

  Lemma Acc_non_leg_step:
    forall (g: Env), Proper fequiv g -> Assume g ->
                     Acc (fun a b => ~ Leg_state b /\ Step a b) g.

Convergence Theorem (Alternative Proof)

Theorem Dijkstra_convergence_alt:
convergence Dijkstra_RO_assumption unfair_daemon Leg_state.
End Dijkstra_Convergence.

Unset Implicit Arguments.
Close Scope nat_scope.