# Lineage-driven Fault Injection > [!abstract] 概要 > 障害は常に起こりうる選択肢であり、大規模データ管理システムでは事実上確実に起こる。耐障害プロトコルとコンポーネントは実装もデバッグも難しいことで知られる。さらに悪いことに、既存の耐障害機構を選び、複雑なシステムに正しく統合することは依然として職人芸であり、プログラマを支援する道具はほとんどない。我々は、耐障害なデータ管理システムのバグを発見する新しい手法、系譜駆動障害注入(lineage-driven fault injection)を提案する。系譜駆動の障害注入器は、正しいシステムの結果から後ろ向きに推論し、実行中の障害がその結果を妨げえたかどうかを判定する。我々は、データベース研究のデータ系譜の技法と最先端の充足可能性判定を新しく組み合わせた系譜駆動障害注入の試作 MOLLY を示す。特定の構成に耐障害性のバグが存在するなら、MOLLY はそれを素早く見つけ、多くの場合ランダム障害注入より桁違いに少ない実行回数で済む。存在しなければ、MOLLY はその構成に対してコードにバグがないことを証明する。 ## 論文情報 - 題名: Lineage-driven Fault Injection - 著者: Peter Alvaro, Joshua Rosen, Joseph M. Hellerstein([[Peter Alvaro]]、[[Joshua Rosen]]、[[Joseph M. Hellerstein]]。いずれも当時 [[University of California, Berkeley]]) - 会議: SIGMOD'15(2015 年 5 月 31 日〜6 月 4 日、メルボルン) - DOI: 10.1145/2723372.2723711 - 分野: Database Management — Distributed Databases。キーワードは fault-tolerance, verification, provenance ## 概要 耐障害性はシステム全体の性質であり、個々の部品の保証は合成で崩れる。従来の[[障害注入]]は浅いバグには有効だが、複数種の障害の稀な組合せを見つけられず、探索空間の網羅も保証できない。本論文は、成功した実行の系譜(その結果を導いたデータとメッセージの導出関係)を後ろ向きにたどり、結果を偽にしうる障害だけを注入する LDFI を提案し、その試作 MOLLY で 14 の耐障害プロトコルを検証する。 ## 問題設定 - 対象は、ノードのクラッシュ、メッセージ喪失、一時的なネットワーク分断で起こるデータ管理システムの耐障害性バグである。ビザンチン障害とクラッシュ回復は扱わない。 - 上位の要件は、健全性(反例は実在するバグに対応する)と、可能なら完全性(反例が見つからなければ、その入力と実行境界でバグが存在しないと保証する)である。 - 動機の事例は Kafka 0.8 の複製バグである。[[ZooKeeper]] が見せる in-sync-replicas(ISR)リストからレプリカ b・c が分断で外れ、リーダー a が唯一のメンバーとして書込みに応答し、複製せずクラッシュして確認済みの書込みが失われる。ZooKeeper も主従複製もそれぞれ正しく、合成で誤る。Kingsbury が経験と直観で見つけたこの種のバグを汎用ツールで見つけられるかが問いである。 ## 提案手法 - 系譜駆動: 障害のない実行で目的の結果(良い結果)を得る。次に、その結果の系譜を導出グラフ(規則発火ノードと目標ノードの二部グラフ)として取り出し、独立な導出(support)ごとの証明木にする。1 つの証明木は、含まれるメッセージのどれか 1 つの喪失、またはノードのクラッシュで偽にできるため、選言(OR)で書ける。全 support を同時に偽にする条件は、選言の連言、すなわち CNF になる。これを SAT ソルバに渡し、充足解を候補の反例(障害の組合せ)とする。 - 前向き・後ろ向きの交互実行: 候補の障害を入力へ戻して具体実行を行う。結果が生成されなければ真の反例になり、別の導出で生成されれば新しい系譜が得られて繰り返す。候補が尽きたとき、その構成に反例がないと保証する。ソルバと具体評価器の交互実行は、コンコリック実行に似る。 - 障害仕様: Fspec = ⟨EOT, EFF, Crashes⟩ で、EOT は論理時間の上限、EFF はメッセージ喪失が止まる時刻(有限障害の終わり)、Crashes はクラッシュ数の上限である。EFF < EOT として回復の猶予を与える。既定では EFF = 0 から EOT を増やし、次に EFF を増やすスイープで最小のパラメータを探す。 - 同期実行モデル: 配送されたメッセージは決定的な順序で受信されると仮定し、障害だけを体系的に探索する。非同期の全体を模擬する代わりに、実行数を大幅に減らせる。 - 言語と実装: 試作は宣言型言語 Dedalus(Datalog に時間と空間を加えたもの)で書く。Dedalus を clock 関係付きの Datalog¬ に書き換え、メッセージ喪失を clock 関係からの行削除、クラッシュを以降の全行の削除として表す。系譜は Kohler らの来歴付き書換えで規則ごとの firings 関係として記録する。 - 記述例は Figure 2(simple-deliv の Dedalus コード)、Figure 3(信頼できる配送の pre / post 仕様)、Figure 5(ack-deliv)、Figure 6(redun-deliv の系譜)にあり、いずれも本文で代替できるため転載しない。 - 正しさの仕様は組込みメタ結果 pre / post による含意 pre → post で書く。pre が偽なら空虚に正しい実行とみなし、探索から除く。ソルバは Datalog 評価器と SAT ソルバの既製品である。 - 否定を含むゴールの来歴(why-not)は、無視する、代理タプルを使う、静的解析で保守的に過大近似する、の 3 通りを提供する。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig01-molly-architecture.png|500]] *Figure 1: MOLLY の前向き・後ろ向きの交互実行(具体評価器、ハザード解析、SAT ソルバ)。* - 対戦の導入(3 節): プログラマと敵対者の対戦として信頼できるブロードキャストを段階的に改善する。ラウンド 1 の naive 版は support が 1 つで 1 メッセージ喪失に負ける。ラウンド 2 の再送版は時間冗長だが、送信元 A のクラッシュに弱い。ラウンド 3 の全ノード再送版は空間・時間ともに冗長で、敵対者は手を失う。ラウンド 4 の ACK 付き版は、ACK 未着の障害実行で追加の再送が起きるため、系譜が具体実行ごとに変わることを示す。ラウンド 5 の古典的ブロードキャストはフェイルストップ前提の正しさ証明をメッセージ喪失のある環境へ持ち込んだ誤用で、反例が見つかる。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig04-outcome-lineage-counterexamples.png|900]] *Figure 4(4a・4b・4c): 結果の系譜と反例トレース。simple-deliv、retry-deliv、classic-deliv。* ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig07-ack-deliv-lineage.png|500]] *Figure 7: ACK 付き有限再送 ack-deliv の系譜と失敗した障害注入の試行。* ## 新規性 - 障害注入(ランダム・ヒューリスティック探索)に、データ来歴(lineage)で導いた後ろ向き推論と SAT による組合せ探索を持ち込み、注入すべき障害を「結果の導出を偽にしうるもの」に限定する。 - モデル検査が状態空間の大きさに依存するのに対し、LDFI の複雑さは良い結果の系譜の深さに依存する。 - 反例をラムポート図と系譜グラフの可視化として返し、根本原因の推定に使える。健全性と完全性の証明を付録に示す。 - 位置づけ(付録 A の比較表): 障害のテスト、実行可能コード、safety / liveness 違反、バグの説明のうち、バグの説明と liveness 違反を併せ持つ点が特徴である。入力生成と割込み順序のテストは持たず、既存ツールと補完関係にある。 ## 実験設定 - 検証対象は Dedalus で実装した信頼できる配送(simple / retry / redun / classic / ack)、2PC、2PC + CTP、3PC、Paxos、bully リーダー選出、Flux、Kafka の複製サブシステムである。 - 比較対象は Molly 自身に実装したランダム障害注入(SAT と系譜抽出なし。25 回平均)である。 - 不在保証は、バグのない 5 つのプログラムをパラメータスイープで 120 秒動かし、到達した最大の Fspec を報告する。 ## 実験結果 - 2PC のブロッキング、CTP の依然残るブロッキング、3PC のメッセージ喪失下での合意違反(coordinator は abort、残りの agent は commit)を、既知の限界として自動で再現した。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig08-2pc-blocking.png|500]] *Figure 8: 2PC のブロッキング実行(コーディネータ障害で終了性違反)。* ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig09-3pc-conflict.png|500]] *Figure 9: 3PC でメッセージ喪失により agent が食い違う決定をする実行(合意違反)。* - Kafka のバグは Kingsbury の反例と同じ形(分断で b・c が ISR から外れ、a が単独確認応答後にクラッシュ)で再現した。Kafka のモデルは全体で 18 行で、複製ロジックを詳細に(約 12 行)、ZooKeeper とクライアントをスケッチで書いた。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig10-kafka-replication-bug.png|500]] *Figure 10: Kafka の複製バグ(分断で ISR が縮退し、確認済みの書込みが失われる)。* - 効率は、浅いバグではランダム注入と拮抗する一方、深い Kafka のバグでは実行 38 回・3.74 秒に対し、ランダム注入は平均 1183.12 回・133.30 秒で、約 1 桁以上の差がある。3PC も 55 回対 40.60 回で、浅い設定では逆転している。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig12-buggy-programs.png|900]] *Figure 12: バグのあるプログラムで、MOLLY はランダム注入より少ない実行で反例を見つける。* - 不在保証では、redun-deliv が 11 回の実行で 8.07 × 10^18 通りの組合せを、Flux が 187 回で 6.20 × 10^76 通りを網羅した。 ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig13-bugfree-programs.png|500]] *Figure 13: バグのないプログラムの、120 秒スイープで到達した Fspec と網羅した実行数。* ![[wiki/sources/_attachments/2015__SIGMOD__Lineage-driven-Fault-Injection/fig11-search-space-growth.png|500]] *Figure 11: EOT と EFF を増やしたときの具体実行数と可能な障害組合せ数の比較。* ## 考察 - 同期モデルの代償として、非同期に依存するバグは見逃しうる。合意系プロトコルでは、Paxos の合意(agreement)の安全性は検証できても、停止性は保証できない。 - 内部決定性(環境の非決定性を除けば決定的)を仮定するため、anti-entropy や乱択合意のような本質的に非決定的なプロトコルの不在証明には追加研究が要る。 - 入力とトポロジは事前に与える前提で、記号実行や入力生成と組み合わせられる。クラッシュ回復の検証、Java 等の主流言語への適用、系譜を使った耐障害プログラム合成が今後の課題である。 - 命令型言語での適用は、アスペクト指向による通信の割込みや後方スライシングで系譜を取り出す道がある。 ## 強み / 弱点・課題 - 強み: 反例が実在バグに対応する(健全)。有界の範囲で見逃しがない(完全)。Kafka のような合成起因の複雑なバグを少ない実行で再現する。系譜図で原因解釈を助ける。 - 弱点: Dedalus のような系譜と通信の割込みを提供する言語が前提である。同期モデルの単純化と内部決定性の仮定を置く。ビザンチン障害・クラッシュ回復・順序入替えを扱わない。否定ゴールの来歴は近似を含む。試作の対象は数十行の抽象モデルであり、本番実装ではない。