2019/05/26 by Zhaoguo Wang, Wang, Zhaoguo, Changgeng Zhao +7 · 3 citations
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.DC
paper · pdf · doi:10.48550/arxiv.1905.10786
arxiv created 2019/05/26 · arxiv updated 2019/05/28
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.