On implementing and evaluating the raft distributed consensus algorithm

Abstract

The actor based model is a theoretical model stating that all possible computation can be expressed in terms of actors. An actor is a computational entity capable of (1) spawning other actors; (2) sending (asynchronous) messages to other actors; and (3) describing how to handle the receipt of a message. This model has inspired the creation of a number of programming languages, and in this project, I set out to study the efficacy such languages have on implementing consensus algorithms. A consensus algorithm is a distributed algorithm used to provide fault-tolerance by replicating an application's instructions over a multitude of servers. The fault-tolerance observed is the lack of deviation from the application's expected output, despite some of the replicated servers halting during the system's runtime. The algorithm I implement in this project is Raft - a consensus algorithm designed around understandability. I expand the process of creating a generic Raft implementation in Elixir (an actor based language), detailing my efforts in verifying the system to be correct. I conclude that actor based languages provide in-built functionalities which ease the development of consensus algorithms yet also introduce challenges to verifying their correctness. I find the most suitable verification technique to be runtime verification, a technique which involves translating invariants of the consensus algorithm into a specification language to synthesise a series of monitors. These monitors examine the trace of events experienced by the system during its runtime to determine whether an invariant has been violated. The challenges introduced by the actor model revolve around the limited visibility of an actor's internal state. I attempt to overcome these problems by inferring state changes through messages sent within the consensus cluster and by querying servers for snapshots of required information. This method is unsuccessful in translating all of the invariants into the specification language, however, yields positive results for four out of the five main invariants of Raft. The artefact I produce through this project is Graft - a generic Raft API written in Elixir. This interface allows for the set-up of custom cluster configurations and provides methods to concisely specify the operations Raft should replicate.