Compositional Relaxed Concurrency CRC
A compositional relaxed-concurrency semantics for a fragment of the C11 model — non-atomic accesses with catch-fire semantics, release-acquire accesses, and sequentially-consistent fences. Because the relaxed fragment is excluded, the model sidesteps the thin-air problem. The authors built a tool for automatic verification of program transformations in this fragment.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- no Speculative load intro.
- yes Roach motel
- yes Strengthening
- yes Trace preserving
- no Common subexpr. elim.
- Global transformations
- yes Register promotion
- yes Thread inlining
- Reasoning guarantees
- yes External DRF
- yes Coherence
- no No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
Ordering relationships
- Strictly stronger than
- C11/C++11 Memory Model — CRC is a compositional semantics for a thin-air-free fragment of C11 (non-atomics with catch-fire, release-acquire, SC fences); by omitting relaxed atomics it forbids the out-of-thin-air behaviours plain C11 permits.
References
- Mike Dodds, Mark Batty, Alexey Gotsman. Compositional Verification of Compiler Optimisations on Relaxed Memory. ESOP 2018, 2018. doi:10.1007/978-3-319-89884-1_36
- Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050