Symbolic MRD sMRD
A successor to Modular Relaxed Dependencies (MRD) and the first thin-air-free memory model to admit compiler optimisations that aggressively leverage alias analysis, an assumption of freedom from undefined behaviour, and the extrinsic choices of real implementations (e.g. over-alignment). Built on symbolic execution, it models dynamic memory — allocation, dereferencing, and reclamation — rather than only concrete locations, and exports a semantic-dependency relation that integrates with the C/C++ memory model, preserving the standard compilation mappings for atomics. It matches every test in the recently published ISO C/C++ semantic-dependency desiderata, and its tooling runs orders of magnitude faster than other executable thin-air-free semantics.
Ordering relationships
- Strictly weaker than
- Modular Relaxed Dependencies (MRD) — 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.
- Repaired C11 (RC11) — Symbolic MRD interfaces with an RC11-style axiomatic model but refines its dependency relation (dp), removing false dependencies so that load→store reorderings in load-buffering shapes — e.g. the LB+UB+data outcome RC11 forbids because of a cycle in ⊑∪rf — become allowed, while genuine out-of-thin-air cycles stay forbidden. It therefore admits strictly more behaviours than RC11.
- Strictly stronger than
- C11/C++11 Memory Model — Like MRD, Symbolic MRD repairs the C/C++ thin-air problem: it forbids the out-of-thin-air reads C11 permits while preserving the standard atomics compilation mappings, and it matches the ISO C/C++ semantic-dependency desiderata.
References
- Jay Richards, Daniel Wright, Simon Cooksey, Mark Batty. Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice. OOPSLA 2025 (PACMPL vol. 9), 2025. doi:10.1145/3721089
- 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