A Framework for Certified Self-Stabilization
PADEC Coq Library

• March 2017

Global Imports

Local Imports

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)

Potential sum_dist

/contains:/ Definitions and results about sum_dist /assumes:/ Parameter k>1; the network is a unidirectional rooted ring;

• sum_dist: sum of distances to the root of every token holder
• sum_dist increases by at most N-1 when the root moves and decreases otherwise.
• sum_dist is naturally upper bounded by the sum of the distances of every node to the root.

The ring contains at least 3 nodes

Definitions for the sum of distances to the root of every

token holder. We define sum_dist which is the complete sum and then sd which is a partial sum computed on a given slice of the ring. accumulation function

sum_dist: sum of distances to the root of every token holder.

sd: partial sum computed on a given slice of the ring

Tools about sd

to reduce or split the slice on which sd is computed

decomposition for sd that exihibits the value of a given node in the slice.

Relation between sd and sum_dist

Tools for sd (at most) decreasing

When no node obtains a token in some slice, then the sum of the slice does not increase (proof by induction on the list of the nodes in the slice)

When no node obtains a token, but at least one loses a token, sd decreases

In a slice, where no node obtains a token but the last one, if some node inbetween actually loses a token, then sd decrease.

LO

We build the list of non-root nodes that obtain a token during a step from g to g'. Note that this list is built traversing the node from (Succ Root) to (Pred Root) in the reverse order.

token_obtained

We say that a node obtains a token during a step from g to g' when it does not hold a token in g, but holds one in g'.

LO

Note that for every node x in LO, x itself does not move, its predecessor Pred x moves, and its successor Succ x either does not move or else loses its token (since it copies x's value and this value remains constant in the step).

Tools for LO decomposition

We first define tools for LO decomposition. We consider the case when LO contains at least one element and then the case of at least two (consecutive) elements.

If LO contains at least an element:

LO can be decomposed as l ++ x ++ l' where x is a node and l and l' are lists. Then, we have:

• token_obtained x
• Between (Succ Root) x (Pred Root)
• ~ x == Root
• x == Succ Root -> l' == nil
• x == Pred Root -> l == nil

Those results come directly from the definitions and the assumption N>=3.

As there is no duplicate in a traversal list of node, if LO is split into 3 parts (l, x, l') then l and l' are the results of the filtering operation on the list before x, resp. after x.

Particular case of the considered element being Succ Root to prove this result, we directly apply LO_decomp_decomp

Particular case of the considered element being Pred Root to prove this result, we directly apply LO_decomp_decomp

If LO contains at least two elements:

LO can be decomposed as l ++ x :: y :: l' where x and y are nodes and l and l' are lists.

• ~ x == y (since a traversal contains no replicate)
• ~ x == Succ y (two consecutive nodes in the ring cannot be in the list, since the predecessor of a node in LO actually moves in the step (hence has a token in g), see Lemma token_obtained.)
• ~ x == Succ Root
• ~ y == Pred Root
• Between (Succ Root) y (Pred x)
• Between (Succ y) x (Pred Root)

The 4 last results come directly from the definitions and the assumption N>=3.

Again, as there is no duplicate in a traversal list of nodes, if LO is split into 4 parts (l, x, y, l') then l and l' are the results of the filtering operation on the list before x, resp. after y, and the filtering operation on the list after x and before y returns an empty list.

Order between the two consecutive elements of LO to prove this result, we directly apply LO_decomp_decomp

Order between the two consecutive elements of LO to prove this result, we directly apply LO_decomp_decomp

3) Remark: in any slice of the ring between two

consecutive elements of LO (resp in the first slice, before flo) (resp in the last slice after llo), no node obtains a token, hence sd computed on this slice does not increase.

Results for Remark 3

Lemma witness

The proof is mainly an induction on LO. It mainly relies the idea that for every node n in LO (and even if LO is empty) we can find a witness node which loses a token and is farther than n from the root. Lemma witness: in a slice m - n of nodes, if n moves, then either m moves and holds a token in g' or there exits a node l between m and n which loses its token. Lemma witness is proven by induction on m using an induction schema of Between. For the base case, (the property has to be proven for n), n moves. Hence, either it loses its token or keeps it; both cases prove the base case. At each induction step, either we already found the witness node or the current node moves and keeps the token. By two_tokens_moves, we obtain that the predecessor of the current node also moves, hence as in the base case, both cases are proven whatever be the fact that the node keeps its token or not.

Case: LO is nil.

We already have "<=" using the remark above. During the step,

• If the root moves, we are done.
• Otherwise, as we consider a step, a non-node n moves: we apply Lemma witness to the slice Succ Root - n: as the root does not move, we exhibit a witness node that makes sum_dist decrease.

The rest of the proof is done by an induction on LO. It

relies on the idea that for every node n in LO we can find a witness node which loses a token and is farther than n from the root. For; the first slice of nodes, Succ flo - Pred Root we have <=.

For every slice of nodes Succ y - x, since Pred x moves, and Succ y either does not move or else loses its token, Lemma witness applied on Succ y - Pred x exhibit a witness node which is farther than x the root and makes sd decrease on the slice.

For the last slice Succ Root - llo, if Succ Root

moves and still holds a token, then the root moves. This is the case with no witness when sd increases by at most N - 1 = Dist (Succ Root) Root in the slice. Otherwise, Lemma witness applies to Succ Root - Pred llo and exhibits a witness node which is farther than llo from the root and makes sd decrease on the slice.

Results on all the slices:

Assuming LO not nil. We compute sd on the slice from Succ Root to flo. It either increases by at most N-1 when the root moves and decreases otherwise. The proof is done by induction on LO, proving that sd computed from sd to every element in LO follows the above property. Induction step uses Lemmas sd_mid_slice and sd_last_slice.

Lemma sum_dist_evolves

Case LO is nil: sd_decr_LO_nil and sd_decr_LO_nil_RM provide the result. Case LO not nil: sd_mid_last_slices and sd_first_slice provide the result.

Bound on sum_dist

sum_dist is maximal when every node holds a token, maximum given by the sum of distances (induction on the slice on which sum_dist is computed)

Technical lemma to handle particular cases for small values

of N, exhbit the weight of two token holders in sum_dist Induction on the list of nodes (given by (traversal_Pred N Root)) if the liste contains both n1 and n2 then res >= Dist n1 Root + Dist n2 Root else if the list contains n1 then res >= Dist n1 Root else if the list contains n2 then res >= Dist n2 Root