Repaired C11 with C++17 release sequences (RC17)
RC11 updated to account for the C++17 release-sequence definition: like RC11 (repaired seq_cst, no out-of-thin-air via acyclic(po|rf)), but a release sequence is continued only by read-modify-writes, not by later same-thread relaxed stores. It is therefore strictly weaker than RC11 (it admits a non-synchronising outcome RC11 forbids) and strictly stronger than C++17 (it keeps the no-thin-air axiom C++17 lacks). Mechanised by the rc17.cat model (vendored from gonzalobg/cpp_memory_model; herd7-checked).
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- no Speculative load intro.
- yes Roach motel
- 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
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Strictly weaker than
- Repaired C11 (RC11) — RC17 is RC11 with the C++17 release-sequence narrowing (RMWs only). Like the C11→C++17 case the narrowing is monotone — it only removes synchronisation — so RC17 admits an outcome RC11 forbids and forbids nothing RC11 allows. Mechanised: mp-rs-add-est-atomic is Never under rc11.cat and Sometimes under rc17.cat. Models vendored from gonzalobg/cpp_memory_model; see litmus/strictly-weaker/RC11-vs-RC17.
- Strictly stronger than
- C++17 Memory Model — RC17 and C++17 share the C++17 release sequences but RC17 additionally keeps RC11's no-thin-air axiom acyclic(po ∪ rf), which C++17 lacks. So C++17 permits plain load-buffering / out-of-thin-air reads RC17 forbids, and forbids nothing RC17 allows (RC17 = C++17 plus one axiom, by construction). Mechanised: the relaxed LB shape is Never under rc17.cat and Sometimes under cpp17.cat. Parallels the existing RC11→C11 edge. See litmus/strictly-weaker/RC17-vs-C++17.
References
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer. Repairing Sequential Consistency in C/C++11. PLDI 2017, 2017. doi:10.1145/3062341.3062352
- Cooksey, Brito Gadeschi. C++ Memory Model and Forward Progress Testing (cpp_memory_model): per-version cat models for C++11/17/20 and RC11/RC17. Open-source repository, 2025. github.com/gonzalobg/cpp_memory_model