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.

• Project repository