Skip to content

Instantly share code, notes, and snippets.

@yohhoy
Created October 15, 2026 14:46
Show Gist options
  • Select an option

  • Save yohhoy/fc45464809466c4a47e0bb2a90c45064 to your computer and use it in GitHub Desktop.

Select an option

Save yohhoy/fc45464809466c4a47e0bb2a90c45064 to your computer and use it in GitHub Desktop.

C++20のseq_cst修復(P0668R5)をていねいに読む

調査日: 2026年10月15日

調査モデル : Opus 5.5

元記事: C++メモリモデルの変遷(C++11〜C++26)の「C++20 : seq_cstとリリースシーケンスの修復」節

この文書について

対象読者

  • atomicとmemory_orderを使ったことがある(あるいは名前は知っている)C++プログラマ。
  • 「happens-before」「全順序S」のような規格の用語には、まだ馴染みがない人。

必要な用語は第1章で一から説明する。

この文書で分かること

C++20で、メモリモデルのうち memory_order::seq_cst(逐次一貫性)の定義 が書き直された。提案文書はP0668R5である。この文書では、次の4点を順に説明する。

  1. 何が壊れていたのか(第2〜4章)
  2. どう直したのか(第3〜4章)
  3. 直し方にまだ誤りが残っていること(第5〜6章)
  4. その後のC++23・C++26での変化と、実務での注意点(第7〜8章)

表記

  • 規格の条文は、安定名と段落番号で「[atomics.order]/4」のように書く。段落の中の箇条は「[atomics.order]/4.1」のように書く(規格の(4.1)項)。
  • 特に断らない限り、条文の番号はC++20(N4868)のものである。C++17やC++26の条文を指すときは、そのつど明記する。
  • 「3.3節」のように「節」が付く番号は、この文書の節番号である。
  • 標準ライブラリの名前は、名前空間stdの修飾を省略して書く(例: atomic<int>、memory_order::seq_cst)。

まとめ

  • C++11のseq_cstの定義には、強すぎる部分 と 弱すぎる部分 があった。
    • 強すぎる部分: PowerなどのCPU上の現実のコンパイラが守れない約束をしていた。C++20で弱めた。
    • 弱すぎる部分: seq_cstフェンスが、実際のCPUが提供する保証よりも弱く定義されていた。C++20で強めた。
  • どちらも、論文「Repairing Sequential Consistency in C/C++11」(PLDI 2017)に基づく修正である。
  • ただし、C++20の条文は論文を写し損ねており、今度は x86上で実際に起こる結果を禁止してしまっている。この問題はLWG3941として報告されており、2026年10月時点で未解決である。
  • 実用上の目安: 1つのアトミック変数には、seq_cstとそれ以外(release/acquire/relaxed)を混ぜて使わない。混ぜなければ、これらの問題の影響は受けない。

第1章 予備知識

1.1 なぜ「メモリモデル」が必要なのか

1つのスレッドの中では、プログラムは書いた順に実行されるように見える。しかし実際には、コンパイラもCPUも、結果が変わらない範囲で命令の順序を入れ替えている。

この入れ替えは、別のスレッドから観測すると見えてしまうことがある。有名な例が次の「Store Buffering(SB)」である。x、yの初期値はどちらも0とする。

atomic<int> x{0}, y{0};

// スレッド1
x.store(1, memory_order::relaxed);
int a = y.load(memory_order::relaxed);

// スレッド2
y.store(1, memory_order::relaxed);
int b = x.load(memory_order::relaxed);

2つのスレッドの命令を、どう交互に並べて実行しても、a == 0 かつ b == 0 にはならないように思える。どちらかのストアが先に実行されれば、後のスレッドのロードはその1を読むはずだからである。

ところが、x86を含む多くのCPUでは、a == 0 かつ b == 0 が実際に起こる。CPUは書き込みをいったん「ストアバッファ」という一時置き場に入れ、メモリへの反映を後回しにするからである。両スレッドのストアがまだバッファにあるうちに、両スレッドがロードを実行すれば、どちらも古い値0を読む。

どの結果が起こりうるのかを決めておかないと、マルチスレッドのプログラムは書けない。それを定めるのが、規格のメモリモデルである(C++20では[intro.races]と[atomics.order])。

1.2 memory_orderの種類

C++では、アトミック操作ごとに、どれだけの順序保証が要るかをmemory_orderで指定する。弱い順に並べると次のとおりである。

指定 ざっくりした意味 主な用途
relaxed その変数への操作が不可分であることだけを保証する。他の変数との順序は保証しない カウンタ
acquire(ロード)/release(ストア) releaseストアの値をacquireロードが読むと、ストアより前の書き込みが、ロードより後から見えるようになる フラグによるデータの受け渡し
acq_rel RMW操作(後述)でacquireとreleaseを兼ねる ロックの実装など
seq_cst 上記に加えて、すべてのseq_cst操作が 全スレッドで同じ1つの順序 で起きたように見える 既定値。最も分かりやすい

(consumeもあるが、C++26で非推奨になったので、ここでは扱わない。)

先ほどのSBの例で、4つの操作をすべてseq_cstにすると、a == 0 かつ b == 0 は禁止される。その代わり、x86ではseq_cstストアがMOV+MFENCE(フェンス命令)か、暗黙にフェンスの効果を持つXCHGにコンパイルされ、ストアバッファを空にしてから次へ進むようになる。

1.3 リトマステストの読み方

この文書には、上のSBのような小さなプログラムが何度も出てくる。これを リトマステスト と呼ぶ。リトマステストは、「この結果は起こりうるか?」を問うための最小のプログラムである。

  • x、y、zはatomic<int>で、初期値は特に断らない限りすべて0とする。a、b、cやr1〜r4はスレッドごとのローカル変数である。
  • コメントの// 1やa == 0は、「その読み込みがこの値を読んだとする」という意味である。
  • 問いは、「1回の実行の中で、すべての読み込みがコメントのとおりの値を読むことは、規格上許されるか(起こりうるか)」である。

テスト名(SB、Z6.U、RWC+syncsなど)は、メモリモデル研究で使われている慣用名である。

1.4 用語集

この文書で使う関係を、例とともに説明する。どれも、ある実行の中の2つの操作AとBの間の関係である。

用語 記号 意味 例
sequenced-before sb 同じスレッドの中で、AがBより先に書かれている 1行目のストアと2行目のロード
reads-from rf ロードBが、ストアAの書いた値を読んだ x.store(1)の1をx.load()が読む
変更順序(modification order) mo 1つの変数への書き込みが並ぶ順序。全スレッドが同じ順序を見る x=1の後にx=2が書かれた
synchronizes-with sw releaseストアAの値を、acquireロードBが読んだ。2つのスレッドが「同期した」(正確には、Aに続くRMW操作の値を読んだ場合や、フェンスを介する場合も含む) flag.store(true, release) → flag.load(acquire)
happens-before hb sbとswを矢印として、AからBへたどり着ける スレッド1でデータを書き、フラグをreleaseストアし、スレッド2がフラグをacquireロードしてからデータを読む
全順序S S すべてのseq_cst操作(seq_cstフェンスを含む)を一列に並べた順序。全スレッドがこの順序に合意する —
RMW操作 — 読み込みと書き込みを不可分に行う操作 fetch_add、compare_exchange_strong

