線形化可能性検査とJepsenによる整合性検証

なぜ「検証」が必要なのか

分散データベースやキューが「線形化可能（linearizable）」「直列化可能」とうたっていても、それは 設計上の主張 にすぎません。実装にはバグがあり、ネットワーク分断やリーダー交代という稀な条件下でだけ崩れる保証も多い。整合性モデルが定めるのは「許される履歴の集合」という正しさの基準であって、実装がその基準を守っている保証は別途与えなければなりません。

線形化可能性検査（linearizability checking） は、システムを実際に走らせて得た 操作履歴（history） が、その整合性モデルに照らして妥当かを機械的に判定する手法です。Jepsen はこれに 障害注入 を組み合わせ、稀な条件をわざと作り出して反証を狙うフレームワークです。要点は、保証を 証明 するのではなく、違反を 発見 することにあります。1つでも違反履歴が見つかれば、その主張は反証されます。

線形化可能性検査の定義

履歴は操作ごとに2つのイベントを持ちます。呼び出し（invocation） と 応答（completion） です。各操作はクライアントが呼んでから応答を受け取るまでの 時間区間 を占めます。線形化可能であるとは、各操作にその区間内の ある瞬間（linearization point） を割り当てて全操作を1つの全順序に並べ、その順序が逐次仕様（sequential specification）を満たすことです。

ここで重要な制約が2つあります。第一に、線形化点は必ず 呼び出しと応答の間 になければならない。第二に、ある操作が応答を返したあとに 開始 した操作は、必ずその後ろに並ぶ（実時間順の尊重）。一方、区間が重なる並行操作は、仕様を満たす限りどの順に並べてもよい。

# 時間区間の重なりと並べ替えの自由度
クライアントA: |--- write(x=1) ---|
クライアントB:        |--- read(x) -> 0 ---|
# A と B は区間が重なる。Bの線形化点を Aより前に置けば read->0 は合法。
# だが Aが応答を返したあとに Bが開始していたなら、read->0 は違反。

検査器の仕事は、こうした線形化点の割り当てが 1つでも存在するか を探すことです。存在すれば線形化可能、どう並べても仕様違反になるなら反例として報告します。

Knossos：履歴全体を探索する

Jepsen 初期の検査器 Knossos は、レジスタやキューのような単純なオブジェクトに対し、可能な線形化順序を 全探索 します。中核は Wing と Gong の古典アルゴリズムで、履歴を左から走査しながら「次にどの未完了操作を線形化するか」を試し、逐次仕様で状態遷移をシミュレートして矛盾が出たらバックトラックします。

問題は計算量です。任意のオブジェクトに対する線形化可能性判定は 一般に NP 困難 であることが知られています。並行操作が n 個重なると線形化順序の候補が階乗的に増えるため、Knossos は 並行度が高い長い履歴で爆発 します。実装は到達済み状態のメモ化や対称性の刈り込みで緩和しますが、根本的な指数性は消えません。

Elle：依存グラフで循環を探す

この限界を超えるため Jepsen 作者の Kyle Kingsbury が作ったのが Elle です。発想を反転させ、全順序を 探索 する代わりに、読んだ値から 版（version）の間の依存関係 を復元し、そのグラフに 循環があるか を調べます。循環は「ある全順序が存在しない」ことの証拠であり、循環がなければトポロジカルソートで妥当な順序が構成できます。

Elle は読み取りが返した値を手がかりに、主に3種類の依存辺を引きます。ww（書き込み→書き込み）：ある版が別の版を上書きした順。wr（書き込み→読み取り）：ある読み取りがどの書き込みの値を読んだか。rw（読み取り→書き込み）：ある読み取りが見た版が、後続の書き込みより前にあったという反依存。これらの辺と実時間順の辺を合わせたグラフに循環があれば、整合性違反です。

Elle の決定的な利点は2つです。第一に、グラフの循環という形で 違反の説明 を返すため、開発者がバグを再現・修正できます。第二に、版の追跡により線形化可能性だけでなく Read Committed・Snapshot Isolation・Serializable といったトランザクション分離レベルの違反まで判定できます。並行度が高い長い履歴でも実用的に走るため、現在の Jepsen テストの標準的な検査器になっています。

Jepsen：障害を注入して反証する

検査器に良質な履歴を食わせるのが Jepsen 本体の役割です。構成は3層に分かれます。

• ジェネレータ（generator）：ランダムだが再現可能な操作列（read/write/cas など）を生成し、複数クライアントから並行に発行する。乱数シードを固定すれば同じテストを再現できる。
• ネメシス（nemesis）：テスト中に 障害を注入 するコンポーネント。ネットワーク分断（iptables でパケット遮断）、クロックずれ、プロセス停止（kill -STOP/-CONT）、リーダーの強制交代、メンバーシップ変更などを、操作と並行してスケジュールする。
• チェッカ（checker）：記録した完全な操作履歴を Elle や Knossos に渡し、線形化可能性・分離レベル違反を判定する。

なぜ障害注入が要かというと、線形化可能性が崩れるのは 平常時ではなく異常時 だからです。分断中に少数派のリーダーが古い値を返す、リーダー交代の隙間にコミット済みの書き込みが失われる、といったバグは、分断やプロセス停止を起こさなければ表に出ません。ネメシスは リーダー選出とスプリットブレインで問題になる「2人のリーダー」状態などを意図的に再現し、それでも履歴が線形化可能なままかを問います。

何が検出でき、何ができないか

この手法が見つけるのは 実在する反例 です。検出された違反は本物で、偽陽性は原理的に起きにくい（履歴が仕様を満たす順序を持たないことは確定的に示せる）。代表的に暴かれてきたのは、stale read（古い値の読み出し）、lost update（更新の消失）、split-brain による二重書き込み、リーダー交代時のコミット済みデータ喪失などです。

一方で 限界 は明確です。テストはあくまでサンプリングであり、注入しなかった障害パターンや、生成しなかった操作列で起きるバグは見つかりません。違反が 見つからないこと は正しさの証明にはならず、「今回のテストでは反証できなかった」以上を意味しません。だから カオスエンジニアリングと同じく、Jepsen は 継続的に・多様な条件で 回し続けてこそ価値が出ます。実時間順を判定の根拠にする以上、クライアント側の時計精度や記録の粒度も結果に影響します（論理クロックが因果の追跡に使われるのと対照的に、ここでは外部観測者の実時間が基準になります）。

まとめ

• 線形化可能性検査は、各操作に区間内の線形化点を割り当て、得られる全順序が逐次仕様を満たすかを判定する問題。古い値を返した瞬間に違反になる。
• Knossos は線形化順序を全探索する。判定は一般に NP 困難で、高並行・長尺の履歴では計算量が爆発する。
• Elle は読んだ値から版の依存グラフを作り循環を探す。実用的にスケールし、違反の説明と分離レベル判定まで提供する。
• Jepsen はジェネレータ・ネメシス・チェッカで、障害を注入しながら履歴を記録・検査する。保証を証明するのではなく実装を 反証 する枠組み。
• 見つかった違反は本物だが、見つからないことは正しさの証明ではない。多様な条件で回し続けることが前提。