Formal Specification of the Raft Consensus Algorithm

Organisation:	CONVECS project-team, Inria Grenoble Rhône Alpes and LIG, Grenoble (FRANCE)
Method:	LNT
Tools used:	DLC (Distributed LNT Compiler) CADP (Construction and Analysis of Distributed Processes)
Domain:	Fault Tolerance.
Period:	2014-2017
Size:	450 lines of LNT code
Description:	Consensus is a fundamental problem in fault-tolerant distributed systems, in particular in the context of replicated state machines (servers), which is a general approach to building fault-tolerant systems. The aim of consensus is to have the multiple servers agree on the same value even if some servers can fail, usually resorting to the election of a particular server taking the role of leader. Consensus algorithms are central in, e.g., large-scale cloud computing data management systems, such as the Apache project ZooKeeper or the Chubby lock service of Google. Raft ( http://raft.github.io ) is a recent consensus algorithm developed by Diego Ongaro and John Ousterhout at Stanford. In terms of fault-tolerance, it is functionally equivalent to the well-known Paxos algorithm designed by Leslie Lamport in 1998, with similar performance. However, while Paxos is quite intricate, Ongaro and Ousterhout claim that Raft is more understandable and easier to implement, as it is decomposed into relatively independent subproblems. As regards validation, Raft was specified formally in TLA+ and a correctness proof of Raft was made by its authors, although manually and without resorting to a proof assistant. In this work, Raft was chosen as an example to evaluate DLC (Distributed LNT Compiler, http://cadp.inria.fr/software/15-a-dlc.html ), a compiler from LNT formal models to distributed C code, developed at Inria Grenoble Rhône-Alpes. Starting from the TLA+ specification as reference, a formal model of Raft was written manually (available in Annex B of [Evrard-15]). The model consists of two parts: a parameterized LNT specification of a generic server (450 lines of LNT code, including types, functions, and server process) and an EXP composition expression representing parallel composition of multiple instances of the generic server. As every server can send messages to any other server, the parallel composition uses the 2-among-n synchronization operator.
Conclusions:	The LNT language was found convenient to model Raft. In particular, dynamic data types, such as lists, are very helpful to model, e.g., message buffers and server logs. The process of writing the LNT specification allowed to discover a bug in the TLA+ specification written by the authors of Raft. This error was signaled to the authors (see this message http://groups.google.com/forum/#!topic/raft-dev/yu-wOUx-gnA in the newsgroup dedicated to Raft development), who have corrected the TLA+ specification since then.
Publications:	[Evrard-Lang-15] Hugues Evrard and Frédéric Lang. "Automatic Distributed Code Generation from Formal Models of Asynchronous Concurrent Processes". Proceedings of the 23rd Euromicro International Conference on Parallel, Distributed and Network-based Processing, Special Session on Formal Approaches to Parallel and Distributed Systems PDP/4PAD'2015, IEEE, March 2015. Available on-line at: http://cadp.inria.fr/publications/Evrard-Lang-15.html or from the CADP Web site in PDF or PostScript [Evrard-15] Hugues Evrard. "Génération automatique d'implémentation distribuée à partir de modèles formels de processus concurrents asynchrones" (in French). PhD thesis of Grenoble University, July 2015. Available on-line at: https://tel.archives-ouvertes.fr/tel-01215634 or from the CADP Web site in PDF or PostScript [Evrard-Lang-17] Hugues Evrard and Frédéric Lang. "Automatic Distributed Code Generation from Formal Models of Asynchronous Processes Interacting by Multiway Rendezvous". In Journal of Logical and Algebraic Methods in Programming 88:121-153, Elsevier, 2017. Available on-line at: http://cadp.inria.fr/publications/Evrard-Lang-17.html or from the CADP Web site in PDF or PostScript [Evrard-20] Hugues Evrard. "Modeling the Raft Distributed Consensus Protocol in LNT". Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems MARS'2020 (Dublin, Ireland), Electronic Proceedings in Theoretical Computer Science vol. 316, pp. 15-39. Available on-line at: http://eptcs.web.cse.unsw.edu.au/paper.cgi?MARS2020.2 or from the CADP Web site in PDF or PostScript Slides of Hugues Evrard's invited talk at MARS 2022 in PDF
Contact:	Dr. Hugues Evrard Google UK, London Email: hevrard@google.com
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