Concurrency Semantics for Relaxed Atomics CSRA
A concurrency semantics for relaxed atomics that permits optimisation while avoiding thin-air executions. It pairs a memory subsystem inspired by the POWER model with a thread subsystem in which each thread is represented as an event structure; at each step the machine may either commit an event to memory or transform one of the event structures. Soundness of the optimal compilation mappings to x86 and POWER was shown, though the mappings to ARMv7/ARMv8 were later revealed to be non-optimal.
Ordering relationships
- Strictly stronger than
- C11/C++11 Memory Model — CSRA pairs a POWER-inspired memory subsystem with per-thread event structures and permits optimisation while avoiding thin-air. Its authors state CSRA is a subset of C/C++11 by design ('the converse is not to be expected ... the point of our model is to exclude the thin-air executions that C/C++11 allows'): only out-of-thin-air outcomes separate them, all allowed by C11 and forbidden by CSRA. So C11 is strictly weaker. (Reclassified from incomparable; see litmus/strictly-weaker/CSRA-vs-C11.)
- Incomparable with
- Promising Semantics (PS) — Both are semantic-dependency-preserving models avoiding thin-air; CSRA's compilation to x86 and POWER is sound, but unlike Promising its mappings to ARMv7/ARMv8 were later shown non-optimal. Neither contains the other.
References
- Jean Pichon-Pharabod, Peter Sewell. A Concurrency Semantics for Relaxed Atomics that Permits Optimisation and Avoids Thin-Air Executions. POPL 2016, 2016. doi:10.1145/2837614.2837616
- 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