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.
- 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.
- IBM POWER Memory Model — IMM compiles correctly to POWER.
- 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