Monadic interpreters have gained increasing attention as a powerful tool for modeling and reasoning about first order languages. A monadic approach allows the definition of programming language semantics that is modular, compositional and executable. In particular, the Vellvm project uses the Interaction Tree data structure to formalize the semantics of sequential LLVM IR in the Coq proof assistant.
We work towards extending this line of work to concurrency. Our contribution is twofold. First, we revise the underlying tree structure, introducing Choice Trees, a variant of Interaction Trees with a new kind of node that represents nondeterministic choice. This addition has many meta-theoretical implications, hence we extensively study coinductive proof techniques on Choice Trees, in particular related to notions of program equivalence and program refinement, in which labeled transition systems play a central role.
Taking advantage of this novel Choice Trees structure, we model the semantics of a minimal concurrent subset of LLVM IR. Our semantics is built in successive stages, interpreting each aspect of the semantics separately. We instantiate the approach with a Promising-like memory model. The modularity of the approach makes it possible to plug a different memory model (or source language) by changing a single interpretation phase. By leveraging results on the notions of (bi)similarity of CTrees, we establish the equational theory of our constructions, and show how to transport equivalences through our layered construction. Finally, our model is executable, hence we can test the semantics by extraction to OCaml.
Gratuit
Disciplines