Modular Relaxed Dependencies (MRD)
Resolves the thin-air problem by tracking syntactic dependencies modularly, using a denotational semantics. Intended as a sound and compositional replacement for relaxed C11 atomics.
Ordering relationships
- Strictly stronger than
- C11/C++11 Memory Model — MRD is a proposed replacement for C11 relaxed atomics, forbidding thin-air reads that C11 allows.
- Symbolic MRD (sMRD) — Symbolic MRD extends MRD: it keeps the modular semantic-dependency approach and thin-air freedom, but additionally admits aggressive optimisations MRD forbids — those exploiting alias analysis, undefined-behaviour freedom, and extrinsic choices such as over-alignment — and handles dynamic memory rather than only concrete locations. Admitting more transformations, it permits strictly more behaviours.
References
- Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty. Modular Relaxed Dependencies in Weak Memory Concurrency. ESOP 2020, 2020. doi:10.1007/978-3-030-44914-8_22