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.
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
- yes POWER
- yes Armv7
- yes Armv8
- Reasoning guarantees
- yes External DRF
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Repaired C11 (RC11) — Paviotti et al. (Modular Relaxed Dependencies in Weak Memory Concurrency, ESOP 2020) relax the RC11 axiomatic model with their MRD dependency model to form MRD-C11. Lemma 3 (Implementability of MRD-C11): for all programs P, ⟦P⟧MRD-C11 ⊇ ⟦P⟧RC11 — MRD-C11 is strictly weaker than RC11, admitting the false-dependency-eliminating load→store reorderings RC11 forbids while still forbidding out-of-thin-air. (The MRD+IMM instantiation of Theorem 3, ⟦P⟧MRD+IMM ⊇ ⟦P⟧IMM, is a distinct model and is not represented by this node.)
- 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