PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_specifications_proved

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

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Ring_topology.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_specifications.
From Padec Require Import Dijkstra_complexity.
From Padec Require Import Dijkstra_complexity_degenerated.
From Padec Require Import Steps.

Open Scope nat_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)

Specifications Proved

/contains:/ Proof that the algorithm is self-stabilizing wrt token ring circulation

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

Closure: The result is direct from the result shown in

Dijkstra_common, in particular, Lemmas token_obtained and two_tokens_move.

Convergence: The result is direct from complexity.
Specification: As we have (Always Leg_State), (Always is_exec) and (Always Assume_RO), we have to prove that for every node, for every execution beginning in Assume_RO and Leg_State, it eventually reaches a configuration where the node holds the token. This proof is done by induction on the Ring traversal (using Succ), starting from the token holder. The step of induction relies on Lemma token_passes_to_Succ: after a step, a node that move transmits its token to its successor.

Section Dijkstra_spec_proved.

  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 HNk: N <= k.

Closure

i.e. Step preserves legitimate configurations

Lemma Dijkstra_closure_small:
forall g g', Assume g -> Leg_state g -> Step g' g -> Leg_state g'.

Closure Lemma

Lemma Dijkstra_closure: closure Dijkstra_RO_assumption
unfair_daemon Leg_state.

Convergence: eventually a legitimate configuration is

reached Obtained from complexity

  Lemma Dijkstra_convergence:
    convergence Dijkstra_RO_assumption unfair_daemon Leg_state.
  Section Convergence_alternative_proof.

  End Convergence_alternative_proof.

Specification

As we have (Always Leg_State), (Always is_exec) and (Always Assume_RO), we have to prove that for every node, for every execution beginning in Assume_RO and Leg_State, it eventually reaches a configuration where the node holds the token. This proof is done by induction on the Ring traversal (using Succ), starting from the token holder. The step of induction relies on Lemma token_passes_to_Succ: after a step, a node that move transmits its token to its successor.

  Lemma token_passes_to_Succ:
    forall g g', Assume g -> Leg_state g -> Step g' g ->
                 forall n, Token g n -> Token g' (Succ n).

  Lemma Dijkstra_spec_ok:
    forall (e: Exec) (assume: Assume (s_hd e))
           (ise: is_exec e) (legit: Leg_state (s_hd e)),
    forall n, Always (Eventually (fun e => Token (s_hd e) n)) e.

Functional Specification of the Algorithm.

  Theorem Dijkstra_self_stab_prop:
    self_stabilization Dijkstra_RO_assumption unfair_daemon
                       Token_Circulation_Spec.

End Dijkstra_spec_proved.

Unset Implicit Arguments.
Close Scope nat_scope.