Operational Release-Acquire/Relaxed RC11 RAR
An operational reformulation of RC11 supporting release-acquire and relaxed accesses (hence RAR), on top of which the authors build a proof calculus for invariant-based reasoning and mechanically verify mutual-exclusion algorithms.
Ordering relationships
- Equivalent to
- Repaired C11 (RC11) — RAR is an operational reformulation of RC11's release-acquire and relaxed fragment, used as the basis for an invariant-based proof calculus.
References
- Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick. Verifying C11 Programs Operationally. PPoPP 2019, 2019. doi:10.1145/3293883.3295702
- 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