A Denotational Approach to Release/Acquire Concurrency
summary
Presents a directionally adequate denotational semantics for Release/Acquire memory using Brookes-style trace semantics adapted to a view-based machine; traces carry initial and final views and are closed under new rewind/forward closure rules plus a Titan rewrite to justify tricky transforms like read/WR reorder and read elimination. Semantics is compositional, supports known RA program transformations and first-class parallelism, but omits recursion, non-atomics and does not claim full abstraction.
AI-written summary · about
chapters (19)
- 0:00Denotational semantics intro
- 0:26Standard-based semantics goal
- 1:31Brook-style traces basics
- 3:17Denotational approach contributions
- 3:58Weak memory crash course
- 5:42Timelines and message propagation
- 7:28Operational semantics to parallelism
- 8:11Trace-based release/acquire
- 9:58Rely-guarantee trace rules
- 11:47Composing terms and traces
- 12:29Abstraction via program transforms
- 13:32Read elimination validity
- 15:02Write-read reordering challenges
- 16:27Closure rules decoupling
- 16:49Titan rule justification
- 18:15Conclusion and limitations
- 19:41Future directions
- 20:23Q&A: Recursion limits
- 20:45Q&A: No full abstraction
related talks
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
15mThread-modular Analysis of Release-Acquire Concurrency
48mNot Just Happens-Before: Unconventional Semantics
30mImplementing and Verifying Release-Acquire Transactional Memory in C11
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
20mDisentanglement with Futures, State, and Interaction
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency