C++ のメモリモデルについてのメモ。
評価
このメモでは以下の２つを評価と呼ぶ。
- オブジェクト M に対する読み込み (値の計算)
- オブジェクト M に対する書き込み (副作用)
規格上はこれら以外の評価もあるが、このメモで扱わない。
happens before
happens before は評価と評価の間に定義される半順序関係。
感覚的に言えば、A happens before B であるとは、評価 B が始まる前に必ず評価 A が完了しているということ。
詳しくは後で。
conflict
オブジェクト M と M に対する評価 A, B が以下の 3 条件を満たすとき、A と B は conflict しているという。
- A happens before B でない。
- B happens before A でない。
- A, B の少なくとも一方が書き込み。
atomic
std::atomic<T> テンプレートによってアトミックに読み込み、書き込みが可能なオブジェクトを作成できる。アトミックなオブジェクトは data race を起こさない。
アトミックオブジェクトに対する読み込み、書き込みには memory_order を指定することができる。
happens before 再び
- 同じスレッド上で実行される評価の間には、プログラム上で表現されている通りの順序で happens before が入る。
- アトミックオブジェクト M に対する読み込み R と、M に対する書き込み W が以下の条件を満たすならば、W happens before R である。
- R が acquire operation.
- W が release operation.
- R が読んだ値が W によって書かれた値である。
(3番目の条件はもっと緩和できる。W から始まる release sequence のどれかの値なら OK）
// TODO: release sequence
data race
オブジェクト M と M に対する評価 A, B が以下の 2 条件を満たすとき、プログラムに data race があるという。
- M がアトミックでない。
- A と B が conflict している。
プログラムに data race があるとき、その挙動は undefined behavior である。
modification order
アトミックはオブジェクトは modification order という全順序を持っている。
アトミックオブジェクト M に対する全ての書き込みの集合を S とすると、M の modification order < は S の上の全順序。
アトミックオブジェクト M に対する読み込みと書き込みは、この modification order と矛盾しないように制約される。具体的には以下の 4 つの制約が入る。(制約に含まれる読み込みや書き込みは全て M に対するものとする。)
-
(write-write coherence) A, B を書き込みとする。A happens before B ならば A
<B である。 -
(read-read coherence) A, B を読み込みとし、X を書き込みとする。A happens before B かつ A が X の値を読んだとすると、B は X の値か「X
<Y であるような 書き込み Y」の値を読む。 -
(read-write coherence) A を読み込み、B を書き込みとする。A は「X
<B であるような書き込み X」の値を読む。 -
(write-read coherence) A を書き込み、B を読み込みとする。A happens before B であるとき、B は A の値を読むか「A
<X であるような書き込み X」の値を読む。
要するに、アトミックオブジェクトに対する書き込みは reorder してはいけない。（reorder したことが外部から観測可能であってはいけない）
visible side effect
- アトミックオブジェクト M に対する読み込み R が読む値は、次の条件を満たすある書き込み W が書いた値である。
- M に対する書き込みである。
- R happens before W でない。
- アトミックでないオブジェクト M に対する読み込み R は、以下の2条件を満たす M に対する書き込み W によって書かれた値を読む。(W は一意に決まる)
- W happens before R
- W happens before X かつ X happens before R であるような M への書き込み X が存在しない。
アトミックでないオブジェクトを読み込んだときに、値の候補が複数ある（「一つ前」の書き込みが複数ある）ような場合は、必ず undefined behavior になる。つまり、値の候補を書き込んだ 2 つの書き込み A, B の間に happens before 関係が存在しないということなので、A と B は conflict している。よって data race が存在する。