← The Books

The Part-Time Parliament

How can a group of machines agree on a sequence of commands when any of them may wander off at any time, and no one is in charge for long?

Lamport answered this himself, with the part-time legislators of the Greek island of Paxos. We present his paper as he wrote it, with interactive figures. It is the paper that inspired this entire project. Lamport ends it with the parliament's fall; the other books set that aside, and in them the parliament is still sitting.

After Leslie Lamport, The Part-Time Parliament, 1998 · Leslie Lamport, Paxos Made Simple, 2001

The Chamber of the Paxon Parliament seen from above its terrace, legislators with scrolls and messengers in blue walking in and out by its one door
Where this book sits
Draws on
This book retells
Leads to
  • How to Build a Highly Available System Using ConsensusLampson 1996
    • the algorithmfrom Lamport 1998The algorithm, explained for builders of systems.
  • Revisiting the Paxos AlgorithmDe Prisco, Lampson & Lynch 1997
    • the algorithmfrom Lamport 1998The algorithm, given a formal model and a timing analysis.
  • Practical Byzantine Fault ToleranceCastro & Liskov 1999 · Keeping Order Among Liars
    • overlapping quorumsfrom Lamport 1998Agreement on a sequence of commands by quorums that overlap, under a primary that can be replaced.
  • Flexible Paxos: Quorum Intersection RevisitedHoward, Malkhi & Spiegelman 2016
    • quorum overlapfrom Lamport 1998Majority quorums, relaxed: only the quorums of the two phases need to overlap.

Each link is an idea one paper took from another. Point at one, or tap it, to read how.

a paper this book retells a paper retold in another book a paper outside the series

First, in machine terms

Many computers, one log

A group of computers must keep the same log of commands, in the same order. That is easy until something fails, and two kinds of failure are always possible.

  • Machines stop and restart at any moment.
  • Messages may be slow, lost, or delivered twice.

Lamport's algorithm, Paxos, holds up under both. The logs never disagree, and whenever a majority of the machines is up and steady, new commands get through.

Lamport told it as the story of an ancient island parliament whose members would not stay in their seats. So will we.

Three machines, one log

Commands arrive. Every machine writes them in the same order.

Inside the Chamber: a round marble hall with one tall door, a checkerboard floor and legislators sitting along the wall with scrolls
The Chamber of the Paxon Parliament

A parliament whose members come and go

Paxos is an island of merchants, and trade comes before civic duty. Nobody will give a whole life to Parliament, so its legislators wander in and out of the round Chamber as their business allows.

One doorAnyone may leave through it at any moment, and stay away for any length of time.
A scroll eachNobody will stay in the Chamber to hold the record, so each legislator has a scroll of their own.
No podiumThe acoustics are poor and no speech carries, so legislators talk only through messengers.
What the Parliament must do

Settle the law, one numbered decree at a time

The law of Paxos is the sequence of decrees its Parliament has passed. Each legislator writes them into their own scroll, by number, in indelible ink that can never be changed. Two things are required of those scrolls.

Requirement one: consistency

No two scrolls may ever disagree. If one scroll says that decree 132 orders lamps to burn only olive oil, no other scroll may hold a different decree 132. A scroll may still hold nothing at 132, if its legislator has not yet heard that the decree was passed.

Wandering legislators put this in danger. See what happens when one group passes a decree and leaves, and a second group comes in knowing nothing of it.

Two groups, one number press the buttons in order

Three legislators are in the Chamber, with decree 37 before them. The other three are away.

Requirement two: progress

Consistency alone is easy to keep, since scrolls left blank never disagree. So Parliament requires progress as well. If a majority of the legislators stays in the Chamber for long enough, with nobody entering or leaving, then any decree proposed there is passed and reaches the scroll of everyone present.

Nobody can promise more than that, because no legislator will give up their business outside. The whole difficulty is to keep both requirements at once among people who may vanish in the middle of a vote. Before seeing how the Paxons managed it, we should know exactly what they had to work with.

The Chamber from its terrace, priests in white with red sashes strolling round the colonnade
What can go wrong

Everyone is honest, and anyone may be absent

Legislators and messengers on Paxos are scrupulously honest, and they follow the rules of Parliament to the letter. What none of them can be counted on to do is stay.

Parliament has to work under three facts.

A legislator holding up a sandglass beside another writing on a scroll

Memory walks out the door

A legislator who leaves the Chamber may forget what they were doing. Whatever must be remembered goes in the back of the scroll, in indelible ink. Lesser notes go on a slip of paper, which may be lost on the way out.

A messenger hands a note to a seated legislator while two more messengers cross the Chamber floor

Only messengers

Legislators speak to each other only through messengers. A messenger never garbles a message, but may forget having delivered it and deliver it again, or may set off on a long voyage and never deliver it at all.

Legislators sitting along the Chamber wall, each with a scroll

Prompt inside, anything outside

Inside the Chamber, messengers deliver at once and legislators answer promptly, and each legislator has a sandglass to tell how long that should take. Outside it, anything may take any length of time.

The messengers are the hardest of the three to plan for. Send a few messages across the Chamber and see what becomes of them.

Send a message try your luck

0delivered0delivered twice0never arrived

A message may arrive once, arrive twice, or never arrive.

A legislator who gets no answer cannot tell whether the messenger is slow or gone for good, and Parliament has to stay right without ever finding out. It can do so because of one fact that no amount of wandering undoes.

