The goal is to study the feasibility of a certified optimizing compiler for concurrent C programs that takes into account weak memory models. Although weak memory models are often axiomatic, here we are interested in an operational model, which is the operational semantics presented in Section 2 of [1]. In a first phase we will consider a toy language for which we will develop a technique, such as an adaptation of refinement simulations, with which we will prove that some standard optimisations are valid, if not all. The greater goal is to adapt the CompCert compiler to handle standard C programs that make use of release-acquire synchronisations, a paradigm that is faster than mutual-exclusion locks.
This internship involves working with relatively complex operational semantics. We will not have to work with axiomatic memory models, as we will directly work with an operational semantics. Some proofs will be on paper first, but the goal is to have an end-to-end formalization in Rocq.
[1] Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris (Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis)