Bridging the Gap between Programming Languages and Hardware Weak Memory Models

Anton Podkopaev, Ori Lahav, Viktor Vafeiadis

We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consi…