A Formally Verified Foundation for Compositional Heterogeneous Coherence
summary
Claims that the de-facto Principle of Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of CPU/GPU coherence protocols and proves it by a machine-checked, compositional theorem. Uses a unifying abstraction—linearization points, abstract states, consistency labels—and verifies industrial and academic protocols (MOESI/CHI and DeNovo) as instances. Proofbase is 26,000 lines of Lean, artifacts are reusable, and the result reduces correctness to checking per-device axioms plus a single-writer/multi-reader interconnect invariant.
AI-written summary · about
chapters (8)
- 0:00Heterogeneous cache coherence intro
- 2:05Memory consistency challenges
- 4:10Synchronous propagation solution
- 8:02CPU-GPU shim behavior
- 9:25Unifying coherence abstraction
- 13:16Realistic protocols in abstraction
- 14:41Formal foundation for shared memory
- 15:25Q&A on non-coherent hardware
related talks
20mFully Composable and Adequate Verified Compilation with Direct Refinements betwe...
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
16mCompositional Symbolic Execution for the Next 700 Memory Models
27mVeracity: Declarative Multicore Programming with Commutativity
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
20mVerified Density Compilation for a Probabilistic Programming Language
23mVerified Compilation of C Programs with a Nominal Memory Model
30mA Tale of Shared Memory Concurrency in Programming Languages