www.prismmodelchecker.org

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;

View: printable version          Download: herman3.pm
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
112,048 177,148 420 7
138,192 1,594,324 599 8
1532,768 14,348,908 810 9
17131,072 129,140,164 1,05310
19524,288 1,162,261,468 1,32811
212,097,15210,460,353,2041,63512
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} ]
View: printable version          Download: herman.pctl

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.

plot: expected time to reach a stable configuration from any initial state

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.

plot: expected time to reach a configuration when the initial number of tokens equals 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.

plot: optimum performance for differing p

Moreover, zooming in on the above plots reveals unexpected trends for values of p close to 0.5:

N = 7:
plot: optimum performance for differing p
N = 9:
plot: optimum performance for differing p
N = 11:
plot: optimum performance for differing p

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
View: printable version          Download: ij3.nm
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
101,023 409 3
112,047 477 3
124,095 549 3
138,191 625 3
1416,383 705 3
1532,767 789 3
1665,535 877 3
17131,071 969 3
18262,143 1,0653
19524,287 1,1653
201,048,5751,2693
212,097,1511,3773
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} ]
View: printable version          Download: ij.pctl

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 3true21 3.0
4 5true39 6.0
5 7true61 10.0
6 9true87 15.0
7 12true11621.0
8 14true14928.0
9 16true18636.0
1019true22645.0
1123true27055.0
1225true31766.0
1328true36778.0
1431true42091.0
1535true477105.0
1638true537120.0
1741true599136.0
1844true665153.0
1948true733171.0
2052true805190.0
2155true879210.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.

plot: expected time to reach a configuration when 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.

plot: minimum expected time to reach a configuration when the initial number of tokens equals k

Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps.

plot: 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);
View: printable version          Download: beauquier3.nm
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
114,194,304 1,0893
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 true20 2.00
5 8 true64 11.9
7 21true170 37.8
9 40true380 84.4
1165true732 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.

plot: expected time to reach a configuration when 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 equals k.

plot: minimum expected time to reach a configuration when the initial number of tokens equals k

Lastly, we have also plotted the minimum probability of reaching a stable configuration within k steps.

plot: minimum probability of reaching a stable configuration within k steps

Case Studies