On the parallels between Paxos and Raft, and how to port optimizations

TL;DR

This paper formally maps the relationship between Paxos and Raft consensus algorithms and demonstrates how to automatically port optimizations from Paxos to Raft, ensuring correctness.

Contribution

It provides the first formal mapping between Paxos and Raft and introduces a method to port optimizations with correctness guarantees.

Findings

Successfully ported Mencius optimization to Raft

Ported Paxos Quorum Lease to Raft and evaluated performance

Established formal relationship between Paxos and Raft

Abstract

In recent years, Raft has overtaken Paxos as the consensus algorithm of choice. [53] While many have pointed out similarities between the two protocols, no one has formally mapped out their relationships. In this paper, we show how Raft and Paxos are formally related despite their surface differences. Based on the formal mapping between the two protocols, we show how to automatically port a certain class of optimizations from Paxos to Raft with guaranteed correctness. As case studies, we port and evaluate two optimizations, Mencius and Paxos Quorum Lease to Raft.