Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
summary
Presents a fault-aware ADO model that exposes partial failures (uncommitted but visible updates) while hiding protocol internals, and a verification stack called Advert Coq toolchain that proves safety and refinement. Verifies a lock-free key-value store and a Two-Phase Commit DApp with replicated resource managers, shows multi-Paxos and Chain Replication refine ADO semantics, and connects an actual C multi-Paxos implementation down to the ADO spec via certified abstraction layers; artifacts and proofs are on Zenodo.
AI-written summary · about
chapters (9)
- 0:00ADO model introduction
- 1:51Existing model limitations
- 4:42ADO model benefits
- 6:11ADO structure and operations
- 8:24ADO in multi-Paxos
- 10:11Building apps with ADOs
- 11:57ADO failures and optimization
- 13:00ADO to protocol refinement
- 14:03Conclusion and future
related talks
18mAdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
50mCadre: Building Reliable Distributed Stateful Applications
43mWhat We Talk About When We Talk About Distributed Systems
48mThe Verification of a Distributed System
17mMixed & Verified Consistency with Propel and ConOpY
41mProving linearizability of fault-tolerant register protocols: dependency graph approach