Theorem Two
This theorem guarantees that progress can continue: we can always create a new ballot without violating the rules, preventing deadlock.
LAMPORT, P. 8 β Β§2.1Assume the constraints B1(π), B2(π), and B3(π) hold.
Let $b$ be a ballot number larger than the largest successful ballot, and let $Q$ be a set of priests such that $Q \cap B_{\mathrm{qrm}} \neq \emptyset$ for all $B \in \mathcal{B}$.
Then there exists a new ballot $B'$ with:
- $B'_{\mathrm{bal}} = b$
- $B'_{\mathrm{qrm}} = B'_{\mathrm{vot}} = Q$
such that B1, B2, and B3 continue to hold for $\mathcal{B} \cup \{ B' \}$.
LAMPORT, P. 8 β Β§2.1Condition $B1(B \cup \{B'\})$ follows from $B1(B)$, the choice of $B'_{bal}$, and the assumption about $b$.
Condition $B2(B \cup \{B'\})$ follows from $B2(B)$, the choice of $B'_{qrm}$, and the assumption about $Q$.
If $\text{MaxVote}(b, Q, B)_{bal} = -\infty$ then let $B'_{dec}$ be any decree, else let it equal $\text{MaxVote}(b, Q, B)_{dec}$.
Condition $B3(B \cup \{B'\})$ then follows from $B3(B)$
Preserving B1, B2, B3 for a New Ballot
- B1 β Ballot uniqueness: Each ballot number identifies a unique ballot. By choosing the new ballot number $B'_{\mathrm{bal}}$ larger than all existing ballots in π, thereβs no conflict. B1 holds automatically.
- B2 β Quorums are subsets of votes: The quorum $B'_{\mathrm{qrm}} = Q$ is chosen carefully. Because Q intersects all existing quorums as required, the property remains true. B2 is preserved.
-
B3 β Decree consistency:
Determine the decree for the new ballot as follows:
- If $MaxVote(b, Q, \mathcal{B})_{\mathrm{bal}} = -\infty$, no prior vote exists β pick any decree.
- Otherwise β pick $B'_{\mathrm{dec}} = MaxVote(b, Q, \mathcal{B})_{\mathrm{dec}}$ to maintain consistency.
- Progress guarantee: This construction shows a new ballot can always be added without violating the invariants. Ensures the system can continue and never deadlocks due to running out of ballot numbers.