Mastering Simple Paxos: The Core Theory Behind Distributed Consensus

WeChat open‑source production‑grade Paxos library PhxPaxos; this article explains its foundation: Simple Paxos.

Open‑source address: https://github.com/tencent-wechat/phxpaxos

This article extracts parts of an internal WeChat PPT on Paxos and uses annotations to clarify the theoretical proof of Simple Paxos.

Why focus on Simple Paxos? It is the essence of Paxos and the cornerstone of all Paxos‑related algorithms. The article emphasizes the algorithmic derivation process rather than just its execution, because understanding the derivation is crucial to grasp each step’s meaning.

These PPT contents are largely cited from Lamport’s paper "The Part‑Time Parliament".

Page 1 Annotation The slide shows the three most important constraints of Paxos; mastering them means mastering Simple Paxos.

Page 2 Annotation Before formal explanation, return to the most primitive Paxos: three people in different cities each have a paper and a pen. They can write anything, but after stopping, we want all three to have identical content. This illustrates the simple problem of agreeing on a single value.

Page 3 Annotation Introduce the definition of a voting round. A proposal corresponds to the value to be agreed upon. Important definitions include the round identifier Bbal, the set of participants B, and the quorum Bqrm, which must exceed half of the participants.

Page 4 Annotation A single voting round cannot solve consistency because any participant may start a vote, leading to multiple rounds and potential conflicts. Multi‑round voting is introduced, with a distinct Greek‑letter Beta set for multi‑round votes.

Page 5 Annotation Introduce the crucial definition MaxVote, which links multiple voting rounds. MaxVote provides the highest‑numbered vote among those with identifiers smaller than the current round, allowing the current proposal to be derived from that vote.

Page 6 Annotation After all mathematical definitions, the three elegant constraints are presented: unique round numbers, quorum intersection (majority), and the third constraint that forces each new proposal to adopt the value of the highest prior accepted proposal, preventing conflicts.

Page 7 Annotation Shows the multi‑round voting process under the three constraints, highlighting how proposals evolve.

Page 8 Annotation Introduces a proof by contradiction to show that the final agreed proposal must be consistent.

Page 9 Annotation Simplifies the proof, demonstrating that a vote with identifier 3 cannot follow a successful vote with identifier 2 without violating the constraints.

Page 10 Annotation Explains the practical computation of MaxVote using a polling method: before each vote, query a majority of members for the highest prior vote with a smaller identifier.

Page 11 Annotation Notes that in real systems votes may arrive out of order, which can invalidate MaxVote if not handled, analogous to the Prepare‑Promise requirement in Paxos.

Page 12 Annotation To satisfy the constraints, MaxVote computation must be restricted, mirroring the Promise phase of Paxos.

Page 13 Annotation Shows the fully refined algorithm and maps each role in the algorithm to the concepts previously described.

Page 14 Annotation Formal algorithm process as presented in Lamport’s "Paxos Made Simple".

Page 15 Annotation A demonstration of the process.

Conclusion

Simple Paxos is challenging and requires repeated study; patient readers can master it. For implementation details, refer to the author’s previous articles and the full source code in the GitHub repository.

Click the original article to reach the GitHub address with the complete Paxos implementation source.

Follow the WeChat backend team: