Towards composable proofs of cache coherence protocols
summary
Proposes a compositional proof that MSI refines the combination of MI and SI, formalized in Lean 4, cutting required invariants from hundreds to just 15 by proving five classes of local invariants (signal relations, uniqueness, over‑approximation, conflict, signal→state) between one cache and its parent/memory. Works for parametric N caches, proves global coherence (no MS configuration) from only per‑link properties, and ships artifacts and proofs (DOI/Zenodo) for reuse. 15 local invariants Lean 4 formalization
AI-written summary · about
chapters (10)
- 0:00Composable cache coherence proofs
- 1:28Cache coherence needs simpler proofs
- 2:55MSI states in cache coherence
- 5:07Global correctness challenges
- 7:56Local invariants for coherence
- 10:44Five MSI invariant classes
- 11:46Extending to SI and MI subprotocols
- 12:51Modular MSI refinement proofs
- 15:18Summary and future directions
- 15:41Q&A
related talks
20mAn Automated Scalable RISC-V Cache Coherency Verification Project
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
45mCorrectness proofs of distributed systems with Isabelle
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
14mA Refinement Methodology for Distributed Programs in Rust
21mMechanizing the CMP Abstraction for Parameterized Verification
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
25mProperty-agnostic base case extension for scalable verification of distributed systems