Coq Library
Tools

#### Global Imports

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

#### Local Imports

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.
• Convergece: 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)).

Hypothesis HNk: Ring_size Root <= 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'.

## Convergence: eventually a legitimate configuration is

reached Obtained 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.

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.