A Reachability Logic for a Weak Memory Model with Promises
summary
A compositional proof calculus for reachability on a promising weak‑memory model is presented, using flow event structures as assertions to record promised writes, fulfills, reads and ordering. Per‑thread proof outlines are built and then composed by synchronizing reads with fulfills; composition fails when inherited flows produce cycles or memory‑consistency violations. The calculus is mechanically sound and complete for a simplified ARMv8‑style promising semantics (no release/acquire), handles fences via ordering/absence constraints, and validates load‑buffering while forbidding the double‑write counterexample.
AI-written summary · about
chapters (16)
- 0:00Reachability logic intro
- 1:06Load buffering example
- 3:13Weak memory and promises
- 7:12Proof outlines for weak memory
- 8:40Event structures
- 9:21Disallowed behavior
- 12:14Load buffering proof
- 13:21Fence and constraints example
- 16:27Compositionality and rules
- 17:30Summary and soundness
- 17:53Q&A model restrictions
- 18:57Q&A C++ memory model
- 19:18Q&A event structures
- 20:43Q&A unfulfilled promises
- 21:04Q&A auxiliary variables
- 22:13Q&A validity vs provability
related talks
17mPutting Weak Memory in Order via a Promising Intermediate Representation
14mMaking Weak Memory Models Fair
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
15mSoundness of Predictive Concurrency Analyses
21mCSL and relaxed memory
01h 11mProgramming language memory models: Problems, solutions, and directions
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++