The Part-Time Parliament
ACM Transactions on Computer Systems, 1998 · paper · Computer science
Describes the legislative protocol of the ancient Paxos parliament, whose part-time legislators kept consistent records despite absences and unreliable messengers. The protocol offers a new way to implement the state-machine approach to distributed systems.
Checked: PDF from lamport.azurewebsites.net, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance "This is a total of three message delays and about 3N messages, assuming a parliament of N legislators and a quorum of about N/2" and "a total of only 2N messages per decree" do not match the counts implied by steps (3)–(5) as printed.
- p. 18 Section 3.2.2, steps (3)–(5) and the paragraph after them
This is a total of three message delays and about 3N messages, assuming a parliament of N legislators and a quorum of about N/2.
- p. 18 Section 3.2.2
for a total of only 2N messages per decree
- p. 18 Section 3.2.2, after step (5)
about 3N messages, assuming a parliament of N legislators and a quorum of about N/2
Only the authors can say what is right here.
Judge's note: Checked p.18 (printed page 17). Step (3) sends BeginBallot 'to each legislator in a quorum' (about N/2 messages). Step (4) has each quorum member send Voted (about N/2). Step (5) sends Success 'to every legislator' (N). That adds up to about 2N, not 3N. If BeginBallot is combined with the previous Success, the BeginBallot messages drop out and the total is about 1.5N, not 2N. The figures 3N and 2N would hold only if steps 3 and 4 involved all N legislators. The paper gives no other counting rule, so the authors would need to say which is intended.
Second check: another model agreed
Report a problem with this finding
Substance Decree "2716: 8:30 15 Jan 72—∆ĭκστρα is cheese inspector for 3 months" is followed by "His term would end at 8:30 on 15 March", which is two months after the stated start.
- p. 19 Section 3.3.3 Bureaucrats, decree 2716 and the text after it
2716: 8:30 15 Jan 72—∆˘ικστρα is cheese inspector for 3 months
- p. 19 Section 3.3.3, following sentence
His term would end at 8:30 on 15 March
- p. 19 Section 3.3.3, decree 2716 and following paragraph
is cheese inspector for 3 months
Only the authors can say what is right here.
Judge's note: Checked p.19 (printed page 18). The term starts at 8:30 on 15 January or later ('whichever was later'). A later start could only push the end beyond 15 April, never back to 15 March. Either '3 months' or '15 March' is a slip, and only the author can say which; the resignation decree dated 3 Mar 72 fits either reading.
Second check: another model agreed
Report a problem with this finding
Substance Start Polling chooses d from 'the maximum element of prevVotes[p]' while only requiring 'Q ⊆ {v_pst : v ∈ prevVotes[p]}', so the claim 'Conjunct I4(p) implies that the new ballot added by the Start Polling action does not falsify B3(B)' fails when Q is a proper subset of the responders.
- p. 28 Appendix A1, Start Polling Majority Set Q action
Let v be the maximum element of prevVotes[p]. If vbal ̸= −∞ then d = vdec
- p. 28 Appendix A1, Start Polling enabling condition
Q ⊆ {vpst : v ∈ prevVotes[p]}
- p. 32 Appendix A2, proof of I6
Conjunct I4(p) implies that the new ballot added by the Start Polling action does not falsify B3(B).
Only the authors can say what is right here.
Judge's note: Reworked on pp.28, 30–32. B3 (p.9 text): for every B, if MaxVote(B_bal,B_qrm,B)_bal ≠ −∞ then B_dec = MaxVote(...)_dec. I4 gives v = MaxVote(lastTried[p], v_pst, B) for each v in prevVotes[p], so max(prevVotes[p]) = MaxVote(b, R, B) with R ⊇ Q, not MaxVote(b, Q, B). I checked the reviewer's run step by step against the action enabling conditions with 5 priests and majority 3. Ballot 1 (t): q,s,t give null votes; Q={q,s,t}, decree α; q votes (1 = nextBal[q] > −∞). Ballot 2 (r): r,t,p give null votes (t had not voted), decree β; r votes. Ballot 3 (p): LastVotes from p (null), q (1,α), s (null), r (2,β); each has 3 > prevBal. Start Polling with Q={p,q,s} ⊆ {p,q,s,r} is enabled, so d = (r,2,β)_dec = β, but MaxVote(3,{p,q,s},B) = (q,1,α). B3 is then false in a reachable state, so I6 as stated is not an invariant and the quoted proof step does not hold. Consistency itself is not affected (the maximum over a superset of a quorum is safe), but the stated invariant and its proof are wrong as printed. The fix is to take the maximum over votes with v_pst ∈ Q.
Second check: another model agreed
Report a problem with this finding
Wording The I6 sketch says 'I3(p) implies that the action adds a vote later than any other vote cast by p in B, so it cannot change MaxVote(Bbal, Bqrm, B) for any B in B'. A new vote by p in ballot b can change MaxVote for any ballot B with B_bal > b and p ∈ B_qrm, and I does not rule this out.
- p. 32 Appendix A2, proof of I6
I3(p) implies that the action adds a vote later than any other vote cast by p in B, so it cannot change MaxVote(Bbal, Bqrm, B) for any B in B.
Only the authors can say what is right here.
Judge's note: I checked the reviewer's state against I1–I7 on p.29–30. With priests p,q,r and majority 2, B = {ballot 3 (owner q, qrm {p,q}, dec α, no voters), ballot 5 (owner r, qrm {p,q}, dec β, no voters)}. nextBal[p]=3, prevBal[p]=−∞; lastTried[q]=3, lastTried[r]=5, and lastTried[p] is any p-owned number. All priests are idle, outcomes are BLANK, and M = {BeginBallot(3,α)}. I1 holds vacuously; I2 holds; I3 holds; I4 and I5 are vacuous (idle); I6 holds (B1, B2, and B3 vacuously since there are no votes); I7 holds. Receive BeginBallot(3,α) at p is enabled (3 = nextBal[p] > −∞) and adds p's vote to ballot 3. Then MaxVote(5,{p,q},B) = (p,3,α) while ballot 5 has dec β, so B3 is false. I is therefore not inductive, and the quoted step is false as printed. The state is probably unreachable, and strengthening I (e.g. nextBal[q] ≥ B_bal for q in B_qrm) would repair the proof, so the stated result stands. Severity S3.
Second check: another model agreed
Report a problem with this finding
15 minor (typos and the like; most checked by the judge only)
Substance Theorem 2 ("Let b be a ballot number and Q a set of priests such that b > Bbal and Q∩Bqrm ≠ ∅ for all B ∈ B") does not exclude the case B = ∅, Q = ∅, where the conclusion cannot hold.
- p. 9 Section 2.1, Theorem 2
Let b be a ballot number and Q a set of priests such that b > Bbal and Q∩Bqrm ̸= ∅ for all B ∈ B.
- p. 6 Section 2.1, ballot definition
Bqrm A nonempty set of priests (the ballot’s quorum).
Only the authors can say what is right here.
Judge's note: I reworked this myself. On p.6, a ballot's quorum is defined as 'A nonempty set of priests', 'set' means finite set, and B2 requires that any two ballots in B share a priest. If B = ∅, both hypotheses about b and Q hold vacuously for every Q, so Q = ∅ is allowed. The conclusion then needs a ballot B' with B'qrm = ∅, which the definition forbids, and B2({B'}) would need ∅∩∅ ≠ ∅, which is false. For any nonempty B the hypothesis forces Q to be nonempty, and in the protocol Q is a majority set, so only this degenerate case fails. The fix is to add 'Q nonempty'. Severity follows the rule that a theorem false as printed is S1. I rated it minor because the gap is a vacuous edge case.
Second check: another model agreed
Report a problem with this finding
Wording prevVote[p] is defined as "The vote cast by p ... or −∞ if he never voted", giving a vote-valued variable a ballot-number default instead of the null vote null_p defined earlier.
- p. 12 Section 2.3, definition of prevVote[p]
or −∞ if he never voted.
- p. 12 Section 2.3, definition of prevVote[p]
or −∞if he never voted
- p. 11 Section 2.2, step (2)
or his null vote nullq if q did not vote in any ballot
Judge's note: On p.12, prevVote[p] is a vote whose default is printed as −∞. Step (2) sends prevVote[q] as the vote v in LastVote(b, v). The preliminary protocol (p.11) uses 'his null vote null_q' for the same case, and the appendix splits the variable into prevBal = −∞ and prevDec. '−∞' is evidently shorthand for the null vote, but that shorthand is never defined. This is a notational inconsistency only.
Second check: another model agreed
Report a problem with this finding
Wording "algorithms were devised to tolerate up to any fixed number f of arbitrary failures" vs "if fewer than f processes fail ... But if more than f failures occur" — the stated bound shifts, and exactly f failures is covered by neither clause.
- p. 24 Section 4.1, last paragraph
tolerate up to any fixed number f of arbitrary failures
- p. 25 Section 4.1, top of page
than f processes fail, then state machine commands are executed within a fixed
- p. 24 Section 4.1, last paragraph
algorithms were devised to tolerate up to any fixed number f of arbitrary failures
- p. 25 Section 4.1, first lines
if fewer than f processes fail, then state machine commands are executed within a fixed length of time
Judge's note: Checked the end of p.24 and the top of p.25. The text says the algorithms tolerate 'up to' f failures, then gives the guarantee for 'fewer than f' and the failure case for 'more than f'. Read literally, the boundary case of exactly f is left unstated. This is loose wording, not a substantive error.
Second check: another model agreed
Report a problem with this finding
Wording I2(p)'s first conjunct '∧ owner(lastTried[p]) = p' cannot hold for every priest in the initial state, where lastTried[p] is '−∞ if there was none', yet the text says 'checking the first condition is straightforward'.
- p. 29 Appendix A2, definition of I2(p)
∧ owner(lastTried[p]) = p
- p. 26 Appendix A1, variable lastTried[p]
The number of the last ballot that p tried to begin, or −∞ if there was none.
- p. 30 Appendix A2, condition (1)
checking the first condition is straightforward
Only the authors can say what is right here.
Judge's note: Looked at p.26 (lastTried description), p.29 (I2(p)) and p.30 (condition (1)). owner(b) is defined only for ballot numbers (p.27), and no value for owner(−∞) is given anywhere (grep for 'owner'). Initially lastTried[p] = lastTried[q] = −∞, so I2(p) ∧ I2(q) would need owner(−∞) = p and owner(−∞) = q for p ≠ q, which is impossible. Condition (1) therefore fails as written. This is a boundary slip: guarding the conjunct with lastTried[p] ≠ −∞ fixes it, and the result stands.
Second check: another model agreed
Report a problem with this finding
Wording The example of a 'silly' action, 'sending another BeginBallot message to a priest from whom he has already received a LastVote message', describes a condition that every BeginBallot recipient meets (quorum[p] ⊆ LastVote senders), so the qualifier does not show why the action is silly.
- p. 27 Appendix A1, paragraph before 'Try New Ballot'
such as sending another BeginBallot message to a priest from whom he has already received a LastVote message
Judge's note: Looked at p.27 (printed p.26) and the Start Polling and Send BeginBallot actions on p.28. Start Polling requires Q ⊆ {v_pst : v ∈ prevVotes[p]}, and Send BeginBallot sends only to priests in quorum[p]. So every BeginBallot goes to a priest from whom p has already received a LastVote. Read as a duplicate ('another') BeginBallot, the example is still silly, but the 'already received a LastVote' clause adds nothing; 'Voted' may have been intended. Only the author can say which, so this is a wording point.
Second check: another model agreed
Report a problem with this finding
Wording The I4(p) sketch says Try New Ballot 'leaves I4(p) true because it sets status[p] to trying'. Setting status to trying makes the antecedent of I4(p) true; what preserves I4(p) is that the action also sets prevVotes[p] to ∅.
- p. 31 Appendix A2, invariance sketch for I4(p)
which leaves I4(p) true because it sets status[p] to trying
Only the authors can say what is right here.
Judge's note: Looked at p.31 (printed p.30) and the definition of I4(p) on p.30: (status[p] ≠ idle) ⇒ ∀v ∈ prevVotes[p] : …. Setting status[p] to trying cannot by itself preserve the implication. The same paragraph gives the correct reason a few lines earlier ('sets prevVotes[p] to ∅, making I4(p) vacuously true'). The justification is faulty but the step's conclusion stands.
Second check: another model agreed
Report a problem with this finding
Typo Footnote 6: "translating the Paxon’s more primitive notation" uses a singular possessive where the plural 'Paxons’' (the Paxon mathematicians) is meant.
- p. 6 Footnote 6
translating the Paxon’s more primitive notation
Judge's note: Checked footnote 6 on p.6 in the crop and the full page. The same footnote opens with 'Paxon mathematicians' in the plural, so 'the Paxon's' reads as an apostrophe slip. Cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.4: "initiating too may ballots can also prevent progress" — 'may' should be 'many'.
- p. 13 Section 2.4, second paragraph
initiating too may ballots can also prevent progress
- p. 13 Section 2.4, paragraph 2
initiating too may ballots
Judge's note: Visible on the p.13 page image. A plain misspelling.
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.3: "so it does not addresses the question of progress" — should be 'does not address'.
- p. 13 Section 2.3, paragraph after step (6)
so it does not addresses the question of progress
- p. 13 Section 2.3
so it does not addresses
- p. 17 Section 3.2.1
said to to be proposed
Judge's note: Visible on the p.13 page image. The 'to to' item that one reviewer folded in here is judged under C009.
Second check: none (judge only)
Report a problem with this finding
Typo Typographical slips: 'fault-toerant' (Gray and Cheriton reference), 'so it does not addresses', 'initiating too may ballots', 'the difficultly arises', 'said to to be proposed', and 'Saarbruken' (De Prisco et al. reference).
- p. 33 References, Gray and Cheriton 1989
Leases: An efficient fault-toerant mechanism
- p. 33 Reference Gray and Cheriton 1989
efficient fault-toerant mechanism
- p. 33 References, Gray and Cheriton 1989
fault-toerant
- p. 13 2.3, last paragraph
so it does not addresses
Judge's note: Every item is visible on the page images: 'fault-toerant' and 'Saarbruken' on p.33; 'does not addresses' and 'too may ballots' in the p.13 crops; 'difficultly arises' in the p.15 crop; 'to to be' in the p.17 crop. None is an extraction artefact. All are cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Section 2.4: "However, the difficultly arises only because" — 'difficultly' should be 'difficulty'.
- p. 15 Section 2.4, top of page
However, the difficultly arises only because
- p. 15 Section 2.4, first paragraph on page 14
the difficultly arises only because
- p. 15 Section 2.4
the difficultly arises only
Judge's note: Visible at the top of the p.15 page image (printed page 14).
Second check: none (judge only)
Report a problem with this finding
Typo Footnote 12: "...before a rigorous proof of this result was given.[Fischer et al. 1985]" — the citation follows the full stop with no space.
- p. 15 Footnote 12
was given.[Fischer et al. 1985]
Judge's note: Visible in footnote 12 on the p.15 image. A punctuation and placement point only.
Second check: none (judge only)
Report a problem with this finding
Typo Section 3.2.1: "A decree was said to to be proposed" — duplicated 'to'.
- p. 17 Section 3.2.1, second paragraph
A decree was said to to be proposed
- p. 17
be deduced. A decree was said to to be proposed when it
Judge's note: The reviewers place this on p.17, and the crops show both words on the same line, so this is not a line-break artefact. The full page images I opened (p.18, p.19) are of other pages.
Second check: code check
Report a problem with this finding
Typo Section 3.3.1: "laboriously copied six months worth of decrees" — standard form is 'six months’ worth'.
- p. 18 Section 3.3.1
laboriously copied six months worth of decrees
Judge's note: Visible on the p.18 image. A missing possessive apostrophe; cosmetic.
Second check: none (judge only)
Report a problem with this finding
Typo Section 4.1: "provides a distributed, fault-tolerant implementation of the database system," ends the paragraph with a comma instead of a full stop.
- p. 24 Section 4.1, paragraph after Fig. 2
implementation of the database system,
- p. 24 Section 4.1, paragraph after Fig. 2
provides a distributed, fault-tolerant implementation of the database system,
Judge's note: The p.24 page image shows a comma at the end of the paragraph, and a new paragraph follows.
Second check: none (judge only)