Vrije Universiteit Amsterdam, University of Twente, and CWI (The Netherlands)
Université du Luxembourg, Faculté des Sciences, de la Technologie et de la Communication
CADP (Construction and Analysis of Distributed Processes)
Up to 260 millions states and 1.4 billion transitions.
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.
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
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
De Boelelaan 1081a
Tel.: +31 (0)20 59 87757
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|