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 Z

/contains:/ Definitions and results about Z and convexity /assumes:/ Parameter k>1; the network is a unidirectional rooted ring; assumption: N <= k

• convex: A configuration is said convex w.r.t. to a given value vr if vr is the value of Root and all the nodes holding this value vr shape a convex sequence of vr-valued nodes made of consecutive successors of the root. Convex for a value vr is equivalent to
  • vr is the value of the root and it is actually convex
  • otherwise, no node holds the value vr
  There always exists a value that satisfies convex (This is due to the fact that N <= k).
• Z: The potential Z of a configuration g is
  • 0 if g is convex for the value of the Root
  • the distance to the closest absent value from the Root (modulo k), otherwise
  i.e. Z g = min { z < k | convex g ((v g Root + z) mod k) }
• When Z is null: 'Z g = 0' is equivalent to 'g is convex for the root value'; and a configuration where Z is 0 and where the root holds a token is legitimate.
• Z evolution during a step from an illegitimate configuration:
  • Z decreases when the root executes
  • Z does not increase.
• Bound on Z: Z is upper bounded by N-1. If the configuration is convex, the result is trivial. We consider a non-convex configuration. We use counting arguments which stands on Lemma all_here (that asserts that every value between 0 and Z-1 is represented in the ring).
• When Z g is N - 1: g is of a particular shape. There exists a non-root node, which is not the successor of the root, that holds the root value; moreover, every value from (v g Root + 1) mod k to (v g Root + N-2) mod k is held by a single node. From this observation, easily follows that Z g' <= N - 2.

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

Convexity

A configuration is said convex wrt to a given value vr if

• vr is the value of Root and
• all the nodes holding this value vr shape a convex sequence of vr valued nodes made of consecutive successors of the root.

For example,

• Root->5 5 5 6 3 4 0 is convex for vr = 5
• Root->5 5 5 6 3 4 0 is not convex for any vr <> 5
• Root->5 5 5 6 3 4 5 is not convex for any vr
• Root->5 5 6 2 5 3 0 is not convex for any vr

The convex predicate is weakly-decidable

Boolean getters for convex

Convex for a value vr is equivalent to

• vr is the value of the root and it is actually convex
• otherwise, no node holds the value vr

There always exists a value that satisfies convex. This is due to the fact that N <= k. Here follows the outline of the proof. If the value of the root is convex, then we are done. Otherwise, the value we are looking for is not in the ring (see Lemma convex_equiv). We now focus on the case when the root value is not convex. We first prove that the number of values in the ring is smaller or equal to N (the ring size), using the Library Count. present x := exists n, v (g n) = x. Num_Card Smaller (@eqSig nat eq present) N In particular, we exhibit the following injection relation:

• a present value x corresponds to a natural value (less than N) j when x is the value of the node located at j successor edges from the root.

Let nV be the number values present in the ring: Num_Card Same (eqSig present) nV In particular, we have nV <= N <= k (using transitivity of Card). Let nP be the number of values that satisfy convex (i.e. absent from the ring). P := fun V : nat => V < k /\ convex g V Num_Card Same (eqSig P) nP We show that nV + nP = k using (disjoint union of Card). Now comes the proof: it is split in two cases, depended if nV is less than k or equal to k.

• Case nV < k. We show that nP >0 and then pick an element V from P (i.e., such that V < k /\ convex g V].
• Case nV = k. Then the number of present is exactly N, the number of nodes in the ring: Card Same (@eqSig _ eq present) eqN From this hypothesis, we can show that convex g (v (g Root)), a contradiction.
  Indeed, if the root is the unique node to hold this value, we are done. Otherwise, we count the number of values present in the ring, except the one of the root, using: present_outside_Root := fun x => exists n : Node, ~eqN n Root /\ v (g n) = x and obtain that: it is less than N and also equal to the number of values present in the ring, that is N, a contradiction.

Non-convex properties

When the configuration is not convex, there exists a non-root node that holds the root value (this directly comes from the definition)

Z

The potential Z of a configuration g is

• 0 if g is convex for the value of the Root
• the distance to the closest absent value from the Root (modulo k), otherwise

i.e. Z g = min { z < k | convex g ((v g Root + z) mod k) } For example, with k=7,

• Root->5 5 5 6 3 4 0 has potential 0
• Root->5 5 5 6 3 4 5 has potential 2 (since the closest absent value is 0, at distance 2 from 5)
• Root->5 5 6 2 5 3 0 has potential 3 (since the closest absent value is 1, at distance 3 from 5)

Conv: Boolean function, (Conv g j) returns true when g is convex for the value (vR + j) mod k, where vR is the value of the root.

n.b.: for a function f and a value k, min_below f n is specified by: min_below f n = n /\ (forall x, x < n -> f x = false) \/ min_below f n < n /\ is_minimum f (min_below f n) where, as expected, (is_minimum f m) means: f m = true /\ (forall m', m' < m -> f m' = false) (is_minimum f m) is hence the minimum natural value on which f returns true. (min_below f n) returns

• either n if no value above n allows f to return true
• or the minimum value above n on which f is true.

The potential Z is always smaller than k since there always exists a value < k, such that convex holds (see Lemma convex_exists above).

The potential Z is actually the minimum among the convex values

When Z is zero...

'Potential Z is 0' is equivalent to 'the configuration is convex for the root value'.

In a legitimate configuration, Z is 0, since the configuration is convex. To prove this, we use the characterization of a legitimate configuration ls_charac.

A configuration where Z is 0 and where the root holds a token is legitimate. Indeed, in such configuration, every node holds one and the same value (the root one).

Z-evolution during a step from an illegitimate configuration

The potential Z decreases when the root executes from a illegitimate configuration. We first show that the potential at g is not null, using Z_0_Token_Root_Leg_state. (Indeed, every value in the ring would be equal to the one of the root, hence there would be a unique token, hence this would be a legitimate configuration.) Now, we have:

• the Root holds a Token, i.e., its value is equal to the value of its predecessor (a) Token g Root and (b) v (g Root) = v (g (Pred Root))
• the Root increments its value modulo k (c) v (g' Root) = (v (g Root) + 1) mod k

To show that the potential is g' has decreased, we rewrite potential as minimum (using Z_min) and applies Lemma is_minimum_lt that says that if M1 (resp. M2) is the minimum of some set A1 (resp. A2) and if for every value in A1, there exists a smaller value in A2, then M2 is smaller than M1. Hence, for any value x such that (x + v (g Root)) mod k is absent from the ring in configuration g, we have to build a smaller value x' such that (x + v (g Root)) mod k is absent from the ring in configuration g. If x >= k, we just pick the value given by convex_exists in g'; as this value is smaller than k, we are done. If x < k, x cannot be 0 (resp. 1 otherwise the potential in g (resp. in g') is null. Then the value we are looking for is (x-1), that is to say: we prove that the configuration g' is convex for value (v (g' Root) + (x - 1)) mod k = (v (g Root) + x) mod k. Namely, we prove that forall n, (v (g Root) + x) mod k <> v (g' n) since no value appears in the ring but ((v (g Root) + 1) mod k) and 1 < x < k.

The potential Z does not increase from a illegitimate configuration. We rewrite potentials as minimum (using Z_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.

Bound on Z

Every value between 0 and pot_with_Root-1 is present at some node in the ring. Indeed, Z is minimum among the convex values (v+j)mod k.

Z is upper bounded by N-1 If the configuration is convex, the result is trivial. We consider a non convex configuration. We use counting arguments which stands on all_here (that asserts that every value between 0 and Z-1 is represented in the ring).

• presentNR are the nodes which hold a value different from the root. Cardinal = NR
• presentR are the nodes which hold the root value. Cardinal = R

We show that R >=2 due to nonconvex_Root. And that N = NR + R. Hence NR <= N - 2. Now, Z g - 1 <= NR due to pot_with_root definition. Hence the result.

When Z is N - 1: in a step from a non-legitimate

configuration, it decreases whatever be the node which moves. SKETCH Situation : (vR = value of the Root) There exists a unique non-root node (which neither the successor of the root) which holds vR. For every value between vR+1 et vR+N-2, there exists a unique node which holds this value. Counting arguments. In a step of the algorithm,

• If the root moves then the value of the root becomes vR+1 as vR+1+N-2 is absent (and no value can appear) we obtain Z g' <= N-2
• Otherwise, there exists a node n which moves but whose successor does not. (induction which exhibits such a node, the closest from the root)

If the value of n is vR, then this vR disappears:

• the root still holds vR
• its successort may also holds vR if it has moved

In both cases, we get a convex configuration hence Z g' = 0. If the value vn of n is not vR, then we have

• vR < vn < vR+N-1

n is the only node to hold vn and vn is absent from g'. Hence Z g' < N-1

We note presentX x n the predicate which means that node n holds present value x

The number of non-root nodes is N-1.

Let Ua = { n, ~n==Root /\ exists x < a, x<N-1 /\ presentX x n } Ua_card defines the number of non-root nodes in Ua.

From Lemmas all_here and nonconvex_Root, we know that for each present value in {0, ..., N-2}, there exists a non-root node which holds it.

Let Up_a = { n | ~ n == Root /\ presentX a n } for any value a. Up_a has a cardinality (see Upa_card) which is positive (see Upa). The results are direct from the definition of the set and from Lemma AB.

We show that forall a in {1, ..., N-1}, |Ua| >= a Induction on a. The base case, for a=1, is provided by nonconvex_Root: this exhibits a non-root node withe the same value as the root. For induction step, we write Ua = U(a-1) Union {n, ~n==Root /\ presentX a n} (This is a disjoint union.) By induction hypothesis, |U(a-1)| >= a - 1 and we can prove that |{n, ~n==Root /\ presentX a n}| >= 1 since Lemma all_here provides a node with present value a.

The number of non-root nodes with a present value smaller than N-1 is exactly N-1. Indeed, it is smaller than or equal to the number of non-root nodes, ie N-1 (see HNR) we use the implication of predicates and Inj_impl. It is also greater or equal due to Lemma Ua.

Using cc above, we know that the number of non-root nodes with a present value x<N-1 is (N-1) If there exists a non-root node with a non-present value, then by disjoint union of the sets the number of non-root nodes with a present value x<N-1 would be smaller than (N-1). This proof uses the fact that we can enumerate every natural number between 0 and N-2 in order to check if the value is present of not.