Mastering Paxos: From Theory to Engineering in Large‑Scale Systems

Introduction

"Rather than predicting the future, limit the future" captures the core idea of the Paxos protocol. Paxos itself is simple; engineering it is the real challenge. This article, based on a WeChat engineer’s experience, revisits Paxos Made Simple, clarifies common misconceptions, and provides two proof methods.

Basic Concepts

Proposal Value: the value being proposed.

Proposal Number: a unique identifier that must not conflict.

Proposal: the combination of value and number.

Proposer: the entity that initiates proposals.

Acceptor: the entity that receives proposals.

Learner: the entity that learns the chosen value.

The proposer sends two types of requests: Prepare(n) and Accept(n, v) . Acceptors respond according to the protocol rules, and learners infer the final chosen value.

Protocol Process

Phase A (Prepare) : The proposer selects a proposal number n and broadcasts Prepare(n) to all acceptors.

Phase B (Promise) : An acceptor receiving Prepare(n) promises not to accept proposals with numbers lower than n and returns the highest-numbered proposal it has already accepted, if any.

Phase A (Accept) : After receiving promises from a majority, the proposer either proposes its own value v with number n (if no prior accepted value exists) or adopts the value from the highest-numbered accepted proposal.

Phase B (Accept) : An acceptor accepts the proposal if the proposal number does not violate any prior promise.

A common misunderstanding is that the proposer must send the Accept request only to acceptors that responded to Prepare; in fact, any majority can be targeted.

Protocol Proof

The core Paxos proposition states: if a proposal {n0, v0} is accepted by a majority, no later proposal {n1, v1} with n0 < n1 and v0 ≠ v1 can be accepted by a majority.

We strengthen this proposition stepwise, ultimately proving the original claim via mathematical induction and contradiction.

Inductive Proof : Assume proposal {m, v} is accepted by a majority. By induction on proposal numbers, any proposal {n, v} with n ≥ m must have value v . The base case n = m is trivial; the inductive step shows that if the claim holds for k, it also holds for k+1, using the intersection property of majorities.

Proof by Contradiction : Assume a later proposal {n1, v1} with n0 < n1 and v0 ≠ v1 is accepted. By protocol rules, an acceptor that promised for n1 must have previously accepted {n0, v0}. The proposer would then select the highest-numbered accepted value, which must be v0, contradicting v1 ≠ v0. Hence the proposition holds.

Learning Process

To determine the chosen value, collect all proposals accepted by each acceptor and identify the proposal accepted by a majority. The learner can also act as a proposer, issuing a new proposal and observing whether it is accepted by a majority.

It is crucial to focus on proposals, not just values, because a value may be accepted by multiple acceptors without being the chosen one.

Summary

The Paxos protocol limits future possibilities by ensuring that once a value is chosen, all subsequent decisions converge to the same value, guaranteeing consistency. Engineering Paxos at scale, such as in WeChat’s PaxosStore, involves handling billions of protocol executions per minute, with further work on massive flash storage and NewSQL solutions.