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.
- x86-TSO — IMM compiles correctly to x86-TSO.
- 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