Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
summary
Compass is a framework that gives strong, compositional specifications for relaxed-memory libraries by combining logical atomicity with partial-order relaxations of linearizability, implemented as extensions to Iris/RC11 and mechanized in Coq. It tracks per-operation event graphs including client-generated happens-before via a new syncQ assertion, and verifies examples (concurrent queue plus a flag synchronization) to rule out an unexpected empty dequeue. Several relaxed specs and verified library implementations are provided.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:14The need for strong relaxed-memory library specs
- 3:55Logical Atomicity: a proof technique for linearizability in SC concurrent separation logic
- 7:06COMPASS: Strong and compositional Hoare-style library specs for relaxed memory
- 10:02What partial orders?
- 11:17Internal synchronization is not enough
- 12:23Combining internal synchronization with external synchronization
- 15:46Conclusion
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mCSL and relaxed memory
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
15mCosmo: A Concurrent Separation Logic for Multicore Ocaml
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
20mThe Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc