www.prismmodelchecker.org

Randomised Consensus Shared Coin Protocol

(Aspnes & Herlihy)

Contents

Related publications: [KNS01a]

Introduction

This case study concerns modelling and verifying the shared coin protocol of the randomised consensus algorithm of Aspnes and Herlihy [AH90] using PRISM. The shared coin protocol returns a preference 1 or 2, with a certain probability, whenever requested by a process at some point in the execution of the consensus algorithm. The shared coin protocol implements a collective random walk parameterised by the number of processes N and the constant K > 1 (independent of N). The consensus algorithm proceeds through rounds and for each round r there is a new copy of the shared coin protocol denoted CFr.

The processes access a global shared counter, initially 0. On entering the protocol, a process flips a coin, and, depending on the outcome, increments or decrements the shared counter. Since we are working in a distributed scenario, several processes may simultaneously want to flip a coin, which is modelled as a nondeterministic choice between probability distributions, one for each coin flip. Having flipped the coin, the process then reads the counter, say observing c. If c >= KN it chooses 1 as its preferred value, and if c <= -KN it chooses 2. Otherwise, the process flips the coin again, and continues doing so until it observes that the counter has passed one of the barriers.

PRISM Model

The PRISM source code in the case when there are 8 processes is given below.

// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
// gxn/dxp 20/11/00

mdp

// constants
const int N=8;
const int K;
const int range = 2*(K+1)*N;
const int counter_init = (K+1)*N;
const int left = N;
const int right = 2*(K+1)*N - N;

// shared coin
global counter : [0..range] init counter_init;

module process1
	
	// program counter
	pc1 : [0..3];
	// 0 - flip
	// 1 - write 
	// 2 - check
	// 3 - finished
	
	// local coin
	coin1 : [0..1];	

	// flip coin
	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
	// write tails -1  (reset coin to add regularity)
	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
	// write heads +1 (reset coin to add regularity)
	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
	// check
	// decide tails
	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
	// decide heads
	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
	// flip again
	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
	// loop (all loop together when done)
	[done] (pc1=3) -> (pc1'=3);

endmodule

// construct remaining processes through renaming
module process2 = process1[pc1=pc2,coin1=coin2] endmodule
module process3 = process1[pc1=pc3,coin1=coin3] endmodule
module process4 = process1[pc1=pc4,coin1=coin4] endmodule
module process5 = process1[pc1=pc5,coin1=coin5] endmodule
module process6 = process1[pc1=pc6,coin1=coin6] endmodule
module process7 = process1[pc1=pc7,coin1=coin7] endmodule
module process8 = process1[pc1=pc8,coin1=coin8] endmodule

// labels
label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & pc7=3 & pc8=3 ;
label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 & coin7=0 & coin8=0 ;
label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 & coin7=1 & coin8=1 ;
label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 & coin6=coin7 & coin7=coin8 ;

// rewards
rewards "steps"
	true : 1;
endrewards

View: printable version          Download: coin8.nm

The table below shows the size of the model (number of state/transitions) for various values of N and K.

Model:   States:
N K
22272
4528
81,040
162,064
324,112
648,208
4222,656
443,136
884,096
16166,016
32329,856
621,258,240
4 2,376,448
8 4,612,864
169,085,696
8261,018,112
4114,757,632
8222,236,672
16437,194,752
1022,761,248,768
45,179,854,848
67,598,460,928

Model checking

There are two properties of the shared coin protocol we need to verify to prove Probabilistic wait free termination.

  • C1: For each fair execution of CFr that starts with a reachable state of CFr, with probability 1 all processes that enter CFr leave CFr.
  • C2: For each fair execution of CFr, and each value v=1,2, the probability that all processes that enter CFr will eventually leave with value v is at least (K-1)/2K.

In the case of C2, we actually calculate the exact (minimum) probability of the processes drawing the same value, as opposed to a lower bound (K-1)/2K established analytically in [AH90] using random walk theory.

Property C1

  • C1: For each fair execution of CFr that starts with a reachable state of CFr, with probability 1 all processes that enter CFr leave CFr.

We express this is PRISM as follows:

P>=1 [ F "finished" ]
View: printable version          Download: coin8_c1.pctl

This is found to be satisfied in all states of the all the models listed in the table above.

Property C2

  • C2: For each fair execution of CFr, and each value v=1,2, the probability that all processes that enter CFr will eventually leave with value v is at least (K-1)/2K.

In this case, we calculate the actual minimum probability, p, for which this condition holds.

For v=1, we express this is PRISM as follows:

Pmin=? [ F "finished"&"all_coins_equal_1" ]
View: printable version          Download: coin8_c2.pctl

The table below shows the computed minimum value of p and the lower bound (K-1)/2K, established analytically in [AH90] using random walk theory.

Model:   p:   (K-1)/2K:
N K
2 2 0.3828140.25
4 0.4377520.3125
8 0.4687830.4375
16 0.4845070.46875
32 0.4927150.484375
64 0.4981930.492188
4 20.3173600.25
40.4063070.3125
80.4532550.4375
160.4770880.46875
320.4903790.484375
6 2 0.2943650.25
4 0.3959060.3125
8 0.4482090.4375
160.4751380.46875
8 2 0.2827900.25
4 0.3907490.3125
8 0.4458310.4375
160.4747470.46875
10 20.2759190.25
40.3876930.3125
60.4254500.416667

For the case N=2, the following plot illustrates the results graphically:

Expected time

Finally, we compute the minimum and maximum expected number of steps required for completion of the algorithm.

We express this is PRISM as follows:

R{"steps"}min=? [ F "finished" ]
R{"steps"}max=? [ F "finished" ]
View: printable version          Download: coin8_steps.pctl

The results, for a selection of values of N and K are as follows:

Model   Runtime and Problem Size Analysis for Property (1)
N K err States Transitions Runtime VI Runtime LP NumVars NumCons
220.02724920.0950.06343342
20.012724920.0870.049343342
20.052724920.0670.05343342
20.12724920.0880.044343342
20.152724920.0870.05343342
40.05289720.4740.076735742
40.015289720.4750.095735742
40.055289720.4830.076735742
40.15289720.4430.076735742
40.155289720.4270.082735742
60.078414521.3510.09711271142
60.0178414521.310.10711271142
60.0578414521.3350.10811271142
60.178414521.2040.09811271142
60.1578414521.3930.10811271142
80.0104019322.7220.12415191542
80.01104019322.4490.13815191542
80.05104019322.9310.16115191542
80.1104019322.8280.13815191542
80.15104019322.9430.14415191542
100.0129624125.1330.14219111942
100.01129624125.1320.19619111942
100.05129624125.0140.1719111942
100.1129624125.0910.17819111942
100.15129624125.3070.16919111942

Case Studies