Quorum agreement and progress

A voter can crash after sending a reply. A message can arrive twice or arrive late. Paxos must preserve a chosen value through these events. The key is not that every voter always agrees; it is that a later successful proposer cannot choose a different value for the same slot.

The intersection fact

For $𝑁$ voters, a majority has size $𝑞=\lfloor \frac{𝑁}{2}\rfloor +1$. Any two majority sets ${𝑄}_1$ and ${𝑄}_2$ satisfy

The inequality follows because their union contains at most $𝑁$ voters. For three voters, every quorum has two members. Any pair of such quorums shares at least one.

Intersection alone is insufficient. The shared voter must retain its promise and accepted vote across a crash. It must also report that evidence during recovery.

Promises, votes and ballots

A ballot orders competing attempts. A proposer uses a unique higher ballot to recover a slot. An acceptor promises not to accept lower ballots and reports its accepted value and ballot, if any. Both promise and vote are durable facts.

A ballot must not propose two different values for one slot. An acceptor rejects conflicting values at one ballot and values below its applicable promise. The unique slot owner may use round zero; acceptors check this ownership rule. Round zero is not permission for another voter to skip recovery.

The agreement argument

Assume value $𝑣$ was chosen by quorum $𝑄$ at ballot $𝑏$. Consider a later successful prepare quorum ${𝑄}^{\prime }$. It intersects $𝑄$. At least one reply therefore contains a vote for $𝑣$ or a later accepted vote.

Why must that later vote also name $𝑣$? Induct over higher ballots. The first higher proposer that could obtain a quorum must carry forward the earlier accepted value. At each subsequent successful ballot, highest-vote selection carries the same value forward. A lower ballot cannot collect a new conflicting quorum after the higher promises: the quorums intersect again. Thus two chosen values for one slot must be equal.

This is an argument about protocol actions under durable, truthful acceptors. It does not prove that arbitrary code implements those actions. The model and implementation checks in Formal verification test that correspondence. Byzantine voters, lost durable identities and a device that reports a false successful synchronization violate the premises.

Progress is a different claim

Safety says conflicting choices do not occur. Progress says pending work eventually finishes. A network that drops every message can preserve safety forever while doing no useful work. SQLodin needs a surviving majority, eventual successful communication, fair scheduling and storage/application work that eventually completes.

For a finite offered frontier $ℎ$, consider the lowest unapplied slot $𝑠\le ℎ$:

1. A live owner proposes work or fills a required gap with a skip.
2. If the owner is absent, a surviving voter recovers the slot at a higher ballot.
3. Under an eventually non-preempted exchange, a majority chooses a value.
4. Learning and application advance the contiguous prefix.

The distance $ℎ-𝑎$ decreases as applied prefix $𝑎$ advances. Repeating the argument reaches $ℎ$. New arrivals create new frontiers; the argument does not promise an individual request freedom from starvation under perpetual interference or overload.

Healthy gap filling is event-driven. A regression advances the prefix with no timer ticks, guarding against the earlier 100 ms slot-selection delay. Missing-owner recovery still uses a failure detector: the default stall interval is ten 100 ms ticks. A timer is evidence that recovery should be attempted, not proof that a voter has failed.

See the composition argument for the mapping to upstream ownership, revocation, promise and acceptor functions.