# Randomised Self-Stabilising Algorithms

### Contents

Related publications: [KNP12a]

### Introduction

In this case study we consider a number of self-stabilising algorithms from the literature.

A self-stabilising protocol for a network of processes is a protocol which, when started from some possibly illegal start configuration, returns to a legal/stable configuration without any outside intervention within some finite number of steps. For further details on self-stabilisation see here.

In each of the protocols we consider, the network is a ring of identical processes. The stable configurations are those where there is exactly one process designated as "privileged" (has a token). This privilege (token) should be passed around the ring forever in a fair manner.

For each of the protocols, we compute the minimum probability of reaching a stable configuration and the maximum expected time (number of steps) to reach a stable configuration (given that the above probability is 1) over every possible initial configuration of the protocol.

### Herman [Her90]

The first protocol we consider is due to Herman [Her90]. The protocol operates synchronously, the ring is oriented, and communication is unidirectional in the ring. In this protocol the number of processes in the ring must be odd.

Each process in the ring has a local boolean variable xi, and there is a token in place i if xi=x(i-1). In a basic step of the protocol, if the current values of xi and x(i-1) are equal, then it makes a (uniform) random choice as to the next value of xi, and otherwise it sets it equal to the current value of x(i-1).

##### The Model

By way of example, the PRISM source code for the case where there are three processes in the ring is given below.

```// herman's self stabilising algorithm [Her90]
// gxn/dxp 13/07/02

// the procotol is synchronous with no nondeterminism (a DTMC)
dtmc

const double p = 0.5;

// module for process 1
module process1

// Boolean variable for process 1
x1 : [0..1];

[step]  (x1=x3) -> p : (x1'=0) + 1-p : (x1'=1);
[step] !(x1=x3) -> (x1'=x3);

endmodule

// add further processes through renaming
module process2 = process1 [ x1=x2, x3=x1 ] endmodule
module process3 = process1 [ x1=x3, x3=x2 ] endmodule

// cost - 1 in each state (expected number of steps)
rewards "steps"
true : 1;
endrewards

// set of initial states: all (i.e. any possible initial configuration of tokens)
init
true
endinit

// formula, for use in properties: number of tokens
// (i.e. number of processes that have the same value as the process to their left)
formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x1?1:0);

// label - stable configurations (1 token)
label "stable" = num_tokens=1;

```
##### Model Statistics

The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states and transitions in the DTMC representing the model. The second part refers to the MTBDD used to store it: the total number of nodes and the number of leaves (terminal nodes).

 N: Model: MTBDD: States: Transitions: Nodes: Leaves: 3 8 28 24 3 5 32 244 75 4 7 128 2,188 158 5 9 512 19,684 273 6 11 2,048 177,148 420 7 13 8,192 1,594,324 599 8 15 32,768 14,348,908 810 9 17 131,072 129,140,164 1,053 10 19 524,288 1,162,261,468 1,328 11 21 2,097,152 10,460,353,204 1,635 12
##### Model Checking

We first check the correctness of the protocol, namely that:

• From any configuration, a stable configuration is reached with probability 1

We then study its performance, in particular:

• The maximum/minimum expected time to reach a stable configuration

For the latter, we consider the worst-case behaviour over all possible initial configurations and over all initial configurations with k tokens.

These properties can be expressed in PRISM as follows.

```const int k; // number of tokens
const int K; // number of steps

// labels
label "k_tokens" = num_tokens=k; // configurations with k tokens

// From any configuration, a stable configuration is reached with probability 1
filter(forall, "init" => P>=1 [ F "stable" ])

// Maximum expected time to reach a stable configuration (for all configurations)
R=? [ F "stable" {"init"}{max} ]

// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
R=? [ F "stable" {"k_tokens"}{max} ]
R=? [ F "stable" {"k_tokens"}{min} ]
```

The minimum probability of reaching a stable state is 1 for all models built (up to N = 21).

The worst-case expected time, over all initial configurations, is shown in the plot below (marked "PRISM"). For comparison, we also plot the upper bound on this value proved by Kiefer et al. [KMO+11] of (approximately) 0.64N2. As the graph illustrates, the actual worst-case value is considerably lower. Elsewhere, McIver and Morgan [MM05a] showed that the the worst-case time for initial configurations with 3 tokens is 4abc/N, where a, b and c are the distances between the three tokens. This therefore represents a lower bound on the worst-case expected time and is also shown in the plot. Kiefer, conjecture that this represents the worst-case for any number of tokens. Our results corroborate this conjecture precisely for all models built. Further evidence of the correctness of McIver and Morgan's conjecture is shown in the graph below, where we plot, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens equals k. As can be seen, for all models up to N = 21, the worst case is for k = 3 tokens and the maximum expected time decreases for increasing values of k. Lastly, we examine the effect of the probabilistic value used for the random choice in Herman's algorithm (p in the PRISM code above).

As the plot below indicates, for values of N = 9 or below, p = 0.5 is the optimum value. However, interestingly, for larger values of N, this does not hold. In fact, in these case, values of p other than 0.5 (i.e. biased coins) result in better performance (lower expected execution time) for the protocol. Moreover, zooming in on the above plots reveals unexpected trends for values of p close to 0.5:

 N = 7: N = 9: N = 11: See [KNP12a] for further results on this model.

### Israeli and Jalfon [IJ90]

The protocol we consider in this section is due to Israeli and Jalfon [IJ90]. It operates asynchronously with an arbitrary scheduler, the ring is oriented and communication is bidirectional in the ring.

Each process has a boolean variable qi which represents the fact that a token is in place i. A process is active if it has a token and only active processes can be scheduled. When an active process is scheduled, it makes a (uniform) random choice as to whether to move the token to its left or right. Note that if a process ends up with two tokens, these tokens are merged into a single token.

##### The Model

By way of example, the PRISM source code for the case where there are three processes in the ring is given below.

```// Israeli-Jalfon self stabilising algorithm
// dxp/gxn 10/06/02

mdp

// variables to represent whether a process has a token or not
// note they are global because they can be updated by other processes
global q1  : [0..1];
global q2  : [0..1];
global q3  : [0..1];

// module of process 1
module process1

[] (q1=1) -> 0.5 : (q1'=0) & (q3'=1) + 0.5 : (q1'=0) & (q2'=1);

endmodule

// add further processes through renaming
module process2 = process1 [ q1=q2, q2=q3, q3=q1 ] endmodule
module process3 = process1 [ q1=q3, q2=q1, q3=q2 ] endmodule

// cost - 1 in each state (expected steps)
rewards "steps"
true : 1;
endrewards

// formula, for use here and in properties: number of tokens
formula num_tokens = q1+q2+q3;

// initial states (at least one token)
init
num_tokens >= 1
endinit
```
##### Model Statistics

The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).

 N: Model: MTBDD: States: Nodes: Leaves: 3 7 48 3 4 15 85 3 5 31 129 3 6 63 177 3 7 127 229 3 8 255 285 3 9 511 345 3 10 1,023 409 3 11 2,047 477 3 12 4,095 549 3 13 8,191 625 3 14 16,383 705 3 15 32,767 789 3 16 65,535 877 3 17 131,071 969 3 18 262,143 1,065 3 19 524,287 1,165 3 20 1,048,575 1,269 3 21 2,097,151 1,377 3
##### Model Checking

We analysed the protocol through the following properties.

• From any configuration, a stable configuration is reached with probability 1;
• What ‎is the maximum/minimum expected time to reach a stable configuration (for all configurations and for configurations with k tokens)?
• What is the minimum probability of reaching a stable configuration within K steps (for all configurations)?

Which can be expressed in PRISM as follows.

```const int k; // number of tokens
const int K; // number of steps

// labels
label "k_tokens" = num_tokens=k; // configurations with k tokens

// From any configuration, a stable configuration is reached with probability 1
filter(forall, "init" => P>=1 [ F "stable" ])

// Maximum expected time to reach a stable configuration (for all configurations)
Rmax=? [ F "stable" {"init"}{max} ]

// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
Rmax=? [ F "stable" {"k_tokens"}{max} ]
Rmin=? [ F "stable" {"k_tokens"}{min} ]

// Minimum probability reached a stable configuration within K steps (for all configurations)
Pmin=? [ F<=K "stable" {"init"}{min} ]
```

The table below gives the model checking statistics when checking that from any configuration, a stable configuration is reached with probability 1 and calculating the maximum expected time to reach a stable configuration.

 N: A stable configuration is reached with probability 1 Maximum expected time to reach a stable configuration Iterations: Result: Iterations: Result: 3 3 true 21 3.0 4 5 true 39 6.0 5 7 true 61 10.0 6 9 true 87 15.0 7 12 true 116 21.0 8 14 true 149 28.0 9 16 true 186 36.0 10 19 true 226 45.0 11 23 true 270 55.0 12 25 true 317 66.0 13 28 true 367 78.0 14 31 true 420 91.0 15 35 true 477 105.0 16 38 true 537 120.0 17 41 true 599 136.0 18 44 true 665 153.0 19 48 true 733 171.0 20 52 true 805 190.0 21 55 true 879 210.0

In all the cases considered, the configurations which achieve the maximum expected time are those where all the processes have tokens. To illustrate this fact, in the graph below we have plotted, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens equals k. In addition, below we have plotted the minimum expected time to reach a stable configuration given that the initial number of tokens k. Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps. ### Beauquier, Gradinariu and Johnen [BGJ99]

Now we consider the self-stabilising protocol of Beauquier, Gradinariu and Johnen [BGJ99] for an arbitrary scheduler. It operates asynchronously, the ring is oriented, communication is unidirectional in the ring, and the number processes in the ring must be odd.

Each process two boolean variables: di and pi where:

• di=d(i-1) process i is said to have a deterministic token;
• if pi=p(i-1) process i is said to have a probabilistic token.

The stable configurations are those where there is only one probabilistic token. A process is active if it has a deterministic token and only active processes can be scheduled. When an active process is scheduled, it sets di to be the negation of it current value (passes the deterministic token), and if it also has a probabilistic token, it makes a (uniform) random choice as to the next value of pi (randomly selects whether to pass the probabilistic token or not).

##### The Model

By way of example, the PRISM source code for the case where there are three processes in the ring is given below.

```// self stabilisation algorithm Beauquier, Gradinariu and Johnen
// gxn/dxp 18/07/02

mdp

// module of process 1
module process1

d1 : bool; // probabilistic variable
p1 : bool; // deterministic variable

[] d1=d3 &  p1=p3 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
[] d1=d3 & !p1=p3 -> (d1'=!d1);

endmodule

// add further processes through renaming
module process2 = process1 [ p1=p2, p3=p1, d1=d2, d3=d1 ] endmodule
module process3 = process1 [ p1=p3, p3=p2, d1=d3, d3=d2 ] endmodule

// cost - 1 in each state (expected steps)
rewards "steps"
true : 1;
endrewards

// initial states - any state with more than 1 token, that is all states
init
true
endinit

// formula, for use in properties: number of tokens
formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p1?1:0);
```
##### Model Statistics

The table below shows statistics for protocol we have built for different numbers of processes (size of the ring). The first section gives the number of states in the MDP representing the model. The second part refers to the MTBDD which represents this MDP: the total number of nodes and the number of leaves (terminal nodes).

 N: Model: MTBDD: States: Nodes: Leaves: 3 64 141 3 5 1,024 336 3 7 16,384 559 3 9 262,144 810 3 11 4,194,304 1,089 3
##### Model Checking

The table below gives the model checking statistics when calculating, over all configurations, the minimum probability that a stable configuration is reached and the maximum expected time to reach a stable configuration.

 N: A stable configuration is reached with probability 1 Maximum expected time to reach a stable configuration Iterations: Result: Iterations: Result: 3 2 true 20 2.00 5 8 true 64 11.9 7 21 true 170 37.8 9 40 true 380 84.4 11 65 true 732 162

In all the cases considered, the configurations which achieve the maximum expected time are those where only three processes have probabilistic tokens. To illustrate this fact, in the graph below we have plotted, as k varies, the maximum expected time to reach a stable configuration given that the initial number of tokens k. In addition, below we have plotted the minimum expected time to reach a stable configuration given that the initial number of tokens equals k. Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps. 