TheStellar Consensus Protocol 11 that by quorum availability despite DSets B and B , U and U are quorums in ⟨V,Q⟩. 1 2 1 2 It follows from the definition that the union of two quorums is also a quorum. Hence V⧵B=U ∪U isaquorumandwehavequorumavailabilitydespiteB. 1 2 We must now show quorum intersection despite B. Let U and U be any two a b B quorums in ⟨V,Q⟩ . Let U = U ∩ U = U ⧵ B . By quorum intersection of ⟨V,Q⟩, 1 2 2 1 B U = U ∩U ≠ ç. But then by Theorem 1, U = U ⧵B must be a quorum in ⟨V,Q⟩ 1. 1 2 2 1 NowconsiderthatU ⧵B andU ⧵B cannotbothbeempty,orelseU ⧵B =U would a 1 a 2
a a B B1 B1 be. Hence, by Theorem1,eitherU ⧵B isaquorumin ⟨V,Q⟩ =⟨V,Q⟩ ,orU ⧵B
a 1 a 2 B B2 B is a quorum in ⟨V,Q⟩ =⟨V,Q⟩ 2,orboth.Intheformercase,notethatifU ⧵B is a 1 B B a quorum in ⟨V,Q⟩ 1, then by quorum intersection of ⟨V,Q⟩ 1, (U ⧵B )∩U ≠ ç; since a 1 (U ⧵B )∩U = (U ⧵B )⧵B , it follows that U ⧵B ≠ ç, making U ⧵B a quorum in a 1 a 1 2 a 2 a 2 B2 B2 ⟨V,Q⟩ . By a similar argument, U ⧵B must be a quorum in ⟨V,Q⟩ . But then quo- b 2 rumintersection despite B tells us that (U ⧵B )∩(U ⧵B ) ≠ ç, which is only possible 2 a 2 b 2 if U ∩U ≠ç. a b THEOREM3. In an FBAS with quorum intersection, the set of befouled nodes is a DSet. PROOF. Let B be the intersection of every DSet that contains all ill-behaved min nodes. It follows from the definition of intact that a node v is intact iff v ∉ B . Thus, min B is precisely the set of befouled nodes. By Theorem 2, DSets are closed under in- min tersection, so B is also a DSet. min 5. FEDERATEDVOTING This section develops a federated voting technique that FBAS nodes can use to agree on a statement. At a high level, the process for agreeing on some statement a involves nodes exchanging two sets of messages. First, nodes vote for a. Then, if the vote was successful, nodes confirm a, effectively holding a second vote on the fact that the first vote succeeded. From each node’s perspective, the two rounds of messages divide agreement on a statement a into three phases: unknown, accepted, and confirmed. (This pattern dates backtothree-phasecommit[SkeenandStonebraker1983].)Initially,a’sstatusiscom- pletely unknowntoanodev—acouldenduptrue,false,orevenstuckinapermanently indeterminate state. If the first vote succeeds, v may come to accept a. No two intact nodeseveracceptcontradictorystatements,soifvisintactandacceptsa,thenacannot be false. For two reasons, however, v accepting a does not suffice for v to act on a. First, the fact that v accepted a does not mean all intact nodes can; a could be stuck for other nodes. Second, if v is befouled, then accepting a means nothing—a may be false at intact nodes. Yet even if v is befouled—which v does not know—the system may still enjoy quorum intersection of well-behaved nodes, in which case, for optimal safety, v needs greater assurance of a. Holding a second vote addresses both problems. If the second vote succeeds, v moves to the confirmed phase in which it can finally deem a true and act on it. The next few subsections detail the federated voting process. Because voting does not rule out the possibility of stuck statements, Section 5.6 discusses how to cope with them. Section 6 will turn federated voting into a consensus protocol that avoids the possibility of stuck slots for intact nodes.