A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
summary
This work gives a concrete proof recipe and mechanization in Coq (Iris-based iRC11) that reduces manual effort by about 81% via automation, introduces object modification order (OMO) and a commit-with relation to constrain event reordering and enable compositional proofs, and verifies Michael–Scott queue, elimination stack, and Folly’s MPMC queue under relaxed memory, plus stronger spinlock and atomic refcount specs. Artifacts are available and evaluated (DOI: 10.1145/3656384, Zenodo archive).
AI-written summary · about
chapters (9)
- 0:00Linearizability in relaxed memory
- 1:04Challenges in linearizability
- 3:14Reducing proof effort
- 5:00Proof structure for Tri ST
- 7:08Weak connections in proofs
- 9:16Object Modification Order
- 10:42Compositional verification
- 14:32Results and future work
- 15:12Q&A
related talks
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
19mProof Automation for Linearizability in Separation Logic
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
21mCSL and relaxed memory
19mScenario-based Proofs for Concurrent Objects
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz