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.
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