Synchronous Leader Election Protocol

(Itai & Rodeh)

Contents

• Introduction
• Model Statistics
• Model Checking

Introduction:

This case study is based on the synchronous leader election protocol of Itai & Rodeh [IR90]. This protocol solves the following problem.

Given a synchronous ring of N processors design a protocol such that they will be able to elect a leader (a uniquely designated processor) by sending messages around the ring.

The protocol proceeds in rounds and is parametrised by a constant K. Each round begins by all processors (independently) choosing a random number (uniformly) from {1,...,K} as an id. The processors then pass their ids around the ring. If there is a unique id, then the processor with the maximum unique id is elected the leader, and otherwise the processors begin a new round.

We assume that the ring is synchronous: there is a global clock and at every time slot a processor reads the message that was sent at the previous time slot (if it exists), makes at most one state transition and then may send at most one message.

By way of example, the PRISM source code for the case where N=4 and K=8 is given below.

// synchronous leader election protocol (itai & Rodeh)
// dxp/gxn 25/01/01
// N=4 and K=8

dtmc

// CONSTANTS
const N=4; // number of processes
const K=8; // range of probabilistic choice

// counter module used to count the number of processes that have been read
// and to know when a process has decided
module counter
	
	// counter 
	c : [1..N-1];
	
	// reading
	[read] c<N-1 -> (c'=c+1);
	// finished reading
	[read] c=N-1 -> (c'=c);
	//done
	[done] u1 | u2 | u3 | u4 -> (c'=c);
	// pick again reset counter 
	[retry] !(u1 | u2 | u3 | u4) -> (c'=1);
	// loop (when finished to avoid deadlocks)
	[loop] s1=3 -> (c'=c);
	
endmodule

//  processes form a ring and suppose:
// process 1 reads process 2
// process 2 reads process 3
// process 3 reads process 1
module process1
	
	// local state
	s1 : [0..3];
	// s1=0 make random choice
	// s1=1 reading
	// s1=2 deciding
	// s1=3 finished
	
	// has a unique id so far (initially true)
	u1 : bool;
	
	// value to be sent to next process in the ring (initially sets this to its own value)
	v1 : [0..K-1];
	
	// random choice
	p1 : [0..K-1];
	
	// pick value
	[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
	             + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
	// read
	[read] s1=1 &  u1 & !p1=v2 & c<N-1 -> (u1'=true) & (v1'=v2);
	[read] s1=1 &  u1 &  p1=v2 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
	[read] s1=1 & !u1 &  c<N-1 -> (u1'=false) & (v1'=v2);
	// read and move to decide
	[read] s1=1 &  u1 & !p1=v2 & c=N-1 -> (s1'=2) & (u1'=true) & (v1'=0) & (p1'=0);
	[read] s1=1 &  u1 &  p1=v2 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0) & (p1'=0);
	[read] s1=1 & !u1 &  c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
	// done
	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
	//retry
	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
	// loop (when finished to avoid deadlocks)
	[loop] s1=3 -> (s1'=3);
	
endmodule

// construct remaining processes through renaming
module process2=process1[s1=s2,p1=p2,v1=v2,u1=u2,v2=v3] endmodule
module process3=process1[s1=s3,p1=p3,v1=v3,u1=u3,v2=v4] endmodule
module process4=process1[s1=s4,p1=p4,v1=v4,u1=u4,v2=v1] endmodule

// REWARDS -expected number of rounds
rewards "rounds"
	[pick] true : 1;
endrewards

Model Statistics

The table below shows statistics for the DTMCs we have built for different values of the constants N and K. The tables include:

• the number of states and transitions in the DTMC representing the model;
• both the number of nodes and leaves of the MTBDD which represents the model;
• the construction time which equals the time taken for the system description to be parsed and converted to the MTBDD representing it, and the time to perform reachability, identify the non-reachable states and filter the MTBDD accordingly;
• the number of iterations required to find the reachable states (which is performed via a BDD based fixpoint algorithm).

N:	K:		Model:			MTBDD:			Construction:
			States:	Transitions:		Nodes:	Leaves:		Time (s):	Iter.s:
3	2		22	29		367	3		0.059	5
	4		135	198		1,781	3		0.196	5
	6		439	654		5,632	3		0.37	5
	8		1,031	1,542		10,595	3		0.658	5
	10		2,007	3,006		23,382	3		1.501	5
	12		3,466	5,193		29,617	3		1.556	5
	14		5,495	8,238		51,000	3		1.624	5
	16		8,199	12,294		69,553	3		4.719	5
4	2		55	70		908	3		0.079	6
	4		782	1,037		10,801	3		0.242	6
	6		3,902	5,197		58,324	3		1.427	6
	8		12,302	16,397		165,625	3		10.90	6
	10		30,014	40,013		473,188	3		38.38	6
	12		62,222	82,957		929,667	3		163.6	6
5	2		136	167		1,731	3		0.067	7
	4		4,124	5,147		41,528	3		0.623	7
	6		31,133	38,908		337,108	3		15.28	7
	8		131,101	163,868		1,274,313	3		231.5	7
6	2		329	392		3,163	3		0.086	8
	4		20,524	24,619		140,735	3		2.619	8
	6		233,340	279,995		1,732,096	3		561.7	8
8	2		1803	2,058		7857	3		0.147	10
	4		458,847	524,382		1,131,806	3		300.0	10
10	2		9,229	10,252		16,128	3		0.276	12

Model Checking:

We have model checked the following properties:

• With probability 1, eventually a leader is elected.

  This property, in the case when N=4, can be expressed in PCTL as follows:

  P>=1 [ true U (s1=3 & s2=3 & s3=3 & s4=3) ]

  Model checking times:

  N:	K:		Prob1 precomputation:
  			Time (s):	Iterations:
  3	2		0.00	18
  	4		0.01	18
  	6		0.05	18
  	8		0.09	18
  	10		0.21	18
  	12		0.35	18
  	14		0.52	18
  	16		0.74	18
  4	2		0.01	22
  	4		0.12	22
  	6		0.68	22
  	8		2.08	22
  	10		6.83	22
  	12		13.9	22
  5	2		0.02	26
  	4		0.67	26
  	6		8.33	26
  	8		116	26
  6	2		0.05	30
  	4		3.42	30
  	6		148	30
  8	2		0.17	38
  	4		72.5	38
  10	2		0.43	46

  
  Conclusion: the property holds in all states

• The probability of electing a leader within L rounds.

  This property, in the case when N=4, can be expressed in PCTL as follows:

  P=? [ true U<=L*(N+1) (s1=3 & s2=3 & s3=3 & s4=3) ]

  In the graphs below we have plotted these expected values as L varies for a range of values of N and K.

  • N=3

    

  • N=4

    

  • N=5

    

  • K=2

    

  • K=4

    

• The expected number of rounds to elect a leader.

  This property, in the case when N=4, can be expressed in PCTL as follows:

  R=? [ F (s1=3 & s2=3 & s3=3 & s4=3) ]

  In the graphs below we have plotted these expected values for a range of values of N and K.

  
  

Site hosted at the Department of Computer Science, University of Oxford