まだ構築されていないシステムのレジリエンスの欠陥をどう発見するか？

設計そのものを分析可能なシステムとして扱えば、コードを書く前に、システムの最も危険な欠陥の一部を発見できる。Hillel Wayneの講演はこの点を中心に、形式手法の原則が、将来のシステムを検証し、レジリエンス、並行性、障害に関する問題が運用上のエラーになる前に発見する方法を説明している。

Wayneはまず、彼が「タスク実行器」と呼ぶものの簡略化した例から始める。システムはタスクが完了したかどうかを確認し、完了マークを付け、その後でタスクを実行する。この順序は論理的に見えるが、実行中に障害が発生すると破綻する。タスクを完了として記録した後に再試行されるため、タスクが実際には実行されない可能性があるからだ。完了の記録を実行後に移すと、別の問題が現れる。どちらも完了を記録する前に、並行して動作する2つの実行器が同じタスクを2回実行できてしまう。

これは理論上の問題にとどまらない。講演では、注文を2回送信する可能性がある荷物発送システム、同じ予約枠を2人に予約してしまうスケジューリングシステム、要求の反復によって破壊的な挙動に陥る可能性があるアプリケーションのインストール機構などの例と関連付けている。

「正しい」とは何かを定義することから始める

Wayneは、システム要件を二値の特性として定式化することを提案する。つまり、特性は真であるか偽であるかのいずれかである。例として、タスクが複数回実行されないことが挙げられる。これは悪い事象の発生を防ぐ安全性特性である。また、タスクが少なくとも1回実行されることは、必要な事象の発生を保証する活性特性である。

講演では、特性は同じ強さではないことを強調している。毎秒10,000件のクエリを処理できるシステムは、毎秒2件のクエリを処理するという特性を自動的に満たすが、逆は成り立たない。そのため、強い特性を通過することは、複数の弱い特性が正しいことの証拠になり得る一方、弱い特性の失敗は問題の原因範囲を絞り込むのに役立つ。Wayneはこの考えをテストのピラミッドと関連付けている。多数の単体テストは、限られた数のエンドツーエンドテストよりも、エラーの診断に有用な場合がある。

簡略化したモデルが根本的な問題を明らかにする

システムをあらゆる詳細とともに表現するのではなく、Wayneは必要最小限の状態を含む抽象モデルを構築するよう勧めている。そこには、アルゴリズムの現在の段階、タスクが完了としてマークされているかどうか、実行回数が含まれる。これにより、障害や再試行の状態も含め、可能な状態とシステムが進み得る経路を探索できる。

形式手法では、このモデルと特性を論理式で符号化し、モデル検査器やSMTソルバーなどのツールで検証できる。しかし、講演で示される実践的な考え方は、これらのツールを直接使うことを必要としない。エンジニアは、状態と起こり得る遷移を追跡することで、同じ思考方法を取り入れられる。

並行性と障害における「敵対者」の要因

Wayneは、ユーザー入力、並行性、ランダム性、タイムアウト、サーバーの停止など、不確定性の原因となるものをすべて、常に最悪の結果を選択する「敵対者」として捉えることを提案している。システムが無限に再試行する可能性があるなら、この敵対者は毎回障害を選択する。その結果、理論上は成功が可能であっても、活性特性が保証されていないことが明らかになる。

また、並行して動作する2つの実行器が存在する場合、一部の変数を各プロセスに固有のものとして、その他の変数をシステムと外部世界の間で共有されるものとして表現する必要があることも説明している。異なる実行順序を探索することで、各実行器を単独では健全に見える場合でも、タスクが2回実行される状態に到達できる。

仮定は設計の一部である

システムの正しさは、その特性だけでなく、システムが動作する環境に関する仮定にも依存する。ある設計ではプロセスがまったく失敗しないという強い仮定が必要になる一方、別の設計では障害が限られた回数だけ発生する場合に動作できることがある。Wayneは、手順の順序を変更すれば活性に関する仮定を緩和できる可能性があるが、同時に安全性の要件が増える場合があると指摘する。例えば、常に1つの実行器だけが存在することを保証する必要が生じる。

実行環境が変わると状況も変化する。データベースの強整合性に依存した後で最終的整合性へ移行すると、システムのコードが変わっていなくても、以前は正しかった特性が保証されなくなる可能性がある。したがって、サービスプロバイダーやデータベースに関する仮定を外部の細部と見なすべきではない。それらは設計の正しさに直接関わる条件だからである。

実際には何が変わるのか？

この手法の実践的な価値は、テストを置き換えることでも、すべてのプロジェクトで形式手法のツールを使うよう求めることでもない。設計に関する問いをより厳密にすることにある。どのような状態が可能か。どのような事象の順序が最悪か。実際に制御できるものは何か。チームが保証できない仮定は何か。必要な特性が強いほど、また環境の予測可能性が低いほど、システムにはより複雑な設計が必要になるか、要求する特性を緩和する必要がある。例えば、「すべてのメッセージを処理する」という条件を、「メッセージを処理するか、デッドレターキューに送る」という条件に変更することが考えられる。

Wayneはこれらの考えを、形式手法から得られた思考の道具として紹介しており、工学的判断に代わる既製の解決策として扱ってはいない。どのシステムでも、モデルと使用した仮定がどれほど正確かという未解決の問題が残る。状態を1つでも見落としたり、環境が保証していない挙動をチームが仮定したりすれば、実際のシステムとは異なるモデルが正しいことを分析によって証明してしまう可能性がある。