Adore: Atomic Distributed Objects with Certified Reconfiguration
summary
Presents Adore, an object-level abstraction that yields the first safety proof with hot reconfiguration by formalizing a cache-tree model and three concrete reconfiguration rules that prevent split commits. Formal development in Coq produces a parametric proof (over quorum schemes), a refinement to a Raft-like implementation, and an executable artifact via Coq extraction to OCaml. The work completes the safety proof, shows how rules prevent the known Raft bug, and yields a verified, runnable protocol.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:15Why Reconfiguration?
- 3:25Network-Based Abstractions
- 4:10State Machine Replication (SMR)
- 9:21Reconfiguration in Adore
- 10:05Reconfiguration Rules
- 12:03Proving Safety
- 14:05Refinement
- 14:23Extraction
- 14:37Conclusion
related talks
18mAdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol
28mReasoning about Distributed Reconfigurable Systems
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
45mCorrectness proofs of distributed systems with Isabelle
15mModular Verification of Op-Based CRDTs in Separation Logic
01h 11mA Programmable Cloud: CALM Foundations and Open Challenges