C++

C++ メモリモデル メモ

More than 3 years have passed since last update.

C++ のメモリモデルについてのメモ。

評価

このメモでは以下の2つを評価と呼ぶ。

  • オブジェクト M に対する読み込み (値の計算)
  • オブジェクト M に対する書き込み (副作用)

規格上はこれら以外の評価もあるが、このメモで扱わない。

happens before

happens before は評価と評価の間に定義される半順序関係。

感覚的に言えば、A happens before B であるとは、評価 B が始まる前に必ず評価 A が完了しているということ。

詳しくは後で。

conflict

オブジェクト M と M に対する評価 A, B が以下の 3 条件を満たすとき、A と B は conflict しているという。

  1. A happens before B でない。
  2. B happens before A でない。
  3. A, B の少なくとも一方が書き込み。

atomic

std::atomic<T> テンプレートによってアトミックに読み込み、書き込みが可能なオブジェクトを作成できる。アトミックなオブジェクトは data race を起こさない。

アトミックオブジェクトに対する読み込み、書き込みには memory_order を指定することができる。

happens before 再び

  • 同じスレッド上で実行される評価の間には、プログラム上で表現されている通りの順序で happens before が入る。
  • アトミックオブジェクト M に対する読み込み R と、M に対する書き込み W が以下の条件を満たすならば、W happens before R である。
    1. R が acquire operation.
    2. W が release operation.
    3. R が読んだ値が W によって書かれた値である。

(3番目の条件はもっと緩和できる。W から始まる release sequence のどれかの値なら OK)

// TODO: release sequence

data race

オブジェクト M と M に対する評価 A, B が以下の 2 条件を満たすとき、プログラムに data race があるという。

  1. M がアトミックでない。
  2. A と B が conflict している。

プログラムに data race があるとき、その挙動は undefined behavior である。

modification order

アトミックはオブジェクトは modification order という全順序を持っている。

アトミックオブジェクト M に対する全ての書き込みの集合を S とすると、M の modification order < は S の上の全順序。

アトミックオブジェクト M に対する読み込みと書き込みは、この modification order と矛盾しないように制約される。具体的には以下の 4 つの制約が入る。(制約に含まれる読み込みや書き込みは全て M に対するものとする。)

  1. (write-write coherence) A, B を書き込みとする。A happens before B ならば A < B である。
  2. (read-read coherence) A, B を読み込みとし、X を書き込みとする。A happens before B かつ A が X の値を読んだとすると、B は X の値か「X < Y であるような 書き込み Y」の値を読む。
  3. (read-write coherence) A を読み込み、B を書き込みとする。A は「X < B であるような書き込み X」の値を読む。
  4. (write-read coherence) A を書き込み、B を読み込みとする。A happens before B であるとき、B は A の値を読むか「A < X であるような書き込み X」の値を読む。

要するに、アトミックオブジェクトに対する書き込みは reorder してはいけない。(reorder したことが外部から観測可能であってはいけない)

visible side effect

  1. アトミックオブジェクト M に対する読み込み R が読む値は、次の条件を満たすある書き込み W が書いた値である。
    1. M に対する書き込みである。
    2. R happens before W でない。
  2. アトミックでないオブジェクト M に対する読み込み R は、以下の2条件を満たす M に対する書き込み W によって書かれた値を読む。(W は一意に決まる)
    1. W happens before R
    2. W happens before X かつ X happens before R であるような M への書き込み X が存在しない。

アトミックでないオブジェクトを読み込んだときに、値の候補が複数ある(「一つ前」の書き込みが複数ある)ような場合は、必ず undefined behavior になる。つまり、値の候補を書き込んだ 2 つの書き込み A, B の間に happens before 関係が存在しないということなので、A と B は conflict している。よって data race が存在する。