Programming Languages and Tools Lab

IMM: Compilation Correctness for Relaxed Memory Models

The IMM framework simplifies compilation correctness proofs from programming language memory models (e.g., Promising and Weakestmo) to hardware memory models (x86, Power, Arm, RISC-V). The framework is mechanized in Coq.

We’re developing an intermediate weak memory model, IMM, as a way of modularizing proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove correctness of compilation from multiple new programming language memory models (mainly the ones aiming to fix the out-of-thin-air problem) to hardware memory models such as POWER, ARMv7, ARMv8, RISC-V, and x86-TSO. Our results are mechanized in Coq, and to the best of our knowledge, these are the first machine-verified compilation correctness results for models that are weaker than x86-TSO.


Anton Podkopaev
Evgenii Moiseenko