You are here

Automated verification of randomised distributed algorithms

Team and supervisors
Department / Team: 
Team Web Site: 
http://www.irisa.fr/sumo/
PhD Director
Nathalie Bertrand
Co-director(s), co-supervisor(s)
Contact(s)
NameEmail addressPhone Number
Nathalie Bertrand
nathalie.bertrand@inria.fr
0299842281
PhD subject
Abstract

Randomisation is an elegant tool to design efficient algorithms or even to solve problems otherwise unsolvable, for distributed systems, where probabilities break symmetry between the participants. An example is the central problem of consensus for asynchronous message-passing systems, which admits no deterministic solution when
as few as one process can crash [FLP85], and for which Ben Or proposed a randomised solution [B83]. Despite the code simplicity of such randomised distributed algorithms, the literature only contains paper-and-pencil proofs of their correctness, or of their performances. However, as observed by Lehmann and Rabin: “proofs of correctness for probabilistic distributed systems are extremely slippery” [LH81]. Formal verification techniques can be extremely useful in this context: they would avoid tedious and error-prone manual proofs.

Since distributed algorithms are designed to run on systems composed of arbitrarily many agents, their automated verification is particularly challenging: one should validate at once all instances, independently of the parameterised number of participants. This falls under the name of parameterised verification [E14]. However, the
verification of parameterised probabilistic systems models is currently out-of-reach of state-of-the-art techniques and tools [KLVW17]. Building on parameterised verification and probabilistic model checking techniques, we propose to design a rigorous modelling framework, develop efficient algorithms, and implement them in a
verification platform, to demonstrate our techniques on real-life case studies.

See detailed description at people.rennes.inria.fr/Nathalie.Bertrand/Phd-rand-dist-algo.pdf

Bibliography

[B83] M. Ben Or. Another advantage of free choice: Completely asynchronous agreement protocols. In
Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed
Computing (PODC’83), pages 27–30. ACM, 1983.


[E14] J. Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Pro-
ceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS’14),
volume 25 of LIPIcs, pages 1–10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014.


[FLP85] M. J. Fischer, N. A. Lynch, and M. Paterson. Impossibility of distributed consensus with one faulty
process. Journal of the ACM, 32(2):374–382, 1985.


[KLVW17] I. Konnov, M. Lazic, H. Veith, and J. Widder. A short counterexample property for safety and live-
ness verification of fault-tolerant distributed algorithms. In Proceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages (POPL’17), pages 719–734. ACM, 2017.


[LR81] D. J. Lehmann and M. O. Rabin. On the advantages of free choice: A symmetric and fully distributed
solution to the dining philosophers problem. In Proceedings of the 8th Annual ACM Symposium on
Principles of Programming Languages (POPL’81), pages 133–138. ACM Press, 1981.

 

Work start date: 
septembre 2019
Keywords: 
formal methods, model checking, parameterized verification, probabilistic models, randomised distributed algorithms
Place: 
IRISA - Campus universitaire de Beaulieu, Rennes