Database of Case Studies Achieved Using CADP

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 our FTP 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 our FTP 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: https://hal.inria.fr/hal-01412911
or from our FTP site in PDF or PostScript
Contact:
Dr. Hugues Evrard
Inria Grenoble Rhône Alpes
CONVECS team
655, avenue de l'Europe
38330 Montbonnot
FRANCE
Tel: +33 (0)4 76 61 52 72
Email: Hugues.Evrard@inria.fr



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


Last modified: Mon Jun 19 11:53:39 2017.


Back to the CADP case studies page