The one fact everything rests on

Any two majorities share a member

However the legislators wander, two majorities of the same Parliament can never be made up of entirely different people. Someone always sits in both.

That shared member carries what the first majority decided into the second, even when everyone else from the first has left. Here are seven legislators, seen from above the Chamber. Click any of them to send them out through the door or to call them back. Then let a majority pass a decree, and see who is still there when the next majority gathers.

Send some legislators out through the door first, if you like.
the one door

A smaller puzzle first

One decree, once every nineteen years

Parliament grew out of an older body. Every nineteen years a Synod of priests met to choose a single symbolic decree. When the priests too began wandering in and out of the Chamber, a Synod ended with no decree chosen.

The mathematicians who were asked to prevent a second such disaster had the priests choose by ballots. A ballot has a number, and it puts one decree to a chosen group of priests, its quorum. Each of them either votes for the decree or does not vote, and the ballot succeeds if every one of them votes. Any number of ballots may be held, and the decree of a successful one is the Synod's choice.

Three rules make sure that no two successful ballots ever choose different decrees.

RULE ONE

Every ballot has its own number

No two ballots share a number, so of any two it is always clear which is the later.

RULE TWO

Any two quorums share a priest

A quorum is always a majority of the priests, so whatever one quorum did, someone in the next quorum was there for it.

RULE THREE

A ballot carries the latest vote forward

If any priest in a ballot's quorum voted in an earlier ballot, the new ballot must be for the decree of the latest of those earlier ballots.

The third rule is the hard one, and a Paxon manuscript shows it at work. The manuscript lists five ballots held among the five priests Α, Β, Γ, Δ and Ε.

The manuscript click a ballot

Each row is one ballot, with its number, its decree and its quorum. A boxed priest is one who voted. Click a ballot to see whether it was free to choose its decree or had to copy an earlier one, and from whom.

BallotDecreeQuorum
Try ballot 27.

Together the rules do what was asked of them. Once a ballot has succeeded, the quorum of every later ballot holds a priest who voted in it, and the third rule hands its decree on to each later ballot in turn. So any two successful ballots are for the same decree, and no two scrolls can disagree.

What remains is to turn the rules into steps that a priest can follow.

The three rules, formally · and the proofs that they give consistency

Each ballot B has a number Bbal, a decree Bdec, a quorum Bqrm and a set of voters Bvot, and ℬ is a set of ballots. The three rules are the conditions B1(ℬ), B2(ℬ) and B3(ℬ). A ballot is successful when Bqrm ⊆ Bvot.

To state B1(ℬ)–B3(ℬ) formally requires some more notation. A vote v was defined to be a quantity consisting of three components: a priest vpst, a ballot number vbal, and a decree vdec. It represents a vote cast by priest vpst for decree vdec in ballot number vbal. The Paxons also defined null votes to be votes v with vbal = −∞ and vdec = blank, where −∞ < b < ∞ for any ballot number b, and blank is not a decree. For any priest p, they defined nullp to be the unique null vote v with vpst = p.

Paxon mathematicians defined a total ordering on the set of all votes, but part of the manuscript containing the definition has been lost. The remaining fragment indicates that, for any votes v and v′, if vbal < v′bal then v < v′. It is not known how the relative order of v and v′ was defined if vbal = v′bal.

For any set ℬ of ballots, the set Votes(ℬ) of votes in ℬ was defined to consist of all votes v such that vpst ∈ Bvot, vbal = Bbal, and vdec = Bdec for some B ∈ ℬ. If p is a priest and b is either a ballot number or ±∞, then MaxVote(b, p, ℬ) was defined to be the largest vote v in Votes(ℬ) cast by p with vbal < b, or to be nullp if there was no such vote. Since nullp is smaller than any real vote cast by p, this means that MaxVote(b, p, ℬ) is the largest vote in the set

{v ∈ Votes(ℬ) : (vpst = p) ∧ (vbal < b)} ∪ {nullp}

For any nonempty set Q of priests, MaxVote(b, Q, ℬ) was defined to equal the maximum of all votes MaxVote(b, p, ℬ) with p in Q.
Conditions B1(ℬ)–B3(ℬ) are stated formally as follows.8

B1(ℬ) ≜ ∀B, B′ ∈ ℬ : (B ≠ B′) ⇒ (Bbal ≠ B′bal)
B2(ℬ) ≜ ∀B, B′ ∈ ℬ : Bqrm ∩ B′qrm ≠ ∅
B3(ℬ) ≜ ∀B ∈ ℬ : (MaxVote(Bbal, Bqrm, ℬ)bal ≠ −∞) ⇒ (Bdec = MaxVote(Bbal, Bqrm, ℬ)dec)

Although the definition of MaxVote depends upon the ordering of votes, B1(ℬ) implies that MaxVote(b, Q, ℬ)dec is independent of how votes with equal ballot numbers were ordered.

8. I use the Paxon mathematical symbol ≜, which meant equals by definition.

To show that these conditions imply consistency, the Paxons first showed that B1(ℬ)–B3(ℬ) imply that, if a ballot B in ℬ is successful, then any later ballot in ℬ is for the same decree as B.

Lemma

If B1(ℬ), B2(ℬ), and B3(ℬ) hold, then

((Bqrm ⊆ Bvot) ∧ (B′bal > Bbal)) ⇒ (B′dec = Bdec)

for any B, B′ in ℬ.

Proof of Lemma

For any ballot B in ℬ, let Ψ(B, ℬ) be the set of ballots in ℬ later than B for a decree different from B’s:

Ψ(B, ℬ) ≜ {B′ ∈ ℬ : (B′bal > Bbal) ∧ (B′dec ≠ Bdec)}

To prove the lemma, it suffices to show that if Bqrm ⊆ Bvot then Ψ(B, ℬ) is empty. The Paxons gave a proof by contradiction. They assumed the existence of a B with Bqrm ⊆ Bvot and Ψ(B, ℬ) ≠ ∅, and obtained a contradiction as follows.9

  1. Choose C ∈ Ψ(B, ℬ) such that Cbal = min{B′bal : B′ ∈ Ψ(B, ℬ)}.
    Proof: C exists because Ψ(B, ℬ) is nonempty and finite.
  2. Cbal > Bbal
    Proof: By 1 and the definition of Ψ(B, ℬ).
  3. Bvot ∩ Cqrm ≠ ∅
    Proof: By B2(ℬ) and the hypothesis that Bqrm ⊆ Bvot.
  4. MaxVote(Cbal, Cqrm, ℬ)bal ≥ Bbal
    Proof: By 2, 3 and the definition of MaxVote(Cbal, Cqrm, ℬ).
  5. MaxVote(Cbal, Cqrm, ℬ) ∈ Votes(ℬ)
    Proof: By 4 (which implies that MaxVote(Cbal, Cqrm, ℬ) is not a null vote) and the definition of MaxVote(Cbal, Cqrm, ℬ).
  6. MaxVote(Cbal, Cqrm, ℬ)dec = Cdec.
    Proof: By 5 and B3(ℬ).
  7. MaxVote(Cbal, Cqrm, ℬ)dec ≠ Bdec
    Proof: By 6, 1, and the definition of Ψ(B, ℬ).
  8. MaxVote(Cbal, Cqrm, ℬ)bal > Bbal
    Proof: By 4, since 7 and B1(ℬ) imply that MaxVote(Cbal, Cqrm, ℬ)bal ≠ Bbal.
  9. MaxVote(Cbal, Cqrm, ℬ) ∈ Votes(Ψ(B, ℬ))
    Proof: By 7, 8, and the definition of Ψ(B, ℬ).
  10. MaxVote(Cbal, Cqrm, ℬ)bal < Cbal
    Proof: By definition of MaxVote(Cbal, Cqrm, ℬ).
  11. Contradiction
    Proof: By 9, 10, and 1.

End Proof of Lemma

9. Paxon mathematicians always provided careful, structured proofs of important theorems. They were not as sophisticated as modern mathematicians, who can omit many details and write paragraph-style proofs without ever making a mistake.

With this lemma, it was easy to show that, if B1–B3 hold, then any two successful ballots are for the same decree.

Theorem 1

If B1(ℬ), B2(ℬ), and B3(ℬ) hold, then

((Bqrm ⊆ Bvot) ∧ (B′qrm ⊆ B′vot)) ⇒ (B′dec = Bdec)

for any B, B′ in ℬ.

Proof of Theorem

If B′bal = Bbal, then B1(ℬ) implies B′ = B. If B′bal ≠ Bbal, then the theorem follows immediately from the lemma. End Proof of Theorem

The Paxons then proved a theorem asserting that if there are enough priests in the Chamber, then it is possible to conduct a successful ballot while preserving B1–B3. Although this does not guarantee progress, it at least shows that a balloting protocol based on B1–B3 will not deadlock.

Theorem 2

Let b be a ballot number and Q a set of priests such that b > Bbal and Q ∩ Bqrm ≠ ∅ for all B ∈ ℬ. If B1(ℬ), B2(ℬ), and B3(ℬ) hold, then there is a ballot B′ with B′bal = b and B′qrm = B′vot = Q such that B1(ℬ ∪ {B′}), B2(ℬ ∪ {B′}), and B3(ℬ ∪ {B′}) hold.

Proof of Theorem

Condition B1(ℬ ∪ {B′}) follows from B1(ℬ), the choice of B′bal, and the assumption about b. Condition B2(ℬ ∪ {B′}) follows from B2(ℬ), the choice of B′qrm, and the assumption about Q. If MaxVote(b, Q, ℬ)bal = −∞ then let B′dec be any decree, else let it equal MaxVote(b, Q, ℬ)dec. Condition B3(ℬ ∪ {B′}) then follows from B3(ℬ). End Proof of Theorem

The rules as steps

One ballot, step by step

A priest who wants a decree chosen starts a ballot, and the three rules settle what each step must be. Here priest Α runs ballot 27 among the five priests. Scroll slowly, and the picture moves with you.

1 · Choose

Pick a fresh number and a quorum

Α starts the ballot. Α picks the number 27, which no ballot has used, and a quorum of three: Α, Γ and Δ. Β and Ε sit this one out.

2 · Ask

A question, with a price

Α sends the quorum one message: “Tell me the latest vote you ever cast, and promise never to vote in any ballot numbered below this one.”

3 · Promise

Each answers, and promises

Each member writes the promise in the back of their scroll, in indelible ink, and replies with the latest vote they have cast, or with none.

4 · Look back

Α now holds a fact about the past

