Bridging the Gap between Programming Languages and Hardware Weak Memory Models

TL;DR

This paper introduces IMM, an intermediate weak memory model, to facilitate modular proofs of compilation correctness from concurrent languages to multi-core architectures, with mechanized verification in Coq.

Contribution

The paper presents IMM, a novel weak memory model, and demonstrates its use in machine-verified correctness proofs for compilation to POWER and ARM architectures.

Findings

Corrected and improved previous compilation correctness results

Mechanized proofs in Coq for models weaker than x86-TSO

Validated compilation correctness for POWER and ARM architectures

Abstract

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 consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove the correctness of compilation from the promising semantics of Kang et al. to POWER (thereby correcting and improving their result) and ARMv7, as well as to the recently revised ARMv8 model. 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.