Distributed Causal Memory for Higher-Order Distributed Separation Logic
summary
Presents the first full specification and machine-checked verification of a causally-consistent distributed database implementation and client libraries, formalized in Aneris and mechanized in Coq. Implementation follows Ahamad et al., runs three concurrent threads (apply/send/receive), uses vector clocks and per-apply sequence numbers, and maps physical state to an abstract logical time and global memory with a validity predicate. Verifies small concurrency-sensitive examples and a session-manager library; introduces a hookup rule (higher-order concurrent abstract predicate) to soundly reason about non-atomic writes.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:44Causal memory in AnerisLang
- 4:32Formal model for causal memory
- 9:47Modular reasoning with separation logic
- 12:13Client API for reads/writes
- 16:51Verification and verified libraries
- 17:55Conclusion and Q&A
related talks
15mModular Verification of Op-Based CRDTs in Separation Logic
30mVerifying Reliable Network Components in a Distributed Separation Logic with Dep...
28mReasoning about Distributed Reconfigurable Systems
20mInductive diagrams for causal reasoning
21mEmbedding Hindsight Reasoning in Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
14mBolt-On Strong Consistency: Specification, Implementation, and Verification