DRFx Memory Model
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.
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