Γ last voted in ballot 5 and Δ in ballot 2. Α has never voted. The latest of these is ballot 5, so the third rule leaves Α no choice: ballot 27 must be for that ballot's decree, β. Α could have chosen freely only if nobody in the quorum had ever voted.

5 · Propose

“Vote for this, in this ballot”

Α sends decree β to the quorum and asks for their votes in ballot 27.

6 · Vote

Unless they promised something higher

Each member votes, unless they have since promised a higher ballot. They note the vote in the back of their scroll and report it to Α.

7 · Done

Every member voted, so the ballot succeeded

Α writes β in their scroll as the Synod's decree and sends word to every priest, in the quorum or out of it. Whoever hears writes it down too.

Every step is something a priest may do, and none is something a priest must do. A priest who walks out, or a messenger who never arrives, only leaves a step undone, and a step left undone cannot break any of the three rules. A message delivered twice only repeats a step, and the second time it changes nothing. So the scrolls stay consistent whatever goes wrong.

Appendix · proof of consistency of the Synod's protocol

The one-ballot protocol above, stated as the actions a priest may take, with the invariant those actions maintain and its proof.

A1 · The Basic Protocol

The Synod’s basic protocol, described informally above, is stated here using modern algorithmic notation. We begin with the variables that a priest p must maintain. First come the variables that represent information kept in his ledger. (For convenience, a priest's previous vote is kept as its two components prevBal[p] and prevDec[p].)

Ledger variables

outcome[p] — The decree written in p’s ledger, or blank if there is nothing written there yet.

lastTried[p] — The number of the last ballot that p tried to begin, or −∞ if there was none.

prevBal[p] — The number of the last ballot in which p voted, or −∞ if he never voted.

prevDec[p] — The decree for which p last voted, or blank if p never voted.

nextBal[p] — The number of the last ballot in which p agreed to participate, or −∞ if he has never agreed to participate in a ballot.

Next come variables representing information that priest p could keep on a slip of paper:

Slip-of-paper variables

status[p] — One of the following values:
  idle — Not conducting or trying to begin a ballot
  trying — Trying to begin ballot number lastTried[p]
  polling — Now conducting ballot number lastTried[p]
If p has lost his slip of paper, then status[p] is assumed to equal idle and the values of the following four variables are irrelevant.

prevVotes[p] — The set of votes received in LastVote messages for the current ballot (the one with ballot number lastTried[p]).

quorum[p] — If status[p] = polling, then the set of priests forming the quorum of the current ballot; otherwise, meaningless.

voters[p] — If status[p] = polling, then the set of quorum members from whom p has received Voted messages in the current ballot; otherwise, meaningless.

decree[p] — If status[p] = polling, then the decree of the current ballot; otherwise, meaningless.

There is also the history variable ℬ, which is the set of ballots that have been started and their progress—namely, which priests have cast votes. (A history variable is one used in the development and proof of an algorithm, but not actually implemented.)

Next come the actions that priest p may take. These actions are assumed to be atomic, meaning that once an action is begun, it must be completed before priest p begins any other action. An action is described by an enabling condition and a list of effects. The enabling condition describes when the action can be performed; actions that receive a message are enabled whenever a messenger has arrived with the appropriate message. The list of effects describes how the action changes the algorithm’s variables and what message, if any, it sends. (Each individual action sends at most one message.)

Recall that ballot numbers were partitioned among the priests. For any ballot number b, the Paxons defined owner(b) to be the priest who was allowed to use that ballot number.

The actions in the basic protocol are allowed actions; the protocol does not require that a priest ever do anything. No attempt at efficiency has been made; the actions allow p to do silly things, such as sending another BeginBallot message to a priest from whom he has already received a LastVote message.

The actions of the basic protocol

Try New Ballot
Always enabled.
– Set lastTried[p] to any ballot number b, greater than its previous value, such that owner(b) = p.
– Set status[p] to trying.
– Set prevVotes[p] to ∅.

Send NextBallot Message
Enabled whenever status[p] = trying.
– Send a NextBallot(lastTried[p]) message to any priest.

Receive NextBallot(b) Message
If b ≥ nextBal[p] then
– Set nextBal[p] to b.

Send LastVote Message
Enabled whenever nextBal[p] > prevBal[p].
– Send a LastVote(nextBal[p], v) message to priest owner(nextBal[p]), where vpst = p, vbal = prevBal[p], and vdec = prevDec[p].

Receive LastVote(b, v) Message
If b = lastTried[p] and status[p] = trying, then
– Set prevVotes[p] to the union of its original value and {v}.

Start Polling Majority Set Q
Enabled when status[p] = trying and Q ⊆ {vpst : v ∈ prevVotes[p]}, where Q is a majority set.
– Set status[p] to polling.
– Set quorum[p] to Q.
– Set voters[p] to ∅.
– Set decree[p] to a decree d chosen as follows: Let v be the maximum element of prevVotes[p]. If vbal ≠ −∞ then d = vdec, else d can equal any decree.
– Set ℬ to the union of its former value and {B}, where Bdec = d, Bqrm = Q, Bvot = ∅, and Bbal = lastTried[p].

Send BeginBallot Message
Enabled when status[p] = polling.
– Send a BeginBallot(lastTried[p], decree[p]) message to any priest in quorum[p].

Receive BeginBallot(b, d) Message
If b = nextBal[p] > prevBal[p] then
– Set prevBal[p] to b.
– Set prevDec[p] to d.
– If there is a ballot B in ℬ with Bbal = b [there will be], then choose any such B [there will be only one] and let the new value of ℬ be obtained from its old value by setting Bvot equal to the union of its old value and {p}.

Send Voted Message
Enabled whenever prevBal[p] ≠ −∞.
– Send a Voted(prevBal[p], p) message to owner(prevBal[p]).

Receive Voted(b, q) Message
If b = lastTried[p] and status[p] = polling, then
– Set voters[p] to the union of its old value and {q}

Succeed
Enabled whenever status[p] = polling, quorum[p] ⊆ voters[p], and outcome[p] = blank.
– Set outcome[p] to decree[p].

Send Success Message
Enabled whenever outcome[p] ≠ blank.
– Send a Success(outcome[p]) message to any priest.

Receive Success(d) Message
If outcome[p] = blank, then
– Set outcome[p] to d.

This algorithm is an abstract description of the real protocol performed by Paxon priests. Do the algorithm’s actions accurately model the actions of the real priests? There were three kinds of actions that a priest could perform “atomically”: receiving a message, writing a note or ledger entry, and sending a message. Each of these is represented by a single action of the algorithm, except that Receive actions both receive a message and set a variable. We can pretend that the receipt of a message occurred when a priest acted upon the message; if he left the Chamber before acting upon it, then we can pretend that the message was never received. Since this pretense does not affect the consistency condition, we can infer the consistency of the basic Synod protocol from the consistency of the algorithm.

A2 · Proof of Consistency

To prove the consistency condition, it is necessary to show that whenever outcome[p] and outcome[q] are both different from blank, they are equal. A rigorous correctness proof requires a complete description of the algorithm. The description given above is almost complete. Missing is a variable ℳ whose value is the multiset of all messages in transit.15 Each Send action adds a message to this multiset and each Receive action removes one. Also needed are actions to represent the loss and duplication of messages, as well as a Forget action that represents a priest losing his slip of paper.

With these additions, we get an algorithm that defines a set of possible behaviors, in which each change of state corresponds to one of the allowed actions. The Paxons proved correctness by finding a predicate I such that

  1. I is true initially.
  2. I implies the desired correctness condition.
  3. Each allowed action leaves I true.

The predicate I was written as a conjunction I1 ∧ ... ∧ I7, where I1–I5 were in turn the conjunction of predicates I1(p)–I5(p) for all priests p. Although most variables are mentioned in several of the conjuncts, each variable except status[p] is naturally associated with one conjunct, and each conjunct can be thought of as a constraint on its associated variables. The definitions of the individual conjuncts of I are given below, where a list of items marked by ∧ symbols denotes the conjunction of those items. The variables associated with a conjunct are listed in bracketed comments.

15. A multiset is a set that may contain multiple copies of the same element.

The invariant I, in full
I1(p) ≜ [Associated variable: outcome[p]]
(outcome[p] ≠ blank) ⇒ ∃B ∈ ℬ : (Bqrm ⊆ Bvot) ∧ (Bdec = outcome[p])
I2(p) ≜ [Associated variable: lastTried[p]]
∧ owner(lastTried[p]) = p
∧ ∀B ∈ ℬ : (owner(Bbal) = p) ⇒
    ∧ Bbal ≤ lastTried[p]
    ∧ (status[p] = trying) ⇒ (Bbal < lastTried[p])
I3(p) ≜ [Associated variables: prevBal[p], prevDec[p], nextBal[p]]
∧ prevBal[p] = MaxVote(∞, p, ℬ)bal
∧ prevDec[p] = MaxVote(∞, p, ℬ)dec
∧ nextBal[p] ≥ prevBal[p]
I4(p) ≜ [Associated variable: prevVotes[p]]
(status[p] ≠ idle) ⇒ ∀v ∈ prevVotes[p] :
    ∧ v = MaxVote(lastTried[p], vpst, ℬ)
    ∧ nextBal[vpst] ≥ lastTried[p]
I5(p) ≜ [Associated variables: quorum[p], voters[p], decree[p]]
(status[p] = polling) ⇒
    ∧ quorum[p] ⊆ {vpst : v ∈ prevVotes[p]}
    ∧ ∃B ∈ ℬ : ∧ quorum[p] = Bqrm ∧ decree[p] = Bdec
                  ∧ voters[p] ⊆ Bvot ∧ lastTried[p] = Bbal
I6 ≜ [Associated variable: ℬ]
∧ B1(ℬ) ∧ B2(ℬ) ∧ B3(ℬ)
∧ ∀B ∈ ℬ : Bqrm is a majority set
I7 ≜ [Associated variable: ℳ]
∧ ∀NextBallot(b) ∈ ℳ : (b ≤ lastTried[owner(b)])
∧ ∀LastVote(b, v) ∈ ℳ : ∧ v = MaxVote(b, vpst, ℬ) ∧ nextBal[vpst] ≥ b
∧ ∀BeginBallot(b, d) ∈ ℳ : ∃B ∈ ℬ : (Bbal = b) ∧ (Bdec = d)
∧ ∀Voted(b, p) ∈ ℳ : ∃B ∈ ℬ : (Bbal = b) ∧ (p ∈ Bvot)
∧ ∀Success(d) ∈ ℳ : ∃p : outcome[p] = d ≠ blank

The Paxons had to prove that I satisfies the three conditions given above. The first condition, that I holds initially, requires checking that each conjunct is true for the initial values of all the variables. While not stated explicitly, these initial values can be inferred from the variables’ descriptions, and checking the first condition is straightforward. The second condition, that I implies consistency, follows from I1, the first conjunct of I6, and Theorem 1. The hard part was proving the third condition, the invariance of I, which meant proving that I is left true by every action. This condition is proved by showing that, for each conjunct of I, executing any action when I is true leaves that conjunct true. The proofs are sketched below.

The proofs, conjunct by conjunct

I1(p) — ℬ is changed only by adding a new ballot or adding a new priest to Bvot for some B ∈ ℬ, neither of which can falsify I1(p). The value of outcome[p] is changed only by the Succeed and Receive Success Message actions. The enabling condition and I5(p) imply that I1(p) is left true by the Succeed action. The enabling condition, I1(p), and the last conjunct of I7 imply that I1(p) is left true by the Receive Success Message action.

I2(p) — This conjunct depends only on lastTried[p], status[p], and ℬ. Only the Try New Ballot action changes lastTried[p], and only that action can set status[p] to trying. Since the action increases lastTried[p] to a value b with owner(b) = p, it leaves I2(p) true. A completely new element is added to ℬ only by a Start Polling action; the first conjunct of I2(p) and the specification of the action imply that adding this new element does not falsify the second conjunct of I2(p). The only other way ℬ is changed is by adding a new priest to Bvot for some B ∈ ℬ, which does not affect I2(p).

I3(p) — Since votes are never removed from ℬ, the only action that can change MaxVote(∞, p, ℬ) is one that adds to ℬ a vote cast by p. Only a Receive BeginBallot Message action can do that, and only that action changes prevBal[p] and prevDec[p]. The BeginBallot conjunct of I7 implies that this action actually does add a vote to ℬ, and B1(ℬ) (the first conjunct of I6) implies that there is only one ballot to which the vote can be added. The enabling condition, the assumption that I3(p) holds before executing the action, and the definition of MaxVote then imply that the action leaves the first two conjuncts of I3(p) true. The third conjunct is left true because prevBal[p] is changed only by setting it to nextBal[p], and nextBal[p] is never decreased.

I4(p) — This conjunct depends only upon the values of status[p], prevVotes[p], lastTried[p], nextBal[q] for some priests q, and ℬ. The value of status[p] is changed from idle to not idle only by a Try New Ballot action, which sets prevVotes[p] to ∅, making I4(p) vacuously true. The only other actions that change prevVotes[p] are the Forget action, which leaves I4(p) true because it sets status[p] to idle, and the Receive LastVote Message action. It follows from the enabling condition and the LastVote conjunct of I7 that the Receive LastVote Message action preserves I4(p). The value of lastTried[p] is changed only by the Try New Ballot action, which leaves I4(p) true because it sets status[p] to trying. The value of nextBal[q] can only increase, which cannot make I4(p) false. Finally, MaxVote(lastTried[p], vpst, ℬ) can be changed only if vpst is added to Bvot for some B ∈ ℬ with Bbal < lastTried[p]. But vpst is added to Bvot (by a Receive BeginBallot Message action) only if nextBal[vpst] = Bbal, in which case I4(p) implies that Bbal ≥ lastTried[p].

I5(p) — The value of status[p] is set to polling only by the Start Polling action. This action’s enabling condition guarantees that the first conjunct becomes true, and it adds the ballot to ℬ that makes the second conjunct true. No other action changes quorum[p], decree[p], or lastTried[p] while leaving status[p] equal to polling. The value of prevVotes[p] cannot be changed while status[p] = polling, and ℬ is changed only by adding new elements or by adding a new priest to Bvot. The only remaining possibility for falsifying I5(p) is the addition of a new element to voters[p] by the Receive Voted Message action. The Voted conjunct of I7, B1(ℬ) (the first conjunct of I6), and the action’s enabling condition imply that the element added to voters[p] is in Bvot, where B is the ballot whose existence is asserted in I5(p).

I6 — Since Bbal and Bqrm are never changed for any B ∈ ℬ, the only way B1(ℬ), B2(ℬ), and the second conjunct of I6 can be falsified is by adding a new ballot to ℬ, which is done only by the Start Polling Majority Set Q action when status[p] equals trying. It follows from the second conjunct of I2(p) that this action leaves B1(ℬ) true; and the assertion, in the enabling condition, that Q is a majority set implies that the action leaves B2(ℬ) and the second conjunct of I6 true. There are two possible ways of falsifying B3(ℬ): changing MaxVote(Bbal, Bqrm, ℬ) by adding a new vote to ℬ, and adding a new ballot to ℬ. A new vote is added only by the Receive BeginBallot Message action, and I3(p) implies that the action adds a vote later than any other vote cast by p in ℬ, so it cannot change MaxVote(Bbal, Bqrm, ℬ) for any B in ℬ. Conjunct I4(p) implies that the new ballot added by the Start Polling action does not falsify B3(ℬ).

I7 — I7 can be falsified either by adding a new message to ℳ or by changing the value of another variable on which I7 depends. Since lastTried[p] and nextBal[p] are never decreased, changing them cannot make I7 false. Since outcome[p] is never changed if its value is not blank, changing it cannot falsify I7. Since ℬ is changed only by adding ballots and adding votes, the only change to it that can make I7 false is the addition of a vote by vpst that makes the LastVote(b, v) conjunct false by changing MaxVote(b, vpst, ℬ). This can happen only if vpst votes in a ballot B with Bbal < b. But vpst can vote only in ballot number nextBal[vpst], and the assumption that this conjunct holds initially implies that nextBal[vpst] ≥ b. Therefore, we need check only that every message that is sent satisfies the condition in the appropriate conjunct of I7.

NextBallot: Follows from the definition of the Send NextBallot Message action and the first conjunct of I2(p).

LastVote: The enabling condition of the Send LastVote Message action and I3(p) imply that MaxVote(nextBal[p], p, ℬ) = MaxVote(∞, p, ℬ), from which it follows that the LastVote message sent by the action satisfies the condition in I7.

BeginBallot: Follows from I5(p) and the definition of the Send BeginBallot Message action.

Voted: Follows from I3(p), the definition of MaxVote, and the definition of the Send Voted Message action.

Success: Follows from the definition of Send Success Message.

Safe is not enough

Too many ballots block everything

The steps keep the scrolls consistent, but nothing in them makes any priest start a ballot. With no ballots, no decree is ever chosen. With too many, no decree is chosen either.

The trouble lies in the promise. Each new ballot has its quorum promise never to vote in a lower one, so a ballot started too soon dooms the one before it. Let two priests each believe they are the one to start ballots, and each keeps starting a higher one before the other's can finish.

Two would-be presidents no one is in charge

0decrees passed
0highest ballot started

The Paxons' cure was a president: one priest who alone starts ballots, and who starts a new one only when the last has had time to succeed. Most governments find a president hard to choose, because two at once would be a disaster. In the Synod, two presidents can only slow things down. They can never make the scrolls disagree, because consistency never depended on who starts the ballots.

From one decree to a whole law

A separate Synod for every number

Parliament has to pass a long series of numbered decrees, where the Synod chose only one. It treats each number as a small Synod of its own, and lets one president run them all.

A newly made president sitting on the stone seat copying decrees onto a scroll while others wait

Anyone who wants a decree passed tells the president, who gives it the next free number and holds a ballot for it. The saving comes at the start. A president does not choose a decree until the quorum has answered, so a new president can ask the opening question once, for every number still open. Each legislator answers once too, with what they have voted for and with any later decrees already in their scroll.

What those answers can hold is best seen on a Monday morning, after everyone has been home for the weekend. Press the buttons in order.

The president's scroll newly appointed

Decrees 122 to 124 are known to everyone. Press the first button.

With a president settled and nobody coming or going, the opening question need not be asked again. Each new decree then takes three steps: the president asks a quorum to vote, the quorum votes, and the president announces the result.

Years of practice

Governing the island asked for more

Running Paxos turned out to be harder than passing decrees in order. Three incidents each changed the way Parliament worked.

A president copying decrees onto a scroll

Better presidents

At first the president was whoever stood last in the alphabet among those in the Chamber. One legislator came back from six months away and was made president at once, and Parliament stopped while the new president copied out six months of decrees. A president who was already up to date would have spared everyone the wait.

Two inspectors giving conflicting verdicts on the same lot of cheese in the town square

One office, one holder

Parliament replaced a strict cheese inspector, who did not hear of it for some time. Meanwhile two inspectors gave conflicting verdicts on the same cheese. Every decree now carries the time it was proposed and every post runs for a fixed term, so a post has at most one holder at a time.

A legislator whose scroll stops at decree 76 advises a buyer about black goats

Don't ask one scroll

Decree 77 made it legal to sell black goats. A buyer asked a legislator who had been out of the Chamber, whose scroll stopped at decree 76, and was told the sale was illegal. Since then, a question about the law never returns an older state of it than an earlier question did.

Two more changes came with the years, and neither needed anything new.

Scrolls grew too long fold one

Current law + number of the last decree

As the decrees piled up, finding the current olive tax meant reading through years of them. The scrolls were cut down to the law as it now stands, with the number of the last decree it includes.

Members by decree and scrolls put right

Legislators came to be added and removed by decree. Old decrees were also passed again from time to time, so that a scroll that had gone wrong would be put right.

Both are the same ballot as before, applied to the list of members and to the scrolls themselves.

Why one office has one holder

A decree carries the time it was proposed. That is safe because of a property of the parliamentary protocol, stated here with its proof.

If two decrees are passed by different presidents, then one of the presidents proposed his decree after learning that the other decree had been proposed.

Why the property holds

To see that this property is satisfied, suppose that ballot number b was successful for decree D, ballot number b′ was successful for decree D′, and b < b′. Let q be a legislator who voted in both ballots. The balloting for D′ began with a NextBallot(b′, n) message. If the sender of that message did not already know about D, then n is less than the decree number of D, and q’s reply to the NextBallot message must state that he voted for D.

Back to machines

The island was a replicated service

Read the island again with machines in the legislators' seats. Each server holds its own copy of one log of commands, as each legislator has a scroll, and a command enters the log the way a decree is passed. Hover over a row, or tap it, to see who is who.

On the island
In the machine room

The protocol never lets two logs disagree, however machines come and go.

It makes progress whenever a majority is present and steady for long enough. It never gives up safety, and asks for progress only once things settle.

Its ballot protocol lives on as Paxos, the foundation of modern fault-tolerant distributed computing.

The Chamber, in detail All the papers

Setting The Chamber

The paper and its references

Leslie Lamport, “The Part-Time Parliament,” ACM Transactions on Computer Systems 16, 2 (May 1998), 133–169. Received January 1990; accepted March 1998. The referees wanted the Paxos story removed, the author declined, and the paper sat unpublished for eight years.

  1. Bernstein, P. A., Hadzilacos, V., and Goodman, N. 1987. Concurrency Control and Recovery in Database Systems. Addison-Wesley, Reading, Massachusetts.
  2. De Prisco, R., Lampson, B., and Lynch, N. 1997. Revisiting the Paxos algorithm. In M. Mavronicolas and P. Tsigas (Eds.), Proceedings of the 11th International Workshop on Distributed Algorithms (WDAG 97), Volume 1320 of Lecture Notes in Computer Science, Saarbruken, Germany, pp. 111–125. Springer-Verlag.
  3. Dijkstra, E. W. 1974. Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 11 (Nov.), 643–644.
  4. Dwork, C., Lynch, N., and Stockmeyer, L. 1988. Consensus in the presence of partial synchrony. Journal of the ACM 35, 2 (April), 288–323.
  5. Fekete, A., Lynch, N., and Shvartsman, A. 1997. Specifying and using a partitionable group communication service. In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, pp. 53–62. ACM Press.
  6. Fischer, M. J., Lynch, N., and Paterson, M. S. 1985. Impossibility of distributed consensus with one faulty process. Journal of the ACM 32, 2 (April), 374–382.
  7. Gray, C. G. and Cheriton, D. R. 1989. Leases: An efficient fault-toerant mechanism for distributed file cache consistency. In Proceedings of the Twelfth ACM Symposium on Operating Systems Principles, New York, pp. 202–210. ACM.
  8. Keidar, I. and Dolev, D. 1996. Efficient message ordering in dynamic networks. In Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing. ACM.
  9. Ladin, R., Liskov, B., Shrira, L., and Ghemawat, S. 1992. Providing high availability using lazy replication. ACM Transactions on Computer Systems 10, 4 (Nov.), 360–391.
  10. Lamport, L. 1978. Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 7 (July), 558–565.
  11. Lamport, L. 1984. Using time instead of timeout for fault-tolerant distributed systems. ACM Trans. on Programm. Lang. Syst. 6, 2 (April), 254–280.
  12. Lampson, B. W. 1996. How to build a highly available system using consensus. In O. Babaoglu and K. Marzullo (Eds.), Distributed Algorithms, Volume 1151 of Lecture Notes in Computer Science, Berlin, pp. 1–17. Springer-Verlag.
  13. Oki, B. M. and Liskov, B. H. 1988. Viewstamped replication: A new primary copy method to support highly-available distributed systems. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing, pp. 8–17. ACM Press.
  14. Schneider, F. B. 1990. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys 22, 4 (Dec.), 299–319.
  15. Skeen, M. D. 1982. Crash recovery in a distributed database system. Ph. D. thesis, University of California, Berkeley.
Who was who on Paxos

The paper gives its Paxons the names of computer scientists, spelled in a mock-Greek alphabet.

Λ˘ινχ∂Nancy LynchKeeper of scroll entry 155; co-author of the FLP impossibility result the paper cites.
Φισ∂ερMichael FischerHolder of decree 132; the F in FLP.
ΤωυεγSam TouegStruck by a falling statue; developed irreversible amnesia.
ΓραϊJim GrayBallot number (13, Γραϊ); database transactions legend.
ΛινσεϊBruce LindsayBallot number (13, Λινσεϊ); System R database pioneer.
ΩκιBrian OkiMade president straight off the boat; co-invented Viewstamped Replication — the protocol equivalent to Paxos.
ΔφωρκCynthia DworkThe Monday-morning president who filled gaps with olive days.
Δ˘ικστραEdsger W. DijkstraFirst cheese inspector of Paxos — famously strict. Invented self-stabilization.
ΓωυδαMohamed GoudaSecond cheese inspector. Also a cheese.
ΦρανσεζNissim FrancezWine taster, two months.
Πνυελ˘ιAmir PnueliWine taster, one month; temporal-logic Turing laureate.
ΔωλεφDanny DolevThe farmer with the black (and brown) goats.
ΣκεενDale SkeenThe law-abiding merchant; three-phase-commit pioneer.
Στωκμ˘ιρLarry StockmeyerThe legislator with the out-of-date scroll.
Σ∂ν˘ιδερFred SchneiderCitizen reading the law via decree 87; wrote THE state-machine survey.
ΓρεεςDavid GriesThe second inquirer about the olive tax.
ΛισκωφBarbara LiskovMerchant comparing fleece tariffs; the Liskov of Viewstamped Replication.
ΠαρναςDavid ParnasElder statesman whose son inherited his scroll — information hiding at its finest.
ΣτρωνγRay StrongMade a legislator by decree 3252.
ΛαμπσωνButler LampsonThe general who staged the coup — and, in our world, the great champion of the Paxos algorithm.
Λεωνίδας ΓκίμπαςLeonidas GuibasProvided invaluable assistance with the Paxon dialect.
μαδζ∂ωριτ˘ισετ“majority set”The most contested word in Paxon philology.