Room 206 (2nd floor, badged access)
27 June 2024 - 14h00
Executable semantics based on Choice Trees for a concurrent subset of LLVM IR
by Nicolas Chappe from ENS-Lyon, LIP, CASH
Abstract: Monadic interpreters have gained increasing attention as a powerful tool for modeling and reasoning about first order languages. In the Coq ecosystem, our Choice Trees (CTrees) library provides generic tools to craft such monadic interpreters while supporting concurrency with nodes encoding non-deterministic choice. This monadic approach allows the definition of programming language semantics that is modular, compositional and executable.
I will talk about CTrees and their application to formalize semantics for concurrency and weak memory models in Coq. Our semantics is built in successive stages, interpreting each aspect of the semantics separately. We instantiate the approach by defining the semantics of a minimal concurrent subset of LLVM IR with a memory model based on Kang et al’s work on Promising Semantics, but 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 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.
Nicolas Chappe est en 3° année de thèse avec Ludovic Henrio et Yannick Zakowski.
Il viendra nous présenter ses travaux, notamment sur les Choice Trees (POPL'23).
