Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR

Watch this 30-minute conference talk from CPP 2025 where researchers Nicolas Chappe, Ludovic Henrio, and Yannick Zakowski present their work on using monadic interpreters for modeling concurrent memory models. Explore how the Choice Tree (CTree) library in the Coq ecosystem can be leveraged to create semantics for programming languages that are modular, compositional, and executable. The presentation demonstrates the application of CTrees to formalize semantics for concurrency and weak memory models using a minimal concurrent subset of LLVM IR. Learn about their layered approach to semantics construction, where multi-threading is encoded as an interleaving semantics and different memory orderings are supported. The researchers also discuss how they established equational theories, transported equivalences through their layered construction, and proved simulation results between memory models. The semantics is executable and can be tested through extraction to OCaml. This talk was presented at the CPP 2025 conference sponsored by ACM SIGPLAN and ACM SIGLOG.