Relaxed Memory Model Zoo

C++20 Memory Model
← Back to the map

C++20 Memory Model

2020 · Boehm, Giroux, Vafeiadis · language, formal, standard · axiomatic formalism

The C++ memory model as revised for C++20. It adopts the repaired sequential-consistency semantics of Lahav et al. (P0668), strengthening seq_cst atomics and fences so the broken IRIW / SC-fence behaviours of C++11/14/17 become forbidden; and it weakens release sequences (P0982) so that only RMWs — not later relaxed stores by the same thread — continue them. It still does not resolve the thin-air problem, so out-of-thin-air reads remain (unlike RC11). The seq_cst strengthening and the release-sequence weakening pull in opposite directions, leaving C++20 incomparable with the original C11/C++11 model and strictly weaker than RC11. This is also the model Rust normatively adopts for core::sync::atomic: the shipped Rust atomics model is C++20 (not full RC11 — see ORC11, the stronger operational RC11 used to verify Rust's standard library).

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
  • Repaired C11 (RC11) — C++20 adopts RC11's repaired SC (P0668) but, unlike RC11, does not adopt the no-thin-air axiom acyclic(po ∪ rf): it still permits out-of-thin-air / plain load-buffering reads that RC11 forbids. So RC11 is strictly stronger.
Incomparable with
  • C11/C++11 Memory Model — Two-sided, both directions mechanised under herd7. C++20's repaired seq_cst (P0668) forbids the IRIW/SC-fence behaviour C11/C++11/14/17 allow (rc11.cat Never vs c11_orig.cat Sometimes). C++20's weakened release sequences (P0982 — only RMWs continue a release sequence) make the models incomparable on the release axis too: the all-atomic mp-rs-add-est-atomic is allowed under C++11/17 but forbidden under C++20 (cpp11/cpp17 Sometimes vs cpp2w Never), while the original RS pattern flips the other way (cpp11 Never vs cpp2w Sometimes, the C++20 outcome now a data race). Checked against the cpp11/cpp17/cpp2w cat models in litmus/models/cpp, vendored from gonzalobg/cpp_memory_model. Neither contains the other.

References

  • Hans-J. Boehm, Olivier Giroux, Viktor Vafeiadis. P0668R5: Revising the C++ Memory Model. ISO/IEC JTC1/SC22/WG21, 2018. wg21.link/p0668
  • Hans-J. Boehm. P0982R1: Weaken Release Sequences. ISO/IEC JTC1/SC22/WG21, 2018. wg21.link/p0982
  • 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
  • ISO/IEC. ISO/IEC 14882:2020 — Programming Language C++. ISO Standard, 2020. www.iso.org/standard/79358.html