Herman’s algorithm is a classical example of a randomised self-stabilisation protocol [ Herman 1990 ]. Imagine a network of processes, arranged in a ring, with each process possibly holding a token. ‘Legitimate’ configurations are those in which a token is held by exactly one process. The aim of a self-stabilisation protocol is to guide the network towards legitimate configurations. Let us assume that each process possesses a distinguished two-valued variable, and let us adopt the convention that a process is deemed to hold a token if its distinguished variable has the same value as that of its immediate right-hand neighbour. (Note that in order for this representation scheme to make sense, there must be an odd number of processes in the network.) The algorithm works as follows. At every time step, each process determines whether or not it holds a token. If it does, it flips its distinguished variable with probability 1, and otherwise sets its distinguished variable equal to that of its right-hand neighbour. We assume that processes execute synchronously. What we would like to show is that such a protocol is correct, i.e., that it always eventually leads the system to a legitimate, single-token configuration. To this end, we implemented Herman’s algorithm in our probabilistic programming language for various numbers of processes in the network. The code for a 15-process network is given below.
void main() {
int%2 x[15]; int%2 z; int%3 token; int%15 i;
token:=2;
while(not (token=1)) do {
token:=0;
i:=0;
z:=x[0];
while (i+1) do {
if (x[i]=x[i+1]) then
x[i]:=coin else x[i]:=x[i+1];
if (i>0) and (x[i-1]=x[i]) then
token:=case(token)[1,2,2];
i:=i+1
};
if (x[i]=z) then x[i]:=coin else x[i]:=z;
if (x[i-1]=x[i]) then token:=case(token)[1,2,2];
if (x[i]=x[0]) then token:=case(token)[1,2,2]
}
}
Most of the syntax is self-explanatory, perhaps with the exception of the statement token:=case(token) [ Abramsky et al 2000, Bhargava, Palamidessi 2005 ]. This is similar to the switch construct in C, and is equivalent to if token=0 then token:=1 else if token=1 then token:=2 else if token=2 then token:=2;
In the program, the distinguished variables of processes are held in a 15-element array x of two-valued variables. The inner while loop simulates the synchronous execution of the network over a single time step. In this loop, the variable token is used to count the total number of tokens present in the network, with the value 2 representing ‘two or more’. Recall the use of modulo arithmetic so that variables that overflow simply cycle through 0. The outer while loop ensures that the code is executed until the network contains just a single token. Note that our implementation is a closed program of type void. It should be clear that the correctness of Herman’s algorithm (a single-token configuration is always eventually reached) corresponds to the assertion that our program terminates with probability 1. And indeed, when running apex, the output is the one-state automaton corresponding to void main() { skip } already depicted in Section 3. We remark that it is trivial to modify the code to model networks with different numbers of processes: it suffices to replace the two occurrences of the number ‘15’ in the first line by whatever other value is desired. Although all instances of our program ultimately give rise to the same single-state automaton, the computation times of apex increase with the sizes of the networks modelled. This is not surprising since an n-process network has 2n distinct configurations (ignoring symmetries). The intermediate automata generated by apex reflect this growth, although this is mitigated to some extent by the use of state-space reduction techniques throughout the computation.