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