An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
summary
Claims a library-abstraction theorem for RC11-style weak memory by giving an operational semantics exposing knowledge propagation that records propagation events in totally ordered histories. Introduces mgc calling policies and a new partial release-acquire access mode to distinguish intra-library from client synchronization. Proves equivalence to RC11 declarative semantics, gets data-race-freedom as an instance, and verifies a concurrent-queue refinement where the implementation uses relaxed accesses. Uses the FDR refinement checker to validate an RCU-style specification and mechanized proofs of refinement.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:33Relaxed Memory Programming
- 1:55Weak Memory Model
- 3:52Support for Library Calling Policy
- 4:34Library Abstraction Theorem
- 4:48Library Abstraction as a Formal Agreement
- 7:38Key Observation
- 8:17Novel Semantics: RC11p
- 10:10Counter-Example (revisited)
- 12:34RC11 Equivalent to RC11p
- 13:30Local Data Race Freedom
- 14:53Partial Release-Acquire Accesses
- 17:30Conclusion
- 19:34An application: Read-Copy-Update
related talks
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
14mMaking Weak Memory Models Fair
30mImplementing and Verifying Release-Acquire Transactional Memory in C11
55m“A lock-free concurrency toolkit for deferred reclamation and optimistic speculation"
23mA Denotational Approach to Release/Acquire Concurrency
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...