分散プロトコルは単体テストできない。単体テストは1台のマシン上で1つのプロセスを決まった順序で実行する。分散プロトコルは5台のマシン上で10個のプロセスを、制御できない順序で実行する。この2つの現実の間に、バグが潜んでいる。

モデル検証はその隔たりを埋める。プロトコルが到達しうるあらゆる状態のあらゆる組み合わせを網羅的に探索する。2つのレプリカが不一致になる経路、リーダー選出がデッドロックに陥る経路、split-brainが発生する経路があれば、モデル検証器は必ず発見する。しかも最初のRPC handlerを書く前に。

なぜ分散バグは従来のテストを生き延びるのか

問題は状態爆発である。3つのノードがメッセージを交換するだけで、実行経路は数十億通りに及ぶ。手書きの結合テストはそのうち十数通りしかカバーしない。通常は正常系と、いくつかの明らかな故障モードだけだ。ノードAがprepare送信とackの間にクラッシュするというバグをCIで再現できるだろうか。

形式的検証は学術的な演習のように聞こえるが、モデル検証は異なる。プロトコルが常に正しいことを証明するのではない。仕様記述言語でプロトコルを記述し、関心事項を性質として定義し、ツールに状態空間をある境界まで網羅的に探索させる。違反が見つかれば、最小のトレースが返される。バグ再現のための手順書が step-by-step で手に入る。ヘイゼンバグもない。「私のマシンでは動く」もない。

これに最も実用的なツールは、Leslie Lamport が開発した TLA+ である。見た目が数学的なのは、それが数学だからだ。しかしその数学は思ったより単純で、見返りは、本番環境で深夜2時に表面化するはずだったバグを発見することだ。

モデル検証が実際に行うこと

モデル検証器は3つの入力を受け取る。システムの記述、環境の記述、そして保たれたい性質である。システム記述はプロトコル論理を捉える。環境記述は制御できないすべてを捉える。ネットワーク遅延、メッセージ損失、ノードクラッシュ、時刻ずれである。性質は通常、不変条件（「コミット済みログが上書きされることはない」）や活性条件（「すべてのリクエストは最終的に応答を受け取る」）である。

検証器は到達可能なすべての状態と、状態間の有効な遷移を生成する。有限状態空間については網羅的に、無限については限界付き探索で行う。不変条件が違反されれば、最短の失敗経路を報告して停止する。

これは魔法ではなく力任せである。モデル検証器は意図を理解しない。ただすべてを試す。それがまさに重要な点である。結合テストは人間の仮定に偏っている。モデル検証器は仮定を持たない。

TLA+ での単純な合意プロトコルの記述

最小限の例を見てみよう。リーダーが値を提案し、アクセプタのクォーラムが受け入れることで値が選ばれる、単一裁決の合意プロトコルである。これは Paxos や Raft、その他あらゆる合意アルゴリズムの核心的な考え方である。

システムの TLA+ 仕様は以下の通り：

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

この仕様は次のように述べている。初期状態では何も選ばれていない。propose アクションは chosen を単一の値に設定できるが、それはまだ何も選ばれていない場合に限られる。ChosenUniqueness 不変条件は、選ばれる値は常に高々1つであることを規定する。

TLA+ のモデル検証器 TLC は、ChosenUniqueness を違反する実行トレースが存在しないことを検証する。2つのリーダーが既存の値を確認せずに同時に提案できるバグを導入すれば、TLC は数ミリ秒で反例を発見する。

厄介な要素の追加：クラッシュとメッセージ損失

上記の仕様はきれいすぎる。実際の分散システムはきれいではない。メッセージは消失する。ノードは再起動する。ネットワーク分割がノード群を相互に隔離する。これらの故障をモデル化して初めて、モデルは実用的になる。

メッセージ損失の可能性を含むメッセージ通信をモデル化した、より現実的な断片を以下に示す：

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop は重要な追加である。アクセプタ状態を変更せずにメッセージ損失をモデル化する。TLC は、あらゆるメッセージが配送される、消失する、あるいは無期限に遅延されるトレースを探索する。リーダーのクラッシュと復旧を追加しても状態空間は膨張するが、TLC は依然として体系的に探索する。

これは私が TLA+ を始めたときに躓いた部分だ。当時はプロトコル論理のみをモデル化したかった。しかしバグは論理の中にはなかった。論理と、私が考慮していなかった故障モードとの相互作用の中にあった。両方をモデル化しなければならない。

トレードオフ：状態空間爆発と抽象化

モデル検証にコストはかかる。状態数はプロセス数とメッセージペイロードのサイズに対して指数的に増大する。5つの値と3つのアクセプタを持つ仕様は数百万の状態を生成するかもしれない。4つ目のアクセプタを追加すれば数十億に達する。ラップトップで実行すると、完了する前にメモリを使い果たす。

解決策は抽象化である。実際の64バイト値をモデル化するのではなく、2つの値 V1 と V2 をモデル化する。2つの値でプロトコルが正しく動作すれば、特定の値は関係ない。1万エントリのログもモデル化しない。深さ2のログをモデル化する。深さ2で安全性が保たれれば、ほぼ常に任意の深さでも保たれる。これを small-model checking と呼び、分野の標準的な手法である。

重要なスキルは、どの詳細が重要でどの詳細が重要でないかを見極めることである。メッセージ内容は安全性のためには通常重要でない。メッセージ順序はほぼ常に重要である。ノード識別子は重要でないかもしれないが、各役割のノード数は重要である。

状態空間がそれでも大きすぎる場合、他の選択肢もある。対称性低減を用いて同一ノードを互換可能として扱うこともできる。探索の深さを制限することもできる。あるいは Apalache のような記号的モデル検証器に切り替え、SMT ソルバーを用いてすべてを列挙せずに状態について推論することもできる。

仕様から実装へ：両者の同期を保つ

検証済みの仕様も、実装がそれから逸脱すれば価値がない。仕様は設計図である。コードは建物である。両者の間に自動的な橋渡しはなく、その隙間にバグが潜り込む。

実用的なアプローチは、TLA+ 仕様を偶然にも実行可能な設計文書として扱うことである。プルリクエスト時にコードと併せてレビューする。実装がエッジケースを処理する場合、仕様もそれを処理しているか自問する。本番でバグを発見したら、仕様がそれを捉えられたか確認する。捉えられなかったら、仕様を更新する。

中には、TLC が生成する反例からテストケースを生成するチームもある。2つのレプリカが分岐する様子を示す TLC のトレースが、結合テストのシナリオになる。これは手作業だが、形式的モデルをテストスイートと接続する。

Sentry では、このアプローチを用いて分散レート制限プロトコルを検証した。仕様は、復旧中のノードが特定の分割シナリオで飢餓状態に陥る可能性があるという活性問題を捉えた。我々の結合テストは常に分割をきれいに修復していたため、それを引き起こしたことはなかった。モデル検証器はきれいさを気にしない。厄介なケースを試し、バグを発見し、非常に混乱しうるインシデントを防いでくれた。

始め方：最初のモデル検証

試してみたいのなら、TLA+ Toolbox から始めよう。仕様の記述と検証のための無料IDEである。付属の Paxos や Raft の例題に取り組む。上記の合意プロトコルの断片より複雑だが、実際のプロトコルがどうモデル化されるかを示している。

最初の仕様には、自分のシステムから小さなものを選ぶ。リーダー選出プロトコル、分散キャッシュ無効化スキーム、2相コミットの変種など。保たれていると信じる不変条件を書き出し、TLC に自分が正しいかどうか教えてもらう。答えはたいてい「否」であり、最初の1時間以内に教えてくれる。

モデル検証はあらゆるバグを見つけるわけではない。性能には役立たない。シリアライズの誤りも捉えられない。実装が仕様と一致するかも検証できない。モデル検証が行うのは、結合テストが見逃す深層のプロトコルバグを設計時に発見することであり、その修正コストはゼロである。

これこそが分散システムにおける最も安価なバグ修正である。より良いデバッガでも、より多くの監視でもない。コードが存在する前にバグを捉えることだ。