A belated proof of self-stabilization

Copyright Notice

The following manuscript

EWD 922: A belated proof of self-stabilization

is held in copyright by Springer-Verlag New York, who have granted permission to reproduce it here.

The manuscript was published as

Distributed Computing 1 (1986): 5-6.

A belated proof of self-stabilization

by Edsger W. Dgksstra

Author's Address: Department of Computer Sciences, The University of Texas at Austin, Austin TX 78750, USA.

I thought that in [0] I had published three solutions, but later I learned that I had also published three problems, as the programs had been given without a demonstration of their correctness. As a partial remedy I here offer such a demonstiation for the solution with three-state machines.

I recall the construction. We consider a ring of at least 3 three-state machines. For each machine a "privilege" is defined, i.e. a boolean function of the state of that machine and of the states of that machine's immediate neighbours; when such a function is true, we say that that privilege "exists". A "move" consists of a machine observing that its privilege exists, followed by a change of that machine's state; moves of neighbours exclude each other in time. We have to show that, independently of the initial state of the whole system, within a finite number of moves (i) precisely one privilege exists and (ii)

EWD922-1

in each unbounded sequence of moves, each machine moves an unbounded number of times.

Each machine state is characterized by a variable ranging over ${0,1,2}$ ; in the descriptions of the moves, additive operations are understood to be reduced mod 3; the variables characterizing the left- and right-hand neighbours are denoted by L and R respectively; moves are recorded as guarded commands with the guards defining the privileges.

The ring consists "in order from left to right" of

(i) "Bottom", i.e. a machine whose state is characterized by $B$ and whose move is given by

B + 1 = R \rightarrow B := B + 2

(ii) one or more normal machines, characterized by a variable locally named $S$ ; their moves are

L = S + 1 \vee S + 1 = R \rightarrow S := S + 1

(iii) "Top", i.e. a machine whose state is characterized by $T$ , whose right-hand neighbour is Bottom, and whose move is

L = B ∧ T ≠ B + 1 \rightarrow T := B + 1

In order to demonstrate self-stabilization, we consider the string starting with $B$ , then the S’s , and ending with T . In that

string we place between neighbours whose states differ an arrow such that in the direction of the arrow the state decreases (mod 3) by 1 . We now give in terms of the arrows the transformations each move may effectuate ; for each transformation we furthermore record the change in y , where

y = \begin{array}{l} \mathrm {t h e n u m b e r o f l e f t - p o i n t i n g a r r o w s +} \ \mathrm {t w i c e t h e n u m b e r o f r i g h t - p o i n t i n g a r r o w s .} \end{array}

for Botham:

\mathrm {f r o m} B \leftarrow R \mathrm {f o} B \rightarrow R \Delta y = + 1 (0)

For a normal machine:

\mathrm {P r o m} L \rightarrow S R t o L S \rightarrow R \Delta y = 0 \tag {7}

f r o m L S \leftrightarrow R t o L \leftrightarrow S R \Delta y = 0 \tag {2}

f r o m L \rightarrow S \leftarrow R t o L S R \Delta y = - 3 \tag {3}

f r o m L \rightarrow S \rightarrow R t o L S \leftarrow R \Delta y = - 3 \tag {4}

\mathrm {P r o m} L \leftarrow S \leftarrow R \mathrm {f o} L \rightarrow S R \Delta y = 0 (5)

For Top (whose privilege also depends on $B!$ )

\begin{array}{l} \mathrm {P r o m} L \rightarrow T \mathrm {t o} L \leftarrow T \Delta y = - 1 \tag {6} \ f r o m L T t o L \leftarrow T \Delta y = + 1 (7) \ \end{array}

If the string contains 1 arrow, that one arrow remains the only one, travelling up and down the string via transformations (1) and (2), and being reflected at the ends via transformations (0) and (6). Note that, if $L \rightarrow T$ represents the only arrow, $L = B ∧ T = B - 1$ , and hence Top's

privilege exists. We conclude from the above that it suffices to show that within a finite number of moves we have precisely 1 arrow in the string.

If the string is free of arrows, $L = B ∧ T = B$ and in the next move, transition (7) creates the situation of precisely 1 arrow in the string.

A further consequence of the two preceding para- graphs is that under all circumstances at least one move is possible. So now we consider an unbounded sequence of moves; in the remainder we shall show that, if the number of arrows is more than 1, $y$ will be decreased within a finite number of moves.

From the design of the move of Top we conclude

at least two successive moves of Top

Next we establish

Lemma 1 A sequence of moves in which Bottom does not move is finite.

Proof From Lemma 0 we conclude that in a sequence of moves in which Bottom does not move, at most one move of Top occurs. So it suffices to show that any sequence of normal moves is

finite. As transformations (3), (4), and (5) decrease the number of arrows and none of the normal moves increases that number, it suffices to show that a sequence of transformations (1) and (2) is finite. But this follows from the topology and the finite length of the string. (End of Proof.)

After these preparations we can now prove our Theorem Within a finite number of moves, there is one arrow in the string.

Proof From lemma 1 we conclude that in an unbounded sequence of moves the number of moves of Bottom is unbounded. Between two successive moves of Bottom, the situation "the left-most arrow (exists and) points to the right" is falsified at least once, a falsification that can only occur in transformation (3), (4), or (6).

If it occurs in transformation (6), we have one arrow in the string and are done.

Otherwise it occurs in transformations (3) or (4), which decrease y by 3 ; only transformations (0) and (7) increase y but - on account of Lemma 0- by at most 2 per move of Bottom; the net result is that, per move of Bottom, y is decreased by at least 1. (End of Proof.)

[0] Self-stabilizing Systems in Spike of Distributed Control, by Dykstra, Edsger W., Comm. ACM Vol 17, nr. 11 (Nov. 1974), 643-644

Dr. Edsger W. Dgikstra worked from 1952 until 1962 at the Mathematical Centre in Amsterdam. From 1962 until 1973 he was Full Professor of Mathematics at the Eindhoven University of Technology. From 1973 until 1984, when he accepted the Schlumberger Centennial chair in Computer Sciences at The University of Texas at Austin, his main function was that of Burroughs Research Fellow.