AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
summary
Claims a single abstraction, AdoB abstraction, unifies benign and Byzantine consensus and lets proofs be done by refinement; implements it in Coq with mechanized Coq proofs that show safety and liveness for both fault models. Gives concrete quorum rules (benign needs 2f+1, Byzantine needs 3f+1; M‑quorum parameterizes overlap and supports 2/3 weight or half/three‑quarter choices for Fast Paxos), refines to network specs of Fast Paxos and a Jolteon variant, and ships evaluated artifacts.
AI-written summary · about
chapters (14)
- 0:00AdoB introduction and goals
- 0:21Consensus problem and faults
- 2:32Synchrony models
- 3:57Verification approach
- 5:23Adobe’s contributions
- 6:26Adobe’s philosophy and cache tree
- 8:32Benign consensus execution
- 10:00Network failures with tcache
- 11:05Unifying benign and Byzantine faults
- 12:50Generalized Janus protocol
- 13:53Fast Paxos refinement
- 14:35Proof effort and lessons
- 14:57Conclusion and future work
- 15:44Q&A
related talks
36mFlexible Byzantine Fault Tolerance
22mLiberating Distributed Consensus
01h 04mConsensus with Asymmetric Trust
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
34mWhat properties should asymmetric quorum systems satisfy?
43mAll Together Now: An Introduction to Distributed Consensus
40mConsensus Algorithms in Distributed Systems
48mDistributed Consensus Algorithms