C++17 Memory Model
The C/C++ memory model as of C++17. It narrows release sequences relative to C++11/14: a release sequence is continued only by read-modify-writes, no longer by later relaxed stores of the same thread, so a pattern that synchronised under C++11/14 stops synchronising. It keeps the (broken) C++11 seq_cst and leaves the thin-air problem unresolved. Behaviourally it is therefore strictly weaker than C11/C++11 — it admits a non-synchronising outcome C++11 forbids while forbidding nothing C++11 allows. Mechanised by the cpp17.cat model (vendored from gonzalobg/cpp_memory_model; herd7-checked). Its relationship to C++20 turns on where exactly the release-sequence change landed in the standard — the cpp_memory_model models attribute the narrowing to C++17 while WG21 P0982 is a C++20 paper — so no direct C++17↔C++20 edge is drawn; see the C11↔C++17 litmus README.
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
- yes POWER
- yes Armv7
- yes Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes 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 Thread inlining
- Reasoning guarantees
- no External DRF
- yes Coherence
- no No undefined behaviour
- no In-order execution
- no No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Strictly weaker than
- C11/C++11 Memory Model — C++17 narrows release sequences relative to C++11/14: only RMWs continue a release sequence, no longer later same-thread relaxed stores. That removes happens-before edges, so C++17 admits a non-synchronising message-passing outcome C++11 forbids and forbids nothing C++11 allows (the narrowing is monotone by construction). Mechanised: the all-atomic mp-rs-st-eadd-atomics is Never under cpp11.cat (C++11) and Sometimes under cpp17.cat (C++17). Models vendored from gonzalobg/cpp_memory_model; see litmus/strictly-weaker/C11-vs-C++17.
- Repaired C11 with C++17 release sequences (RC17) — 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
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber. Mathematizing C++ Concurrency. POPL 2011, 2011. doi:10.1145/1926385.1926394
- ISO/IEC. ISO/IEC 14882:2017 — Programming Language C++. ISO Standard, 2017. www.iso.org/standard/68564.html
- 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