Intermediate Memory Model (IMM)
Bridging model between high-level language models and hardware. Correctly compiles to x86-TSO, ARMv8, and POWER. Supports DRF-SC and eliminates thin-air reads. Serves as a compilation target and proof intermediate.
Cat model
Expressible in cat author-extrapolated
Declarative by construction: acyclicity and irreflexivity axioms over one candidate execution, mechanised in Coq. The axioms transcribe to cat directly, but no cat file accompanies the development. Podkopaev et al. 2019
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Compilation optimal mapping to
- yes x86
- yes POWER
- yes Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Compiles correctly to
- ARMv8 / AArch64 Memory Model — IMM compiles correctly to ARMv8. Machine-checked with kater: imm::psc ⊆ arm8::ob*, the mapping's soundness condition, under the well-formedness premise rf;rmw ⊆ mo (litmus/kater/queries/compilation-IMM-vs-ARMv8.kat) — the paper's Table 1 query, reproduced here.
- IBM POWER Memory Model — IMM compiles correctly to POWER.
- x86-TSO — IMM compiles correctly to x86-TSO. Machine-checked with kater: imm::psc ⊆ tso::tso* over kater's imm.kat and tso.kat (litmus/kater/queries/compilation-IMM-vs-x86-TSO.kat). kater's tso.kat is the TSO rendering; it carries to the x86-TSO node along the by-construction TSO ≡ x86-TSO equivalence edge.
- Compilation target of
- Promising Semantics 1.0 (PS) — Podkopaev, Lahav & Vafeiadis (POPL 2019) prove in Coq that compilation from the Promising Semantics to IMM is correct, and from there to x86-TSO, POWER and ARMv8. On ARMv8, PS 1.0's relaxed RMWs need an extra ld fence, because the intended mapping is unsound (the FADD load-buffering, Chakraborty & Vafeiadis 2019 Fig. 6). PS 2.0 removes that fence.
- Promising Semantics 2.0 (PS 2.0) — Lee et al. (PLDI 2020), Theorem 6.9, mechanised in Coq: Beh_PS2.0(P) ⊇ Beh_IMM(P), so the mappings already proved correct from IMM (x86-TSO, POWER, ARMv7, ARMv8, RISC-V) are correct from PS 2.0, without PS 1.0's extra fence after RMWs. The mechanised proof needs a control dependency from the read part of each RMW, which relaxed fetch-and-adds must fake on ARMv8 (§6.5).
- Incomparable with
- Repaired C11 (RC11) — IMM is designed to compile correctly to hardware; it is related to RC11 but targets a different point in the design space.
References
- Anton Podkopaev, Ori Lahav, Viktor Vafeiadis. Bridging the Gap between Programming Languages and Hardware Weak Memory Models. POPL 2019, 2019. doi:10.1145/3290382