Monadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
summary
Defines an executable, layered semantics for a concurrent subset of LLVM IR implemented in Coq using CTrees and extracted to OCaml; builds an interleaving layer that inserts explicit scheduling BR/Sk nodes to compose threads, then plugs alternative memory-model interpreters for sequential consistency vs TSO vs promising (subset). Shows each interpretation phase preserves program equivalence, proves simulation relations between models, implements concrete schedulers (deterministic and pseudo‑random) and a collecting interpreter for litmus tests, and publishes the Coq/OCaml code on GitHub.
AI-written summary · about
chapters (11)
- 0:00Monadic interpreters introduction
- 1:57LLVM role in compilation
- 3:39Choice Trees basics
- 6:11Interpreting C-tree nodes
- 10:33C-tree metatheory
- 11:57Modeling LLVM with C-trees
- 13:26Interpretation stack for memory
- 16:59Concurrent memory models
- 21:18Executable models and scheduling
- 23:07Summary and future work
- 24:12Question and answer session
related talks
30mCalculating Compilers for Concurrency
01h 01mThe Future of Concurrency and Parallelism
39mConcurrent Languages are Functional
16mCompound Memory Models
21mCSL and relaxed memory
27mTimed Concurrent Language for Argumentation: an Interleaving Approach
30mA Tale of Shared Memory Concurrency in Programming Languages
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz