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.
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).
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 // module for process 1 module process1 // Boolean variable for process 1 x1 : [0..1]; [step] (x1=x3) -> 0.5 : (x1'=0) + 0.5 : (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);
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 | 8 | 24 | 3 | ||
| 5 | 32 | 75 | 4 | ||
| 7 | 128 | 158 | 5 | ||
| 9 | 512 | 273 | 6 | ||
| 11 | 2,048 | 420 | 7 | ||
| 13 | 8,192 | 599 | 8 | ||
| 15 | 32,768 | 810 | 9 | ||
| 17 | 131,072 | 1,053 | 10 | ||
| 19 | 524,288 | 1,328 | 11 | ||
| 21 | 2,097,152 | 1,635 | 12 | ||
We first check the correctness of the protocol, namely that:
We then studied the following quantitative properties:
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 label "stable" = num_tokens=1; // stable configurations (1 token) // From any configuration, a stable configuration is reached with probability 1 "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} ] // Minimum probability reached a stable configuration within K steps (for all configurations) P=? [ F<=K "stable" {"init"}{min} ]
We first show results for the first two properties, i.e. the check that a stable configuration is always reached with probability 1 and the worst-case (maximum) expected time for this to occur:
| N: | Probability 1? | Max. expected time | |
| 3 | true | 1.33 | |
| 5 | true | 3.20 | |
| 7 | true | 6.86 | |
| 9 | true | 12.0 | |
| 11 | true | 17.5 | |
| 13 | true | 24.6 | |
| 15 | true | 33.3 | |
| 17 | true | 42.4 | |
| 19 | true | 53.1 | |
| 21 | true | 65.3 |
For the latter property we observed that, in all the cases considered, the configurations that achieve the maximum expected time are those where three 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. Interestingly, these results corroborate an unproven conjecture by McIver and Morgan [MM05a] that the worst-case time for this algorithm always results from a configuration where there are initially three tokens.
In addition, we computed the minimum expected time to reach a stable configuration given that the initial number of tokens equals k. In this case, the minimum value seems to grow as k increases:
Lastly, we have also plotted the minimum probability of reaching a stable configuration within K steps.
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.
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
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 | ||
We analysed the protocol through the following properties.
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 label "stable" = num_tokens=1; // stable configurations (1 token) // From any configuration, a stable configuration is reached with probability 1 "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.
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:
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).
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);
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 | ||
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.
