Database of Case Studies Achieved Using CADP

Distributed Leader Election Algorithms for Unidirectional Ring Networks

Organisation: INRIA Rhone-Alpes (FRANCE)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Distributed algorithms.

Period: 1996

Size: LOTOS description of the Leader election algorithm in a reliable network: 100 lines
LOTOS description of the Leader election algorithm in an unreliable network, without station crashes: 106 lines
LOTOS description of the Leader election algorithm with station crashes: 128 lines

Description: Distributed leader election algorithms aim at designating a unique member in a set of stations connected by a network. These algorithms depend on the topology of the network. In the particular case of unidirectional ring networks, two famous algorithms have been proposed, the first one by G. Le Lann [Lan77] and its variant proposed by E. Chang and R. Roberts [CR79].

We studied these two algorithms and several variants, in various contexts, taking into account message losses and/or station crashes. All these algorithms have been formally described in LOTOS and verified using the CADP toolbox.

Conclusions: We pointed out that the algorithms proposed in [Lan77,CR79] were not complete and did not guarantee the uniqueness of the elected leader in a token-passing context where several elections can take place in sequence.

We proposed an enhanced version of a leader election algorithm that solves this problem and tolerates message losses and station crashes.

Using model-checking and bisimulation techniques, the verification of these non-trivial algorithms was carried out automatically for a fixed number of stations (three stations) [GM96].

Recently, the use of new compositional verification techniques allowed to verify the proposed fault-tolerant protocol with a larger number of stations (up to five or six stations) [KM97].

Publications:
[Lan77]
Gerard Le Lann. "Distributed Systems - Towards a Formal Approach". In B. Gilchrist, editor, Information Processing 77, pages 155-160. IFIP, North Holland, 1977.

[CR79]
Ernest Chang and Rosemary Roberts. "An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes". Communications of the ACM 22(5): 281-283, May 1979.

[GM96]
Hubert Garavel and Laurent Mounier. "Specification and verification of various distributed leader election algorithms for unidirectional ring networks". Science of Computer Programming, 1996. Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report RR-2986. Available on-line from the CADP Web site in : PDF or PostScript

[KM97]
Jean-Pierre Krimm and Laurent Mounier. "Compositional state space generation from LOTOS programs". In Ed Brinksma, editor, Proceedings of TACAS'97 (Tools and Algorithms for the Construction and Analysis of Systems), Enschede, The Netherlands, April 1997. Springer Verlag. Extended version with proofs available as Research Report VERIMAG RR97-01. Available on-line from http://cadp.inria.fr/publications/Garavel-Mounier-96.html
and from the CADP Web site in PDF or PostScript
Contact:
Hubert Garavel
INRIA Rhone-Alpes
655 avenue de l'Europe
38330 Montbonnot Saint Martin
FRANCE
Tel: +(33) 4 76 61 52 24
Fax: +(33) 4 76 61 52 52
E-mail : Hubert.Garavel@inria.fr
and
Laurent Mounier
VERIMAG
Centre Equation
2, avenue de Vignate
F-38610 Gieres
FRANCE
tel : +(33) 4 76 63 48 52
fax : +(33) 4 76 63 48 50
E-mail : Laurent.Mounier@imag.fr
Further remarks: The LOTOS sources as well as explanations on the verification with CADP are available on-line at : http://cadp.inria.fr/ftp/demos/demo_17

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Mon Apr 18 14:01:52 2022.

Back to the CADP case studies page