Monadic interpreters have gained increasing attention as a powerful tool for modeling and reasoning about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) library provides generic tools to craft such monadic interpreters in presence of divergence, stateful effects, failure, and nondeterminism. This monadic approach allows the definition of semantics for programming languages that are modular in its effects, compositional w.r.t. its syntax, and executable.

This paper demonstrates the use of CTrees to formalize a semantics for concurrency and weak memory models in Coq. We instantiate the approach by defining the semantics of a minimal concurrent subset of LLVM IR. Our semantics is built in successive stages, interpreting each aspect of the semantics separately. In particular, one stage encodes multi-threading as an interleaving semantics, and another stage implements a weak memory model that supports various LLVM memory orderings. Furthermore, the modularity of the approach makes it possible to plug a different source language or memory model by changing a single interpretation phase. By leveraging the notions of (bi)similarity of CTrees, we establish the equational theory of our constructions, show how to transport equivalences through our layered construction, and prove simulation results between memory models. Finally, our model is executable, hence the semantics can be tested by extraction to OCaml.