並行性のテスト（決定性再生とモデル検査）

なぜ並行バグはテストで捕まらないのか

逐次プログラムの実行は入力で一意に決まるので、同じ入力なら同じ結果が出ます。ところが複数スレッドが共有状態を触ると、結果は**スレッドのインターリーブ（命令の交差順序）**にも依存します。どの順でスケジューラがスレッドを走らせるかはOSやCPUの都合で毎回変わり、しかもメモリモデルとhappens-beforeが許す範囲で命令の並び替えまで起こります。

ここに2つの困難が生じます。第一に再現性の欠如。バグを踏むのは特定のインターリーブだけで、テストを再実行しても同じ順序にならず再現できない（ハイゼンバグ）。第二に網羅の困難。n個の処理を持つ2スレッドのインターリーブ数は組み合わせ的に増え、3スレッド以上では天文学的になります。普通のテストは多数あるインターリーブのうち1本を運任せで踏むだけなので、残りの危険な順序は素通りします。

スレッドA: a1 a2          可能なインターリーブの一部:
スレッドB: b1 b2          a1 a2 b1 b2 / a1 b1 a2 b2 / a1 b1 b2 a2 ...
                          → 2スレッドでも C(4,2)=6 通り。普通のテストは1本だけ実行

対策は「スケジューリングを偶然に任せず、制御下に置く」ことに尽きます。具体策が決定性再生・網羅的探索・モデル検査の三本柱です。

決定性再生（deterministic replay）

決定性再生は、ある実行で起きた非決定の源を記録しておき、後でそれを固定して同じ実行を再現する技法です。再現できれば、デバッガを当てて何度でも同じ失敗を観察できます。鍵は「何が非決定を生むか」を漏れなく捕まえることです。

実装方式は大別して2つ。順序ベースは共有メモリアクセスやロック獲得の順序を論理時刻で記録し、再生時にその順序を再現します（命令レベルまで追うと重いので、同期点だけを追うことが多い）。入力ベースはシステムコールや乱数・タイマなど外界とのやり取りだけ記録し、内部計算は決定的とみなして再実行します。後者は記録が軽い一方、データ競合のある実行は内部が非決定なので忠実に再生できないことがあります。

決定性再生はプロパティベーステストが乱数シードで反例を再現するのと同じ思想で、非決定をシードのように記録・固定するものだと捉えると見通しが良くなります。

インターリーブの網羅的探索（systematic testing）

再生がバグの再現なら、網羅的探索（systematic concurrency testing）はバグをまだ起こしていない順序を能動的に試す手法です。スケジューラ自体をツールが乗っ取り、スレッド切替の地点（同期操作や共有アクセス）でどのスレッドを次に走らせるかを選び、可能な選択を系統的に列挙します。CHESS（Microsoft）が代表で、Rust の Loom や Java の JPF（Java PathFinder）も同じ発想です。これは単一実行を観測して競合を報告するだけの動的レース検出器（Go の -race など、後述）とは別物で、こちらは複数のスケジュールそのものを能動的に切り替える点が異なります。

素朴に全インターリーブを試すと状態爆発で破綻するため、3つの実用的な枝刈りが効きます。

• 部分順序簡約（partial-order reduction, POR）: 独立な操作（互いに別のメモリを触り順序が結果に影響しない操作）の入れ替えは同じ最終状態に至るため、代表1本だけ調べて残りを省く。可換な遷移を畳み込むのが核心。
• コンテキストスイッチ境界（bounded preemption）: 大半の並行バグは少数（経験的に2回程度）の割り込み的切替で再現できる、という観察に基づき、強制的な横取り（preemption）回数に上限を設けて探索空間を劇的に絞る。バグを取りこぼす可能性と引き換えに現実的なコストに収める。
• 公平性スケジューリング: 活性（後述）を調べるとき、特定スレッドを永遠に飢えさせる非現実的な順序を除外する。

モデル検査と TLA+

決定性再生も網羅探索も「動くコード」が前提です。しかし並行性モデルの設計段階、つまりプロトコルやアルゴリズムの正しさは、コードを書く前に検証したい。そこで使うのがモデル検査で、TLA+ はその代表です。

TLA+ ではシステムを状態と遷移の集合として宣言的に書きます。状態は変数の値の組、遷移は「現在の値（無印）と次の値（プライム付き）の関係」を述べる述語です。検証したい性質は主に2種類で、これらは並行設計の正しさの両輪です。

モデル検査器（TLC）は初期状態から到達可能な全状態を幅優先で展開し、各状態で不変条件（安全性）が破れないかを総当たりで確認します。違反が見つかると、初期状態から違反状態までの反例トレースを返します。これがモデル検査の最大の価値で、「ここでAがロックを取り、Bが割り込み、Aが古い値を見る」という具体的な失敗の筋道を、人手のデバッグなしに突きつけてくれます。活性は無限実行に関する性質なので、状態遷移グラフ上のサイクル探索（公平性仮定のもとで望ましい状態に到達できないループの検出）で確かめます。

TLC の探索（概念）:
  frontier = {初期状態}
  while frontier:
      s = frontier から取り出す
      assert Invariant(s)            # 安全性: 破れたら反例トレースを出力
      for s' in 次状態(s):
          if s' が未訪問: frontier に追加
  # 全到達状態を訪問し終えれば安全性は証明済み

まとめ

並行バグの厄介さは、結果がスレッドのインターリーブという実行ごとに変わる非決定に依存する点にあり、普通のテストは多数の順序のうち1本を運任せで踏むだけです。決定性再生は非決定の源（切替・競合アクセス・外部入力）を記録して固定し、同じ失敗を再現可能にします。網羅的探索はスケジューラを乗っ取って危険なインターリーブを能動的に列挙し、部分順序簡約と切替回数の境界化で状態爆発を抑えます。**モデル検査（TLA+）**は設計を状態遷移系として全状態を探索し、安全性と活性を反例トレースつきで検証して、コードのテストでは届かない上流の欠陥を捉えます。これらはデッドロックの検出・回避のような個別対策の土台となる、並行性を「偶然ではなく原理で」確かめるための道具立てです。