DRFx Memory Model

2010 · Marino, Singh, Millstein, Musuvathi, Narayanasamy · language, formal

An SC-preserving model with catch-fire semantics. A runtime is guaranteed to raise an exception if a program has a data race, and otherwise yields only sequentially consistent outcomes; the data-race detection is made practical through region-bounded checks with some hardware support. Any sequentially valid optimisation (instruction reordering, common-subexpression elimination) is sound within compiler-designated regions, but transformations that introduce speculative reads or writes are unsound. An efficient hardware-assisted implementation is reported at roughly 3.25% average overhead.

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: no x86
no POWER
no Armv7
no Armv8
Reordering sound: no Store→Load
no Store→Store
no Load→Load
no Load→Store
Elimination sound: yes Store/Load
yes Store/Store
yes Load/Load
yes Load/Store
Other local transformations: yes Irrelevant load elim.
no Speculative load intro.
yes Roach motel
yes Inverse roach motel Poetzl & Kroening 2015
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

Equivalent to: Sequential Consistency (SC) — Both yield only sequentially consistent outcomes for data-race-free programs. DRFx additionally gives racy programs catch-fire semantics — a runtime raises an exception when it detects a region-bounded data race — so the survey groups it with SC rather than weakening the behaviour of well-synchronised code.

References

Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy. DRFx: A Simple and Efficient Memory Model for Concurrent Programming Languages. PLDI 2010, 2010. doi:10.1145/1806596.1806636
Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, Satish Narayanasamy. DRFx: An Understandable, High Performance, and Flexible Memory Model for Concurrent Languages. ACM Transactions on Programming Languages and Systems (TOPLAS), 2016. doi:10.1145/2925988
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
Daniel Poetzl, Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models. arXiv:1510.07171, 2015. arxiv.org/abs/1510.07171

Open DRFx in the interactive map →