Verification of Leader Election in Anonymous Rings

Organisation:	Vrije Universiteit Amsterdam, University of Twente, and CWI (The Netherlands) Université du Luxembourg, Faculté des Sciences, de la Technologie et de la Communication
Method:	μCRL
Tools used:	CADP (Construction and Analysis of Distributed Processes) μCRL PRISM
Domain:	Distributed Systems.
Period:	2008
Size:	Up to 260 millions states and 1.4 billion transitions.
Description:	Leader election is the problem of choosing a unique leader in a distributed network. All processes running on the network nodes must execute the same local algorithm. Leader election is a fundamental problem in distributed computing and has many applications: breaking symmetry in a distributed system, executing centralized algorithms in a decentralized environment, recovering from token loss in token-based algorithms, etc. A broad range of leader election algorithms have been proposed, varying in the communication mechanisms, process naming, and network topology. The current study focuses on asynchronous communication with reliable channels but no message order preservation, anonymous network, and bidirectional ring topology. A probabilistic leader election algorithm is proposed, by extending Franklin's algorithm for bidirectional rings. The range of round numbers is limited to 2, making the algorithm finite-state and analyzable using explicit-state exploration methods. Another probabilistic extension of the Dolev-Klawe-Rodeh leader election algorithm was also studied. These algorithms were specified in μCRL and analyzed using the μCRL and CADP tool sets. The CADP model checker provided counterexamples showing that round numbers cannot be omitted from the probabilistic Franklin algorithm, and round numbers modulo 2 do not suffice for the probabilistic Dolev-Klawe-Rodeh algorithm. Finally, the probabilistic model checker PRISM was used to compare the performance of two versions of the probabilistic Franklin algorithm differing in the way fresh identities for the leader are generated.
Conclusions:	Model checking provides a useful way of analyzing probabilistic extensions and variants of leader election protocols. Probabilistic model checkers can also provide precise quantitative results, such as the probability of electing a unique leader within a given number of time steps.
Publications:	[Bakhshi-Fokkink-Pang-vandePol-08] Rena Bakhshi, Wan Fokkink, Jun Pang, and Jaco van de Pol. "Leader Election in Anonymous Rings: Franklin Goes Probabilistic". In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, Proceedings of the 5th IFIP International Conference on Theoretical Computer Science TCS'2008 (Milano, Italy), IFIP, volume 273, pages 57-72, 2008. Full version available on-line at: http://www.few.vu.nl/~rbakhshi/papers/tcs08final.pdf or from the CADP Web site in PDF or PostScript
Contact:	Rena Bakhshi De Boelelaan 1081a 1081HV, Amsterdam Netherlands Tel.: +31 (0)20 59 87757 Email: rbakhshi@few.vu.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page