Database of Case Studies Achieved Using CADP

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 our FTP 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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page