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)
Cosupervised by Dumitru Potop-Butucaru - more details
In some settings, real-time programs can be transformed to parallel and concurrent C programs that satisfy a strong notion of confluence. As a first step towards the formal verification of the soundness of these transformations, we propose to develop a framework for a class of such programs in Iris, using a separation logic for the C11 release/acquire synchronisation discipline. The rules tailored for this class of programs should be enough to establish program safety.