Modular Verification of Op-Based CRDTs in Separation Logic
summary
Framework verifies operation-based CRDT implementations in Coq using Aneris separation logic and a verified Reliable Causal Broadcast protocol plus an OpLib that turns purely functional CRDT definitions into runnable, mutable-node implementations. Claims modular, executable verification; demonstrates it on 12 example CRDTs (registers, sets, product and map combinators) and shows proofs scale via combinators. Builds causal-broadcast + library, proves convergence and functional correctness, and extracts verified, networked implementations.
AI-written summary · about
chapters (13)
- 0:00Modular CRDT verification intro
- 1:04Strong eventual consistency
- 2:08Op-based CRDTs counterexample
- 3:52Implementation in separation logic
- 4:55Reliable causal broadcast
- 5:59Turning data structures into CRDTs
- 7:01Uplift library interfaces
- 9:25Abstract CRDT denotation
- 10:29Implementer requirements
- 11:09Implemented examples
- 12:13Modularity benefits
- 12:36Conclusion
- 13:24Q&A
related talks
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
29mComposing and decomposing op-based CRDTs with semidirect products
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mCRDT Emulation, Simulation, and Representation Independence
14mAutomatically Verifying Replication-aware Linearizability
16mIgloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica