CSL and relaxed memory
summary
Provides a compositional denotational semantics using pomsets parameterized by a memory model via a relaxation relation and a linearity constraint (row and lin), builds relaxed concatenation and parallel composition that enforce coherence, and proves a data‑race‑freedom equivalence: any race‑free weak‑memory pomset linearizes to an SC execution with identical reads (DRF property). Applies that to lift the original CSL soundness proof from SC to TSO and PSO without modeling buffers, avoids thin‑air behaviors, and produces a uniform, modular framework.
AI-written summary · about
chapters (12)
- 0:00CSL and relaxed memory intro
- 1:21History of concurrent separation logic
- 3:29Actions in concurrent separation logic
- 4:12Trace semantics limits
- 5:57Relaxed memory models
- 8:29Pomsets vs traces
- 10:16Memory coherence constraints
- 11:40CSL soundness with pomsets
- 13:48Generic semantics across models
- 16:14Denotational approach benefits
- 17:41Conclusions and future work
- 19:06Q&A
related talks
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
14mMaking Weak Memory Models Fair
20mThe Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
23mA Reachability Logic for a Weak Memory Model with Promises
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic