形式手法とモデル検査（TLA+）による設計検証

なぜテストでは並行バグを捕まえきれないのか

並行・分散アルゴリズムのバグの多くは、特定のインターリーブ——複数プロセスの命令がどの順で絡み合うか——でしか発火しません。テストはこの順序の空間のごく一部しか踏めないため、「100万回走らせて落ちなかった」は「バグがない」を意味しません。落ちなかったのは、致命的な順序をたまたま引かなかっただけかもしれない。ダイクストラの言う「テストは欠陥の存在を示せても不在は示せない」が、並行性では特に容赦なく効きます。

形式手法（formal methods） はこの問題に正面から答えます。実装ではなく 設計（仕様） を数学的な対象として書き下し、その上で成り立つべき性質を 証明 あるいは 網羅的探索 で確かめる。中でも モデル検査（model checking） は、システムが取りうる状態を機械的に全て列挙し、悪い状態へ到達しないかを総当たりで調べます。本記事では、安全性と活性という二つの性質、状態空間探索の原理、TLA+/PlusCal による仕様記述、そして最大の壁である状態爆発と抽象化を、原理から解きほぐします。決定論的シミュレーション（/devops/deterministic-simulation-testing/）が実装の実行を再現可能にするのに対し、モデル検査は設計の全実行を尽くす——層が違います。

安全性と活性：二種類の性質

検証したい性質は、突き詰めると二つに分類されます。この区別は理解の土台なので先に押さえます。

決定的なのは反例の形です。安全性違反は有限の実行で目撃できます——不変条件が破れた瞬間のステップを示せば証拠になる。一方 活性違反は「永遠に達成されない」 という主張なので、有限の前置きの後に「望む状態を含まない無限ループ」が存在することを示す必要があります。モデル検査器が安全性の反例として「初期状態からダメな状態までの最短経路」を、活性の反例として「ループへ落ち込む実行」を返すのは、この性質の差から来ます。

モデル検査の原理：状態空間の網羅探索

モデル検査の発想は驚くほど直接的です。システムを 状態遷移系 とみなす。すなわち、(1) 初期状態の集合、(2) ある状態から次の状態への遷移関係、で定義する。すると到達可能な状態は、初期状態から遷移を繰り返して届く全ての状態の集合——有向グラフのノードです。検査器はこのグラフを 幅優先探索（BFS）などで全ノード展開 し、各ノードで不変条件を評価する。どこかで偽になれば、初期状態からそのノードへの経路がそのまま反例になります。

状態空間 = (初期状態, 遷移関係) から到達可能な全状態のグラフ

   [初期] → [s1] → [s3] → ... 
      │       │
      ▼       ▼
    [s2] → [s4] → [BAD] ← ここで不変条件が偽
                    ↑
   反例 = [初期]→[s2]→[s4]→[BAD] の最短経路を提示

ここで効くのが 状態のハッシュによる重複排除 です。並行プログラムは同じ状態へ別経路から何度も到達するため、訪問済み状態をハッシュ集合で覚えておき、再訪を枝刈りする。これにより探索は有限グラフ上の到達可能性問題に帰着し、全インターリーブを尽くしても各状態は一度だけ調べれば済む。テストが順序空間をランダムに点でつつくのに対し、モデル検査は到達可能な状態を一つ残らず覆う——これが「網羅的」の意味です。

活性の検査はもう一段重い。望む状態へ永遠に到達しない実行を探すには、状態空間の中の 強連結成分（到達後に抜け出せないループ） を解析し、その中に「公平性のもとでも望む状態を含まないサイクル」がないかを調べます。だから活性検証では後述の 公平性仮定 の指定が要となります。

TLA+とPlusCal：仕様をどう書くか

TLA+ はレスリー・ランポートが設計した仕様記述言語で、状態を 変数の値の組 として、振る舞いを 次状態関係（next-state relation） として表します。核は「状態」と「アクション」です。アクションは現在の変数（例 x）と次の状態の変数（プライム付き、例 x'）を関係づける論理式で書きます。たとえば「カウンタを1増やす」は x' = x + 1 のように、代入ではなく「現在と次状態が満たすべき等式」 として表現するのが特徴です。

仕様全体は概ね Init /\ [][Next]_vars という形になります。Init は初期状態の条件、Next は次状態関係（複数アクションの論理和）、[][Next]_vars は「全てのステップが Next に従うか変数が不変（スタッタリング）」を意味します。検証したい性質は別途、不変条件 Inv や時相式として与えます。

\* 相互排他の骨子（イメージ）
VARIABLES pc      \* 各プロセスの制御位置
Init == pc = [p \in Procs |-> "idle"]

Enter(p) == /\ pc[p] = "trying"
            /\ \A q \in Procs : q # p => pc[q] # "crit"  \* 誰もcritにいない
            /\ pc' = [pc EXCEPT ![p] = "crit"]

Next == \E p \in Procs : Enter(p) \/ ...

\* 安全性：同時に2つがcritに入らない
MutualExclusion ==
  \A p, q \in Procs : (p # q) => ~(pc[p] = "crit" /\ pc[q] = "crit")

これを直接書くのは慣れが要るため、PlusCal という擬似コード風の上位言語が用意されています。while や if、ラベル付きの逐次処理を手続き的に書け、それが TLA+ へ機械翻訳されます。ラベルの位置がアトミック性の境界 を定めるのが肝で、ラベルとラベルの間は1ステップ（不可分）として扱われ、ラベル境界で他プロセスのインターリーブが入りうる。つまりラベルの粒度が、検査する並行性の細かさを直接決めます。

実際の検査は TLC モデル検査器が担います。TLC は無限の値域を扱えないため、Procs の要素数やカウンタの上限といった パラメータを有限のモデルへ具体化（model） したうえで状態空間を展開します。だから「3プロセス・カウンタは0..4」のような 小さな有限モデル で検証するのが基本作法になります。

活性と公平性：進行をどう保証するか

活性（最終的進行）を検証するには、落とし穴があります。何も制約しなければ、検査器は「あるプロセスが永遠に選ばれず、何もしないまま時間が過ぎる」実行を合法とみなし、ほぼ全ての活性性質が偽になってしまう。現実には「実行可能な処理はいつか実行される」はずなので、これを 公平性仮定（fairness） として明示します。

• 弱い公平性（weak fairness）: あるアクションが 継続的に 実行可能なら、いつか実行される。一時的に無効化されない限り放置されない、という保証。
• 強い公平性（strong fairness）: あるアクションが 繰り返し 実行可能になるなら（途中で無効化されても再び有効になり続けるなら）、いつか実行される。より強い保証。

公平性は「スケジューラがどのプロセスもいつかは進める」という前提のモデル化であり、これを置いて初めて「要求はいつか応答される」式の活性が証明可能になります。逆に言えば、活性は環境（スケジューラ）への仮定とセットでしか主張できない。これは FLP不可能性（/devops/flp-impossibility/）が示した「非同期かつ仮定なしでは合意の終了を保証できない」という事実と地続きで、形式仕様では公平性をどこまで仮定するかが活性主張の射程を決めます。

状態爆発と抽象化：最大の壁

モデル検査の理論上の万能性を現実で縛るのが 状態爆発（state explosion） です。到達可能状態の数は、変数の値域とプロセス数に対して 指数的 に増えます。プロセスがN個、各プロセスの局所状態がk通りなら、組み合わせだけで k^N のオーダー。共有変数やメッセージキューが加わればさらに膨らみ、メモリと時間がたちまち尽きます。網羅探索の代償がここに集中します。

これに対する武器が 抽象化と簡約 です。状態空間を「検証したい性質を保ったまま」小さくする技法群です。

肝は 「性質を保つ縮約」 であることです。抽象化が雑だと、抽象モデルでは安全でも実モデルでは危険、という偽の安心（不健全な抽象化）を生む。逆に詳細を残しすぎれば状態爆発に戻る。この匙加減——何を捨て何を残すか——がモデル検査の腕の見せ所であり、コンセンサス系のアルゴリズム（/devops/consensus-family-tree/）や整合性モデル（/devops/consistency-models/）のような複雑な対象では、適切な抽象なしには現実的時間で回りません。

まとめ

• モデル検査は、システムを状態遷移系とみなして 全到達可能状態を網羅探索 し、安全性（不変条件）と活性（最終的進行）を総当たりで判定する。違反時は反例の実行列を返すため、テストでは踏めない並行バグを設計段階で確定的に暴ける。
• 性質は二分される。安全性は有限実行で違反を目撃でき、不変条件で表す。活性は無限実行に対する主張で、時相論理と公平性仮定（弱い／強い）を伴って初めて主張できる。
• TLA+ は状態を変数の値、振る舞いを プライム変数による次状態関係 で書く時相論理。PlusCal は擬似コード風の上位言語で、ラベルがアトミック境界 を定める。検査は TLC が 有限モデルへの具体化 のうえで状態空間を展開して行う。
• 最大の壁は 状態爆発——状態数はプロセス数に指数的に増える。有界化・対称性簡約・抽象化・部分順序簡約 で、検証したい性質を保ったままモデルを縮約するのが要諦。
• 実務の定石は 小スコープ仮説 に乗ること。3〜5プロセス程度の小モデルで安全性をまず網羅的に確かめ、活性は公平性を慎重に与えて補完する。設計の致命的欠陥は、たいてい小さなモデルで最短反例として落ちてくる。