The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Conc
summary
Defines a compositional event semantics that attaches preconditions and families of predicate transformers to events, so sequential composition picks a transformer based on which prior events an event semantically depends on, and applies it to ensure no thin‑air reads while allowing compiler and hardware reordering. Claims mechanized proofs totaling 13,000 lines, an OCaml tool that runs litmus tests, and observes an exponential blowup in predicate‑transformer state; model is optimal for MCA architectures and matches ARM‑style behaviors.
AI-written summary · about
chapters (9)
- 0:00Start
- 2:09Concurrency?
- 3:06Hardware Reordering?
- 4:52Compiler Reordering?
- 5:18Semantic Dependencies!
- 9:231 Associative?
- 11:58Real Hardware?
- 13:56Dependencies for C11!
- 19:06Concurrency is easy!
related talks
21mCSL and relaxed memory
16mPomsets with Preconditions: A Simple Model of Relaxed Memory
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
23mA Reachability Logic for a Weak Memory Model with Promises
24mA Compositional Theory of Linearizability
16mCompound Memory Models
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++