Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modelling the Raft Distributed Consensus Protocol in mCRL2

Parth Bora, Pham Duc Minh, Tim A. C. Willemse

TL;DR

A formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language is discussed.

Abstract

The consensus problem is a fundamental problem in distributed systems. It involves a set of actors, or entities, that need to agree on some values or decisions. The Raft algorithm is a solution to the consensus problem that has gained widespread popularity as an easy-to-understand and implement alternative to Lamport's Paxos algorithm. In this paper we discuss a formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language.

Modelling the Raft Distributed Consensus Protocol in mCRL2

TL;DR

A formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language is discussed.

Abstract

The consensus problem is a fundamental problem in distributed systems. It involves a set of actors, or entities, that need to agree on some values or decisions. The Raft algorithm is a solution to the consensus problem that has gained widespread popularity as an easy-to-understand and implement alternative to Lamport's Paxos algorithm. In this paper we discuss a formalisation of the Raft algorithm and its associated correctness properties in the mCRL2 specification language.
Paper Structure (18 sections, 1 figure, 1 table)

This paper contains 18 sections, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Outline.
  3. Modelling RAFT in mCRL2
  4. The Raft Environment
  5. Node
  6. The Raft State Machine.
  7. Log Replication.
  8. Model Statistics.
  9. Raft Properties
  10. Election Safety.
  11. Log Matching.
  12. Leader Completeness.
  13. State Machine Safety.
  14. Discussion
  15. Modelling in mCRL2.
  16. ...and 3 more sections

Figures (1)

  • Figure 1: State transitions for a node in Raft.