happens-beforeは、「AがBより確実に先に起き、Aの結果がBから見える」という関係である。データ競合があるかどうかは、この関係で判定する([intro.races]/21、C++20)。

(C++20の正式な定義には、consumeによる順序づけも含まれる。この文書ではconsumeを扱わないので、「sbとswをたどれる」と理解しておけばよい。C++26では、定義そのものがこの形になった(第7章)。)

全順序S が、この文書の主役である。seq_cstは「すべてのseq_cst操作が、全スレッドで同じ1つの順序で起きたように見える」ことを約束する。規格はこれを、「次の条件を満たす一列の並びSが存在する」という形で書いている。条件を満たすSを1つも作れない実行は、起こらない(禁止される)。

つまり、リトマステストの結果が許されるかどうかは、次のパズルで判定できる。

判定の手順: 条件として「SでAはBより前」という矢印を集める。矢印をすべて満たす一列の並びを作れれば、その結果は許される。矢印が輪(循環)になっていれば作れないので、その結果は禁止される。

この文書の例は、すべてこのパズルとして解いていく。

ただし、このパズルが判定するのは全順序Sに関する条件だけである。結果が許されるには、そのほかの規則(1つの変数についての読み書きの一貫性(coherence)、RMW操作の原子性など)も満たす必要がある。この文書の例では、各章の「実行の様子を整理する」段階で、そちらの規則を満たす実行を先に確定させている。

1.5 コンパイルの「マッピング」と、CPUのフェンス命令

コンパイラは、アトミック操作を、CPUごとに決まった命令列に置き換える。この対応表を マッピング と呼ぶ。マッピングは、規格が約束したことをCPU上で必ず守れるように作らなければならない。守れないマッピングを、この文書では「不健全」と呼ぶ。

この文書に出てくるフェンス命令は次のとおりである。

CPU 命令 性質
x86 MFENCE 完全なフェンス。ストアバッファを空にする
Power sync(hwsync) 重いが強いフェンス
Power lwsync 軽いが弱いフェンス。「先に書いたもの → 後に読むもの」の順序などを保証しない
ARMv7 dmb 完全なフェンス

第2章 何が壊れていたのか: 全体像

2017年の論文「Repairing Sequential Consistency in C/C++11」(PLDI 2017。論文ページ、PDF)が、C/C++11のseq_cstの定義に2つの問題があることを示した。この論文は、修正したモデルをRC11(Repaired C11)と名づけている。以下、この論文を「RC11論文」と呼ぶ。

問題 何がまずいか C++20での対応
問題1 定義が 強すぎた 同じ変数にseq_cstとrelease/acquireを混ぜると、規格が禁じる結果を、Powerの現実のコンパイラ(GCC・LLVM)が生む 定義を弱めた(第3章)
問題2 seq_cstフェンスが 弱すぎた 実際のCPUのフェンスなら防げる結果を、規格は許してしまっていた。フェンスを全箇所に入れても、逐次一貫性に戻らなかった 定義を強めた(第4章)

P0668R5(2018-11-09)は、この論文に「大きく依拠」して、規格の文言を書き直した。P0668R5は2018年11月のSan Diego会議で採択され、C++20のドラフトN4791に入った(N4792 Editors' Report、CWG motion 2)。

なお、P0668R5の冒頭は、メモリモデルの問題をほかに3つ挙げている。リリースシーケンス(P0982R1に分離)、OOTA、consumeである。この文書では、seq_cstの2つの問題だけを扱う。


第3章 問題1: 定義が強すぎた(Z6.U)

3.1 例題

P0668R5が、RC11論文のFig. 3から借りている例である。

// スレッド1
x.store(1, memory_order::seq_cst);         // W1
y.store(1, memory_order::release);         // W2  ← ここだけrelease

// スレッド2
b = y.fetch_add(1, memory_order::seq_cst); // F   b == 1(W2の値を読み、2を書く)
c = y.load(memory_order::relaxed);         // L   c == 3

// スレッド3
y.store(3, memory_order::seq_cst);         // W3
a = x.load(memory_order::seq_cst);         // R   a == 0

問い: b == 1、c == 3、a == 0 は起こりうるか?

ポイントは、変数yにseq_cst(F、W3)とrelease(W2)が混ざっていることである。

3.2 まず、実行の様子を整理する

yに書き込まれた順序(変更順序)を決める。

  1. Fはfetch_addなので、yの「その時点の最新値」を読んで書く(RMW操作の性質、[atomics.order]/10、C++20)。Fは1を読んだので、FはW2(1を書いた)の直後に来る。
  2. Lは、同じスレッドでFの後にある。ある書き込み(ここではFが書いた2)にhappens-beforeする読み込みは、その書き込みより古い値を読めない(write-read coherence、[intro.races]/18、C++20)。Lが3を読んだのだから、W3(3を書いた)はFより後に来る。
  3. よって、yの変更順序は「初期値0 → W2(1) → F(2) → W3(3)」で確定する。

RC11論文は、この順序はアクセスが全部relaxedでも同じになる、と述べている。

同期の関係を整理する。

  • W2(release)が書いた1をF(seq_cstなのでacquireを兼ねる)が読んだので、W2とFは同期する(synchronizes-with)。
  • よって「W1 →(sb)→ W2 →(sw)→ F」とつながり、W1はFにhappens-beforeする。
  • 一方、スレッド3は誰とも同期していない(Lはrelaxedなので同期を作らない)。したがって、W1はRにhappens-beforeしない。Rが古い値0を読むこと自体は、この時点では禁止されていない。
flowchart LR
  subgraph T1[スレッド1]
    W1["W1: x = 1<br/>seq_cst"] -->|sb| W2["W2: y = 1<br/>release"]
  end
  subgraph T2[スレッド2]
    F["F: y.fetch_add<br/>seq_cst<br/>1を読み2を書く"] -->|sb| L["L: y を読む<br/>relaxed<br/>3を読む"]
  end
  subgraph T3[スレッド3]
    W3["W3: y = 3<br/>seq_cst"] -->|sb| R["R: x を読む<br/>seq_cst<br/>0を読む"]
  end
  W2 ==>|"rf + sw(同期)"| F
  F -.->|"yの変更順序"| W3
  W3 -.->|rf| L
Loading

3.3 C++17までの規則で解く: 禁止される

C++17までの規格は、全順序Sに次の条件を課していた。

Sは「happens-before」とも、各変数の変更順序とも矛盾してはならない。また、seq_cstロードは、Sで自分より前にある最後のseq_cst書き込みの値(またはそれ以外の一部の書き込みの値)を読む。

— [atomics.order]/3(C++17)の要約。原文は付録A

この条件から、Sについて次の矢印が得られる。

番号 矢印 理由
(1) R → W1 Rはxの0を読んだ。Sの中でW1(x = 1)がRより前にあったら、Rは1を読まなければならない。だからRはW1より前
(2) W1 → F W1はFにhappens-beforeする(3.2節)
(3) F → W3 yの変更順序でFはW3より前
(4) W3 → R 同じスレッドの中でW3はRより前(sbはhappens-beforeに含まれる)
flowchart LR
  R["R: a = x"] -->|"(1)"| W1["W1: x = 1"]
  W1 -->|"(2) happens-before"| F["F: fetch_add"]
  F -->|"(3) 変更順序"| W3["W3: y = 3"]
  W3 -->|"(4) 同じスレッド"| R
  linkStyle 0,1,2,3 stroke:#d33,stroke-width:2px
Loading

矢印が R → W1 → F → W3 → R と輪になるので、Sを作れない。したがって、この結果は禁止される。

3.4 ところが、Powerでは実際に起こる

Power向けのGCC・LLVMは、アトミック操作を次のようにコンパイルする(RC11論文Fig. 9–10、Cambridgeの対応表)。

操作 Powerの命令列
releaseストア lwsync; st
seq_cstストア sync; st
seq_cstロード sync; ld; cmp; bc; isync
seq_cst RMW sync; + RMWのループ + isync

seq_cst操作の 前に syncを置くので、この方式を「leading sync方式」と呼ぶ。

この例をコンパイルすると、syncの多くはスレッドの先頭に来るので、何も順序づけない。スレッド1でW1とW2の間にあるのは、W2(release)のための軽いlwsyncだけである。P0668R5は、lwsyncには「スレッド1のx = 1を、スレッド3にも見えるようにする」だけの強さ(累積性)が無いと説明している。RC11論文も、有効に働くsyncは1つしか残らず、それもlwsync程度の効果しか持たないと説明している。

結果として、Powerでは 規格が禁止している結果が実際に起こる。規格とコンパイラのどちらかが間違っていることになる。

RC11論文は、もう一方の「trailing sync方式」(seq_cst操作の 後に syncを置く方式)も、別の例(IRIW-acq-sc)で壊れることを示した。つまり、どちらの方式でも、C++11の規格は守れていなかった。2012年に発表されていた「Powerへのコンパイルは正しい」という証明には、この条件の確認漏れがあった(RC11論文§9)。

他のCPUの状況は次のとおりである(P0668R5、RC11論文§1・§6)。

  • ARMv7: GCCとLLVMはacquireロードに重いフェンス(dmb)を使うので、問題は起こらない。
  • ARMv8: P0668R5によれば、通常はacquire/releaseをseq_cstと同じ命令でコンパイルするので、現状は問題ない。ただしRC11論文は、ARMv8でも同種の問題が起こる例があるとしている(§1。例は論文の補遺[3]にあり、この文書では未確認)。
  • NVIDIA GPU: Powerと同じ問題を抱え、直すコストはさらに大きい。

3.5 どちらを直すか

P0668R5は、2つの選択肢を比べた。

  1. コンパイラを直す: releaseストアに軽いlwsyncを使えなくなる。acquire/releaseを使う理由(速さ)の大半が失われる。releaseしか使えない別の型を追加する案もあったが、APIが増えることに懸念があった。非公式の調査でも不人気だった。
  2. 規格を直す: RC11論文が提案した方法。P0668R5はこちらを採った。

P0668R5によれば、この問題は理論的な解析で見つかったもので、バグ報告から見つかったものではない。また、各変数をseq_cstだけで、または弱いオーダーだけでアクセスするコードは、影響を受けない。

3.6 どう直したか: strongly happens-before

問題の根は、(2)の矢印「W1 → F」にある。この矢印は、途中にrelease→acquireの同期(sw)を含むhappens-beforeから来ている。Powerのコンパイル結果では、こうした経路の上に重いsyncが置かれる保証が無い。

RC11論文は、どういうhappens-beforeの経路なら、途中に必ずsyncが入るかを考えた。答えは、経路が同じスレッド内の順序(sb)で始まり、sbで終わる場合 である。そこで、全順序Sが従うべき順序を、次のように狭めた。

  • 同じスレッドの中の順序(sb)には、これまでどおり従う。
  • 同期をはさむ場合は、前後がsbで挟まれているか、同期の両端がseq_cst操作である場合だけ従う。

C++20は、この狭めた順序を strongly happens-before と名づけた。

AがDにstrongly happens-beforeするのは、次のいずれかのときである。

  • (12.1) AがDにsequenced-beforeする(同じスレッドで先)。
  • (12.2) AがDとsynchronizes-withし、AとDがともにseq_cst操作である。
  • (12.3) ある評価B、Cについて、AがBにsequenced-beforeし、BがCにsimply happens-beforeし、CがDにsequenced-beforeする(前後をsbで挟んだ経路)。
  • (12.4) ある評価Bについて、AがBにstrongly happens-beforeし、BがDにstrongly happens-beforeする(推移閉包)。

— [intro.races]/12(C++20)の訳。括弧内の補足はこの文書によるもの。原文は付録A

[intro.races]/12.3の「simply happens-before」は、consumeを使わない限りhappens-beforeと同じものと考えてよい。C++26では名前も「happens-before」に統一された(第3章末尾の余談)。

そして、全順序Sの条件は「happens-beforeに従う」から「strongly happens-beforeに従う」に変わった([atomics.order]/4の前半、C++20)。規格には、次の注記も新設された。

Sは「happens-before」と整合することを要求しない。これにより、一部のアーキテクチャでacquire/releaseを効率よく実装できる。ただし、seq_cstと混ぜると驚くような結果が起こりうる。

— [atomics.order]/6(C++20)の要約

注意: [intro.races]/12.3で前後を挟む操作(AとD)のメモリオーダーは問わない。前後をseq_cst操作で挟む必要があるわけではない。

3.7 C++20の規則で解き直す: 許される

W1とFの間は、W1 →(sb)→ W2 →(sw)→ F である。これがstrongly happens-beforeかどうかを、定義の各項で確かめる。

  • [intro.races]/12.1: W1とFは別スレッドなので、該当しない。
  • [intro.races]/12.2: W1とFは直接同期していない。同期しているのはW2とFだが、W2はreleaseでありseq_cstではない。
  • [intro.races]/12.3: 「W1 →(sb)→ B →(happens-before)→ C →(sb)→ F」という形の経路が要る。つまり、スレッド2の中にFより前の評価Cが必要である。しかし、Fはスレッド2の最初の操作なので、そのようなCは無い。
  • [intro.races]/12.4: 途中の評価を経由する場合も同じである。W1から出る経路はW2を通るしかなく、W2からFへのstrongly happens-beforeは、上と同じ理由([intro.races]/12.2・[intro.races]/12.3が使えない)で成立しない。

したがって、W1はFにstrongly happens-beforeしない。

よって、矢印(2)は消える。ほかの矢印は、C++20でも引き続き得られる。

  • 矢印(4)(W3 → R): [intro.races]/12.1により、W3はRにstrongly happens-beforeする。
  • 矢印(3)(F → W3)と矢印(1)(R → W1): 同じ変数上の「歴史」の順序(coherence-ordered-before)で結ばれたseq_cst操作どうしなので、[atomics.order]/4.1から得られる(4.4節で説明する。(1)には下の補足の注意がある)。

残る矢印(1)(3)(4)だけなら、たとえば S = F → W3 → R → W1 という並びが作れる。

flowchart LR
  F["F: fetch_add"] -->|"(3)"| W3["W3: y = 3"]
  W3 -->|"(4)"| R["R: a = x"]
  R -->|"(1)"| W1["W1: x = 1"]
Loading

この並びではRがW1より前にあるので、Rが0を読むことにも矛盾しない。よって、C++20ではこの結果は許される。規格が、Powerの現実のコンパイラに合わせて弱められたわけである。

補足:

  • W1はLにはstrongly happens-beforeする([intro.races]/12.3で、A = W1、B = W2、C = F、D = L)。ただし、Lはrelaxedなので全順序Sに参加せず、影響はない。
  • (1)の矢印の根拠「Rは初期値0を読んだ」には、細かな条文上の疑義がある。C++20の規定は「アトミックな変更の値を読んだ」場合を想定しているのに、atomicの初期化は「アトミック操作ではない」とされているからである。この点はLWG4174として審議中である。ただし、矢印が1本減っても並びは作りやすくなるだけなので、「許される」という結論は変わらない。

余談: 用語「strongly happens-before」の変遷

本論からは外れるが、用語の変遷を記しておく。strongly happens-beforeという用語自体は、C++17でP0250R3が静的変数の初期化順序などを定めるために導入していた([intro.races]/11、C++17)。C++20のP0668R5は、この旧定義を simply happens-before に改名し、同じ名前に3.6節の新しい定義を与えた。C++26では、consumeの削除(P3475R2)に伴い、simply happens-beforeが「happens-before」に改名された(第7章)。


第4章 問題2: seq_cstフェンスが弱すぎた

4.1 seq_cstフェンスとは

atomic_thread_fence(memory_order::seq_cst)は、seq_cstフェンスを置く関数である。relaxedなアクセスの間にこのフェンスを置くと、フェンスの前後で順序が保たれることが期待される。たとえば1.1節のSBで、各スレッドのストアとロードの間にseq_cstフェンスを置くと、a == 0 かつ b == 0 は禁止される。これはC++11から変わらない。

4.2 C++17までの規則の弱さ

C++17までの規則([atomics.order]/4–7、C++17)は、フェンスについて次のような場合しか定めていなかった。

  • フェンスの 前に同じスレッドで書いた値 が、他スレッドのフェンスの後の読み込みに見えるか。
  • フェンスの後の読み込みが、seq_cstで書かれた値 を見るか。

規格自身も、注記で次のように認めていた。

seq_cstフェンスは、フェンスどうしの全順序しか保証しない。フェンスは一般に、弱いオーダーのアトミック操作に逐次一貫性を回復させるためには使えない。

— [atomics.order]/8(C++17)の要約

この規則には抜けがある。フェンスを持たない別スレッドがrelaxedで書いた値 について、何も言えないのである。

4.3 例題: RWC+syncs(RC11論文Fig. 5)

すべてのアクセスはrelaxedとする。

// スレッド1
x.store(1, memory_order::relaxed);           // Wx

// スレッド2
a = x.load(memory_order::relaxed);           // Ra   a == 1
atomic_thread_fence(memory_order::seq_cst);  // F2
b = y.load(memory_order::relaxed);           // Rb   b == 0

// スレッド3
y.store(1, memory_order::relaxed);           // Wy
atomic_thread_fence(memory_order::seq_cst);  // F3
c = x.load(memory_order::relaxed);           // Rc   c == 0

問い: a == 1、b == 0、c == 0 は起こりうるか?

直感的には、次の理由でおかしな結果である。

  • スレッド2は、x = 1を見た(a == 1)のに、フェンスの後でy = 1をまだ見ていない(b == 0)。
  • スレッド3は、y = 1を書いてフェンスを置いたのに、その後でx = 1をまだ見ていない(c == 0)。
  • 2つのフェンスのどちらが先だったとしても、どちらかのスレッドが、もう一方の書き込みを見ているはずである。

C++17までの規則では許されていた。

  • yについて: Wyはフェンスの前に同じスレッドで書いた値なので、規則が適用される。F3がF2より先なら、Rbは1を読まなければならない。b == 0なので、F2がF3より先と決まる。
  • xについて: Wxを書いたスレッド1にはフェンスが無く、Wxはseq_cstでもない。だから、Rcが0を読むことを禁じる規則が無い。

RC11論文は、この結果は規格上は許されるが、「C11のすべての実装で禁止される」と述べ、「標準の重大な欠落」と呼んでいる。実害の報告もある。論文(§2.2)が紹介する先行研究によれば、Chase-Levデック(work-stealing用のデータ構造)の実装で、この弱さのために、本来不要なseq_cstをrelaxedな書き込みに使わざるを得なかった。

P0668R5によれば、フェンスがこう弱く定義されたのは、当初は意図的で、Itaniumに対応するためだった。Itaniumのフェンスは、全箇所に入れても逐次一貫性を保証しない。しかしRC11論文(Remark 2)とP0668R5によれば、Itaniumではrelaxedでも結局は強い命令を使う必要があり、その場合はフェンスも十分に働く。既知のseq_cstフェンスの実装は、すべてより強い意味論を提供している。

4.4 どう直したか: coherence-ordered-before

C++20は、新しい関係 coherence-ordered-before を導入した([atomics.order]/3、C++20)。

これは、1つの変数の「歴史」の中で、AがBより前の時点に位置する ことを表す関係である。具体的には、同じ変数M上の操作AとBについて、次のいずれかが成り立つときを言う(表の「項」は条文の項番号)。

項 条件 直感的な意味
3.1 Aが書き込みで、BがAの値を読んだ 書いてから、読まれた
3.2 変更順序でAがBより前 先に書かれた
3.3 Aが書き込みXの値を読み、変更順序でXがBより前(ただし、AとBが同じRMW操作である場合を除く) Aは、Bより古い値を読んだ(Bの書き込みを「まだ見ていない」)
3.4 ある書き込みXについて、AがXより前で、XがBより前(推移閉包) 上の関係をつなげたもの

[atomics.order]/3.3が重要である。「古い値を読んだ読み込みは、新しい書き込みより前」とみなす。研究では「reads-before」や「from-read」と呼ばれる。

そのうえで、全順序Sに次の条件を課した。

同じ変数上の操作AとBで、AがBにcoherence-ordered-beforeする組それぞれについて、Sは次の4条件を満たす。

  • (4.1) AとBがともにseq_cst操作なら、SでAはBより前。
  • (4.2) Aがseq_cst操作で、Bがseq_cstフェンスYにhappens-beforeするなら、SでAはYより前。
  • (4.3) seq_cstフェンスXがAにhappens-beforeし、Bがseq_cst操作なら、SでXはBより前。
  • (4.4) seq_cstフェンスXがAにhappens-beforeし、Bがseq_cstフェンスYにhappens-beforeするなら、SでXはYより前。

— [atomics.order]/4(C++20)後半の訳。原文は付録A

[atomics.order]/4.4を言葉にすると、「フェンスXの後でAが起き、フェンスYの前でBが起き、AがBより変数の歴史の上で前にあるなら、XはYより前」となる。

ここで、AやBがrelaxedでもよく、別スレッドが書いた値が絡んでもよい。これが、C++17との大きな違いである。

4.5 RWC+syncsを解き直す: 禁止される

  • yについて: Rbは初期値0を読んだ。Wy(y = 1)は変更順序で初期値より後なので、[atomics.order]/3.3によりRbはWyにcoherence-ordered-beforeする。F2はRbの前(同じスレッド)、WyはF3の前(同じスレッド)なので、[atomics.order]/4.4により F2 → F3。
  • xについて: Rcは初期値0を読んだので、RcはWxにcoherence-ordered-beforeする([atomics.order]/3.3)。WxはRaに読まれたので、WxはRaにcoherence-ordered-beforeする([atomics.order]/3.1)。つなげると、RcはRaにcoherence-ordered-beforeする([atomics.order]/3.4)。F3はRcの前、RaはF2の前なので、[atomics.order]/4.4により F3 → F2。
flowchart LR
  F2["F2: スレッド2のフェンス"] -->|"y: Rb は古い値を読んだ"| F3["F3: スレッド3のフェンス"]
  F3 -->|"x: Rc は古い値を読んだ"| F2
  linkStyle 0,1 stroke:#d33,stroke-width:2px
Loading

F2 → F3 と F3 → F2 が両方必要になるので、Sを作れない。よって、C++20ではこの結果は禁止される。

(Rb・Rcが初期値を読むことから[atomics.order]/3.3を使う点には、3.7節の補足と同じLWG4174の疑義がある。スレッドを起動する前にx.store(0)・y.store(0)を実行しておけば、アトミックな書き込みを読むことになり、同じ結論になる。)

4.6 もう一つの例: W+RWC(累積性、RC11論文Fig. 6)

RWC+syncsのxへの書き込みを、release/acquireの同期を経由して届くように変えた例である。

// スレッド1
x.store(1, memory_order::relaxed);           // Wx
z.store(1, memory_order::release);           // Wz

// スレッド2
a = z.load(memory_order::acquire);           // a == 1(Wzを読み、スレッド1と同期)
atomic_thread_fence(memory_order::seq_cst);  // F1
b = y.load(memory_order::relaxed);           // Rb   b == 0

// スレッド3
y.store(1, memory_order::relaxed);           // Wy
atomic_thread_fence(memory_order::seq_cst);  // F2
c = x.load(memory_order::relaxed);           // Rc   c == 0

スレッド2は、zを通じてスレッド1と同期しているので、x = 1の書き込みもスレッド2の「知っていること」に含まれるはずである。フェンスが、自スレッドが書いたものだけでなく、自スレッドが 知った 他スレッドの書き込みも順序づけるという性質を、累積性(cumulativity)と呼ぶ。RC11論文によれば、x86・Power・ARMのフェンスは累積的なので、この結果はハードウェアでは起こらない。

C++20とC++17の規則で解くと、次のようになる(この節の判定は、論文ではなくこの文書での検証である)。

  • yについて: RWC+syncsと同じ理由で F1 → F2。
  • xについて: RcはWxにcoherence-ordered-beforeする。WxはF1にhappens-beforeする(Wx →(sb)→ Wz →(sw)→ aのロード →(sb)→ F1)。F2はRcにhappens-beforeする。[atomics.order]/4.4により F2 → F1。

輪になるので、禁止される。[atomics.order]/4.4が「同じスレッドの順序(sb)」ではなく「happens-before」で書かれているおかげで、同期を経由して届いた書き込みも順序づけの対象になる。C++17の規則では、Wxはフェンスの前に同じスレッドで書かれた値ではないので、制約がかからず、許されていた。

4.7 その他の変化

  • 「フェンスはフェンスどうしの全順序しか保証しない」という旧注記は、正しくなくなったので削除された。代わりに、「多くの場合、seq_cstのアトミック操作は、同じスレッドの他のアトミック操作との間で順序を入れ替えうる」という注記が入った([atomics.order]/7、C++20)。
  • 書き方の発想も変わった。C++17は、全順序Sを使って「どの値が読めるか」を定めていた。C++20は逆に、実際に読まれた値(coherence-ordered-before)から、Sへの条件を導く。条件を満たすSが無ければ、その実行は起こらない(P0668R5の説明)。
  • seq_cstフェンスは、C++11の時点でも全順序Sに含まれていた。当時の条文も、フェンスのS上の位置を使って書かれており、LWG2130(C++14)の議論でも「seq_cstフェンスはSに含まれる」と述べられている。C++20の変更は、「including fences」と明記したことと、フェンスの条件を一般化したことである。

第5章 直し方に残った誤り: LWG3941

5.1 何が起きたのか

第3章・第4章の修正は、RC11論文が提案したモデルRC11を規格の文章に「翻訳」したものである。ところがこの翻訳には誤りがあり、C++20の規格は、論文のモデルより強い約束 をしてしまった。その結果、x86で実際に起こる結果を、規格が禁止している。

5.2 例題: SB+rfis(RC11論文Remark 4)

1.1節のSBに、自分が書いた変数を読み直すロードを足した形である。

// スレッド1
x.store(1, memory_order::release);
r1 = x.load(memory_order::seq_cst);  // r1 == 1(自分の書いた値)
r2 = y.load(memory_order::seq_cst);  // r2 == 0

// スレッド2
y.store(1, memory_order::release);
r3 = y.load(memory_order::seq_cst);  // r3 == 1(自分の書いた値)
r4 = x.load(memory_order::seq_cst);  // r4 == 0

問い: r1 == 1、r2 == 0、r3 == 1、r4 == 0 は起こりうるか?

5.3 x86では実際に起こる

GCC・LLVMのx86向けマッピング(RC11論文Fig. 8)では、フェンスの効果を持つ命令が入るのは、seq_cstストア(MOV+MFENCE、またはXCHG)、seq_cstフェンス(MFENCE)、RMW操作(LOCK付き命令)だけである。releaseストアもseq_cstロードも、ただのMOVになる。この例にはそのどれも無いので、フェンスは1つも入らない。

x86では、各スレッドの書き込みはまずストアバッファに入る。スレッドは自分のストアバッファの値を先に読める(ストアフォワーディング)。そのため、次のような実行が起こる。

  1. スレッド1のx = 1と、スレッド2のy = 1が、それぞれのストアバッファに入る。まだメモリには反映されていない。
  2. スレッド1は、自分のバッファからx = 1を読む(r1 == 1)。メモリのyはまだ0なので、r2 == 0。
  3. スレッド2も同様に、r3 == 1、r4 == 0。

5.4 C++20の規格では禁止されてしまう

C++20の規則([atomics.order]/3–4)で解く。登場するseq_cst操作は、4つのロード(r1〜r4)である。

  • 同じスレッドの順序(strongly happens-before): r1 → r2、r3 → r4。
  • yの歴史(coherence-ordered-before):
    • r2は初期値0を読んだので、スレッド2のy = 1(release)より前([atomics.order]/3.3)。
    • そのy = 1はr3に読まれたので、r3より前([atomics.order]/3.1)。
    • つなげると、r2はr3にcoherence-ordered-beforeする([atomics.order]/3.4)。r2とr3はどちらもseq_cstなので、[atomics.order]/4.1により r2 → r3。
  • xの歴史: 同様に r4 → r1。
flowchart LR
  r1["r1: x を読む (1)"] -->|同じスレッド| r2["r2: y を読む (0)"]
  r2 -->|"yの歴史<br/>(release ストアを経由)"| r3["r3: y を読む (1)"]
  r3 -->|同じスレッド| r4["r4: x を読む (0)"]
  r4 -->|"xの歴史<br/>(release ストアを経由)"| r1
  linkStyle 0,1,2,3 stroke:#d33,stroke-width:2px
Loading

r1 → r2 → r3 → r4 → r1 と輪になるので、Sを作れない。したがって、C++20の規格ではこの結果は禁止される。しかしx86では起こるので、GCC・LLVMのx86向けマッピングは、規格の文面に照らすと不健全ということになる。

(r2・r4が初期値を読むことに依拠する点には、3.7節と同じLWG4174の疑義がある。ただし、スレッドを起動する前にx.store(0)・y.store(0)を実行しておけば、初期値ではなくアトミックな書き込みを読むことになり、同じ輪ができる。)

5.5 論文と規格はどこが違うのか

RC11論文のモデル: seq_cstアクセスどうしの順序を「変数の歴史」から導くときは、2つのseq_cstアクセスが変更順序(mo)か「古い値を読んだ」関係(rb)で直接結ばれている場合だけを使う。「古い値を読んだ → 別の書き込みを経て → それを読んだ」のように、非seq_cstの書き込みを間に挟んだ合成は使わない(論文§3のscb、付録B)。論文は§2.2の末尾とRemark 4で、まさにこのSB+rfisを例に挙げ、その合成まで含めるとx86の標準マッピングが不健全になると指摘している(要約)。そのうえで、そうしない設計を選んでいる。

C++20の規格: coherence-ordered-beforeは推移閉包([atomics.order]/3.4)なので、途中にreleaseストアのような非seq_cstの書き込みを挟んでもつながってしまう。そのうえで、両端がseq_cstなら[atomics.order]/4.1がSに順序を課す。これで、論文が避けた経路が規格に入り込んだ。

5.6 LWG3941

この食い違いは、LWG3941「[atomics.order] inadvertently prohibits widespread implementation techniques」(2023-05-27起票、Status: Open、Priority 3)として報告されている。issueの内容は次のとおりである。

  • issueによれば、この問題を発見したのはRC11論文の筆頭著者自身である。
  • 説明に使われている例は、この文書の5.2節と同じSB+rfisである。
  • 影響はx86の「fence-after-store」方式に限られない。「ストアの直後の、同じ変数へのseq_cstロードを省く」というコンパイラ最適化も、この規定に反しうる。
  • issueは、これを「論文を規格の文言へ単純化・翻訳する際の誤り」とし、元の論文には既知の問題は無いとしている。そして、「フェンスだけを強めるつもりが、通常のseq_cst操作の意味まで意図せず強めて、壊してしまった」と述べている。
  • 直し方の候補として、seq_cstフェンスの強化を元に戻す案(望ましくない)と、論文の定式化をそのまま採る案(直感的な説明が難しい)が挙がっている。
  • 2024年3月のSG1(並行性の作業部会)は、「x86のような既存実装を保つ形でLWG3941に対処したい」と全会一致で合意した。ただし、2026年10月時点で修正の文言は無い。

issueには、規格のこの部分を読んでいる人がほぼいないのではないか、という所感も記されている。長い間誰も気づかず、実装者も困らなかったのは、実装者が規格の文章ではなく、専門家が作ったマッピング表に従っているからではないか、という推測である。


第6章 もう一つの相違: 冗長なseq_cst書き込みの削除

この章の内容は、RC11論文と条文をこの文書で比較した結果である。この点を扱った委員会の文書は、今回の調査では見つけられなかった。(関連して、LWG3941は「ストアの直後のseq_cstロードを省く」最適化が規定に反しうることに触れている。この章で扱う「上書きされるseq_cst書き込みの削除」とは別の変換である。)

RC11論文(§2.1.1)は、第3章の修正にさらに手を加えている。目的は、次のようなコンパイラ最適化を正しいものとして認めることである。

  • 同じ変数への連続するseq_cst書き込みのうち、すぐ上書きされる前の方を削除する(x = 1; x = 2; → x = 2;)。
  • 同じ変数への連続するseq_cst読み込みを1回にまとめる。

そのために論文は、3.6節の[intro.races]/12.3(前後をsbで挟む)に「挟むsbは、異なる変数どうしの順序に限る」という限定を付けた。C++20の条文([intro.races]/12)にも、C++26の条文([intro.races]/8)にも、この限定は無い。

論文の例(WWmerge、Fig. 4)にC++20の条文を当てはめると、次のようになる。

// スレッド1
a = x.load(memory_order::acquire);  // k   a == 2
b = y.load(memory_order::seq_cst);  // l   b == 0

// スレッド2
x.store(1, memory_order::seq_cst);  // m   ← 削除したい書き込み
x.store(2, memory_order::seq_cst);  // n

// スレッド3
y.store(1, memory_order::seq_cst);  // o
c = x.load(memory_order::seq_cst);  // p   c == 0
  • mがある場合: m →(sb)→ n →(同期)→ k →(sb)→ l なので、[intro.races]/12.3によりmはlにstrongly happens-beforeする。lはoより前(yの古い値を読んだ)、oはpより前(同じスレッド)、pはmより前(xの古い値を読んだ)。よって m → l → o → p → m と輪になり、禁止。
  • mを削除した場合: nからlへの経路は「同期 → sb」で、前にsbが無い。また、kはacquireなので[intro.races]/12.2も使えない。よって、nはlにstrongly happens-beforeしない。輪ができないので、許される。

削除によって、元のプログラムでは起こらない結果が起こるようになる。つまり、C++20の条文の下では、この最適化は正しくない。RC11論文によれば、GCCとLLVMはこの最適化を行っていないので、現時点で実害は無い。


第7章 C++23・C++26での変化

C++20(N4868)・C++23(N4950)・C++26(N5050)の該当節を比べた。

規格 intro.races atomics.order [atomics.fences]
C++23 文言の手直しのみ 変更なし 変更なし
C++26 consume関連の定義を削除し、simply happens-beforeを「happens-before」に改名([intro.races]/7)。strongly happens-beforeの[intro.races]/8.3も「happens-before」で書かれるようになった([intro.races]/8) 変更なし consumeへの言及を削除。後述のmodify-write操作の例外を追加

C++26の[intro.races]の変更はP3475R2による。 P3475R2はconsumeを非推奨にする提案で、その本文の指示は次のとおりである。

  • consumeのための定義(carries a dependency、dependency-ordered before、inter-thread happens before)と、それらで組み立てていた旧happens-beforeを削除する。
  • 「simply happens before」を「happens before」に改名する。

consumeが無くなれば、旧happens-beforeとsimply happens-beforeは同じものになる。そのため、定義はsimply happens-beforeのものを残し、名前は「happens-before」に一本化した、と読める。ドラフトへの反映はcplusplus/draft PR #7682(2025-02 CWG Motion 6)の差分で確認した。

P3475R2の本文には、ほかに次の記述がある。

  • 旧happens-beforeの定義にあった「happens-beforeに循環があってはならない」という明示の規定も消える。consumeが無ければ、循環を閉じる最後の同期は成立しえないので、問題ない。
  • consumeを削除する理由の一つとして、consumeがメモリモデルを複雑にしているため、consumeを無視する学術研究の成果を規格に取り込みにくいことを挙げている。そのうえで、メモリモデルには「tricky repair(手の込んだ修理)」が必要だと述べている。この修理が第5章のLWG3941を指すかどうかは書かれていないが、関係があると考えられる(この文書の推測)。

C++26の[atomics.fences]の変更はP3111R8(Atomic Reduction Operations)による。 値を返さない新しいアトミック操作(store_addなどのstore_系関数)を「atomic modify-write operation」と位置づけ([atomics.order]/11、C++26)、フェンスによる同期の読み取り側から除外した([atomics.fences]/2、C++26)。全順序Sの定義([atomics.order]/3–7)には影響しない。


第8章 実務ではどうすればよいか

影響を受けないコード

  • すべてseq_cstで書いた、データ競合の無いプログラム: 逐次一貫性が保証される。これはC++11から変わらない([atomics.order]/7、[intro.races]/21の注記、C++20)。
  • 1つのアトミック変数をseq_cstだけで、またはseq_cst以外だけでアクセスするコード: RC11論文は、この場合、修正後のモデル(RC11)のseq_cstの扱いが、先行研究による強化版のモデルと一致することを示している(Proposition 3)。これは論文のモデルについての結果だが、C++20の条文についても、第3章(Z6.U)と第5章(SB+rfis)の現象は、どちらも1つの変数にseq_cstとreleaseを混ぜたときにだけ起こる。

注意が要るコード: 1つの変数にseq_cstとそれ以外を混ぜる

型 規格上 実機 注意
Z6.U型(第3章) C++20で許される Power・NVIDIA GPUで起こる seq_cst操作の順序から、他の変数の値が見えるはずだと推論すると外れうる
SB+rfis型(第5章) C++20の文面では禁止 x86で起こる 規格の文面を信じてこの順序に依存すると、x86で壊れる

混用は珍しいが、正当な使い道もある。RC11論文は実例として、seqlockとRustのcrossbeamライブラリを挙げている。「最初は全部seq_cstで書き、性能が要る箇所だけ弱める」という書き方をすると、混用が生じやすい(P0668R5)。

seq_cstフェンス

relaxedアクセスとseq_cstフェンスを組み合わせる設計は、C++20以降の方が規格上の保証が強い(第4章)。この強化は、実際のCPU(x86、Power、ARMv7)のフェンスがもともと提供していた保証を、規格が追認したものである。RC11論文は、強化後のモデルでも各CPUへのコンパイルが正しいことを証明している。

ライブラリを設計する人へ

P0668R5は、ライブラリが「この呼び出しはあの呼び出しより前」と約束するときは、happens-beforeではなくstrongly happens-beforeを使うべきだとしている。利用者が、その約束とseq_cst操作の順序を組み合わせて推論しても、矛盾しないようにするためである。


第9章 未確認事項・注意

  • 4.6節(W+RWC)と第6章(WWmerge)へのC++20の条文の当てはめは、この文書独自の検証である。RC11論文は、自身のモデルについての結論だけを述べている。
  • 第6章の「C++20の条文の下では冗長なseq_cst書き込みの削除が正しくない」という点は、委員会の文書での言及を見つけられなかった。
  • LWG3941とLWG4174は、2026年10月時点でOpen/SG1である。修正が採択されれば、第3〜6章の判定が変わりうる。
  • C言語(C23)に同等の修正が入ったかどうかは調べていない。

付録A 条文の原文

本文で訳・要約した条文の原文を示す。英文はWeb版(timsong-cpp.github.io)の該当段落と照合した。項番号((3.1)など)は規格のとおりに付け、段落内の注記(Note)は省いた。

C++17 [atomics.order]/3(全順序Sの旧定義)

There shall be a single total order S on all memory_order_seq_cst operations, consistent with the “happens before” order and modification orders for all affected locations, such that each memory_order_seq_cst operation B that loads a value from an atomic object M observes one of the following values:

  • (3.1) the result of the last modification A of M that precedes B in S, if it exists, or
  • (3.2) if A exists, the result of some modification of M that is not memory_order_seq_cst and that does not happen before A, or
  • (3.3) if A does not exist, the result of some modification of M that is not memory_order_seq_cst.

— [atomics.order]/3(C++17)

続く[atomics.order]/4–7(C++17)がフェンスの規則、[atomics.order]/8(C++17)が「Fences cannot, in general, be used to restore sequential consistency ...」を含む注記である。C++11の[atomics.order]/7(N3337の29.3/7)は2つのフェンスを介する場合だけを定めており、1つのフェンスを介する場合はLWG2130(C++14)で追加された。

C++17 [intro.races]/11(旧strongly happens before)

An evaluation A strongly happens before an evaluation B if either

  • (11.1) A is sequenced before B, or
  • (11.2) A synchronizes with B, or
  • (11.3) A strongly happens before X and X strongly happens before B.

— [intro.races]/11(C++17)

C++20 [intro.races]/12(新strongly happens before)

An evaluation A strongly happens before an evaluation D if, either

  • (12.1) A is sequenced before D, or
  • (12.2) A synchronizes with D, and both A and D are sequentially consistent atomic operations ([atomics.order]), or
  • (12.3) there are evaluations B and C such that A is sequenced before B, B simply happens before C, and C is sequenced before D, or
  • (12.4) there is an evaluation B such that A strongly happens before B, and B strongly happens before D.

— [intro.races]/12(C++20)

C++26では同じ定義が[intro.races]/8に移り、[intro.races]/12.3に当たる項の「simply happens before」が「happens before」に変わった。

C++20 [atomics.order]/3(coherence-ordered-before)

An atomic operation A on some atomic object M is coherence-ordered before another atomic operation B on M if

  • (3.1) A is a modification, and B reads the value stored by A, or
  • (3.2) A precedes B in the modification order of M, or
  • (3.3) A and B are not the same atomic read-modify-write operation, and there exists an atomic modification X of M such that A reads the value stored by X and X precedes B in the modification order of M, or
  • (3.4) there exists an atomic modification X of M such that A is coherence-ordered before X and X is coherence-ordered before B.

— [atomics.order]/3(C++20)

C++20 [atomics.order]/4(全順序S)

There is a single total order S on all memory_order::seq_cst operations, including fences, that satisfies the following constraints. First, if A and B are memory_order::seq_cst operations and A strongly happens before B, then A precedes B in S. Second, for every pair of atomic operations A and B on an object M, where A is coherence-ordered before B, the following four conditions are required to be satisfied by S:

  • (4.1) if A and B are both memory_order::seq_cst operations, then A precedes B in S; and
  • (4.2) if A is a memory_order::seq_cst operation and B happens before a memory_order::seq_cst fence Y, then A precedes Y in S; and
  • (4.3) if a memory_order::seq_cst fence X happens before A and B is a memory_order::seq_cst operation, then X precedes B in S; and
  • (4.4) if a memory_order::seq_cst fence X happens before A and B happens before a memory_order::seq_cst fence Y, then X precedes Y in S.

— [atomics.order]/4(C++20)

続く注記は[atomics.order]/5–7(C++20)にある。C++26でも[atomics.order]/3–7は変わらない([atomics.order]、C++26)。

付録B RC11論文の形式的な定義

論文に馴染みのある読者向けに、本文で説明した内容を論文の記法で対応づけておく。記法: sb = sequenced-before、rf = reads-from、mo = 変更順序、rb = rf⁻¹; mo(reads-before)、hb = (sb ∪ sw)⁺、[E^sc]はseq_cstアクセスの集合、[F^sc]はseq_cstフェンスの集合、R|loc は同じロケーション間に限った関係。

C11のSの条件(論文§2)

条件 内容 本文での対応
S1 [E^sc]; hb; [E^sc] ⊆ S 3.3節の(2)(4)
S2 [E^sc]; mo; [E^sc] ⊆ S 3.3節の(3)
S3 [E^sc]; rb; [E^sc] ⊆ S 3.3節の(1)(先行研究による簡略・強化版。論文Remark 1)
S4–7 seq_cstフェンスの条件 4.2節

修正(論文§2.1〜§2.2.1)

  • S1fix: [E^sc]; (sb ∪ sb; hb; sb ∪ hb|loc); [E^sc] ⊆ S。C++20の[intro.races]/12.1〜12.3に当たる(12.2はhb|locのうちseq_cst間のswに当たる)。
  • scb ≜ sb ∪ sb|≠loc; hb; sb|≠loc ∪ hb|loc ∪ mo ∪ rb。sb|≠locへの限定は、C++20には取り込まれていない(第6章)。
  • eco ≜ (rf ∪ mo ∪ rb)⁺。C++20のcoherence-ordered-beforeに当たる。
  • psc_base ≜ ([E^sc] ∪ [F^sc]; hb?); scb; ([E^sc] ∪ hb?; [F^sc])
  • psc_F ≜ [F^sc]; (hb ∪ hb; eco; hb); [F^sc]。C++20の[atomics.order]/4.4に当たる([atomics.order]/4.2・4.3は、psc_baseのうちフェンスが関わる部分におおむね対応する)。

論文のpsc_baseでは、ecoの合成(rb; rfなど)はseq_cstアクセスどうしを直接は結ばない。C++20の[atomics.order]/4.1は、coherence-ordered-before(= eco)で結ばれたseq_cst操作どうしに順序を課す。この差がLWG3941の原因である(第5章)。論文のRemark 4は、[E^sc]; (sb ∪ eco); [E^sc]の非巡回性を要求すると、x86の標準マッピングが不健全になることを、SB+rfisで示している。

RC11の一貫性条件(論文§3、Definition 1)

条件 式
COHERENCE hb; eco? が非反射的
ATOMICITY rmw ∩ (rb; mo) = ∅
SC psc = psc_base ∪ psc_F が非巡回的
NO-THIN-AIR sb ∪ rf が非巡回的

論文は、RC11からx86-TSO、Power(leading/trailingの両方式)、ARMv7へのコンパイルが正しいことを証明している(Theorem 1–3)。

RC11のうちC++に取り込まれなかったもの

RC11の要素 C++での扱い
NO-THIN-AIR 取り込まれていない。P0668R5は、OOTAは「引き続き無視するが、解決の邪魔はしない」とした。C++14以来の勧告([atomics.order]/8、C++20)のまま
リリースシーケンス RC11のリリースシーケンスは、同じスレッドの後続の書き込みを含む(論文§3.2のrsの定義)。また、先行研究で提案されたリリースシーケンスの定義の強化も取り込んでいる(§3.4)。C++20は逆に、P0982R1で同じスレッドのストアをリリースシーケンスから除いた
consume RC11は扱わない。C++はC++26で事実上撤回した(P3475R2)
sb|≠locへの限定 取り込まれていない(第6章)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment