背景

社内で形式手法の勉強会が行われた。このリンクの内容。全3回のうちの第1回らしい。
形式手法は知ってはいたけど、非常にコストが高く実務的ではないという認識だった。この勉強会は、クラウドなど産業界で実際に使われている事例を紹介して、興味を持つことを目指しているようだった。

勉強会のスライドを読み進めると、上記リンク中の参考資料1「Amazon Web Services はどのように形式手法を利用したか」を読むよう記載されており、読んでみると非常に興味深いものだった。
勉強会第一回の内容と合わせて、面白いと思ったところをまとめてみる。

AWSでの形式手法の利用

報道されるような重要なシステムでの大規模障害の原因は様々で、対処方法も複数ある。
仕様の誤りに形式手法で対応できれば、正確な仕様を元にした実装とテストができ、障害を防ぐことができる。
障害発生後の原因は調査しやすいが、障害発生前に防ぐことは難しい。形式手法ならそれができる。
クラウドのような大規模かつ複雑な並列・分散システムでは、ハードウェアや人間のエラーも想定しなければならない。このような複雑な仕様を、検証可能で表現力のある形式手法で取り扱うことが必要となっている。

形式手法で検証可能な仕様が記載されれば、そこから実装を生成することもできるかもしれない。その場合、実装する人間は仕事が少なくなるかもしれない。
しかし、仕様を作成する仕事は創造性が求められ、これは人間にしかできない。

Amazon Web Services はどのように形式手法を利用したか

形式手法ではない、業界で一般的な方法では、大規模分散システムのレアケースを未然に発見することはできなかった。
この問題を解決することを目標として、代替手段を探し始めた。

複雑な仕様を厳密に記述しつつ、記述量を抑制するソリューションとして、TLA+を見出した。
TLA+は離散数学に基づいた形式的仕様記述言語で、モデルチェッカーはもちろん、疑似コードを置き換える表現力を持つPlusCal言語を備えている。

設計にTLA+を使うことの副次的な利点として、人間の設計手法を向上させることがある。
TLAによらない既存の手法では、まずビジネス要求に応える最短のハッピーケースを設計し、その後でエンジニア個人の知識と経験に基づき問題点の検討を行う。この場合、能力を超える複雑な問題を見つけることはできない。
TLA+の場合はまず「正しく進むには何が必要か」というシステム特性を、安全性と生存性の観点から記述することから始まる。次に、ハードウェアの異常や人間のミスなど、起こりうる動的イベントを特定する。その後、モデルチェッカーで仕様の正しさを確認する。
前者は「うまくいかないもの」をアドホックに見つけ、後者は「正しく進むために必要なもの」を厳密に特定する。

形式手法はまた、仕様が安全であること、または安全ではないことを、事前に知ることができる。
さらに、優れたドキュメントとして機能する。

さらに、設計の正確でテスト可能な、十分にコメントされた記述は、優れた形式のドキュメントである。というのも、AWS システムのライフタイムには期限がないため、このことは、重要である。
時間が経過し、ビジネスの成⻑とともにチームも成⻑する。そのため、我々は定期的に新しい人々をシステムに慣れさせる必要がある。この教育は効果的でなければならない。微妙なバグを作らないようにするには、すべてのエンジニアがシステムの同じメンタルモデルを持つことが必要なのだが、その共有モデルは、精密で正確で完全である必要がある。
エンジニアはさまざまな方法でメンタルモデルを形成する。互いに話し合ったり、設計ドキュメントを読んだり、コードを読んだり、バグ修正や小さな機能を実装したりする。 しかし、会話や設計のドキュメントはあいまいであったり不完全であったりする。実行可能コードが大きすぎてすぐに理解できなかったり、あるいはそのコードは意図したデザインを正確に反映していない場合があるのだ。 対照的に、形式仕様は、正確で短く、ツールを使用して調査や実験ができる。

TLA+に向いていないこともある。AWSのインフラはハード・リアルタイムスケジューリングをサポートしておらず、サービスに対しては一定以上の遅延をエラーとみなすソフト・リアルタイムスケジューリングが要求されている。
TLA+では安全上の特性として応答時間の上限を設定できるが、このギャップを埋めるには至っていない。

AWSでの形式手法の導入経緯

バグを防ぐ手法を模索する上で、形式手法はROIが低いという偏見があり、当初は検討されていなかった。
ある時、形式手法言語Alloyによって分散システムのメンバーシップ・プロトコルChordの不具合を見つけたことで、有用性を認識した。
Allowの表現力不足を解決する方法を模索していた際、LamportのFast Paxos論文のAppendixにTLA+仕様が記載されていることを見つけた。
Paxosアルゴリズム作成者がTLA+を作ったという事実は、TLA+の実用性を確信させるものだった。

Lamport, L. Fast Paxos. Distrib. Comput. 19, 79–103 (2006). https://doi.org/10.1007/s00446-006-0005-x
※自分は論文へのアクセス権を持っていないので未確認

発見者はAmazonの同僚にTLA+を薦めたが、必要性がなく導入はされなかった。
しかしDynamoDBで採用され、TLA＋の学習と仕様記述を2週間で行い、8Coreと23GBのEC2インスタンス10台でモデルチェッカーの分散バージョンを実行して、データが失われるバグを発見した。
このDynamoDBでの成功と、社内へのプレゼンテーションの工夫によって、TLA+を伝える試みを改善させた。

エンジニアは「検証」ではなくデバッグの観点から考えるため、プレゼンテーションでは「設計のデバッグ」と呼んだ[18]。こうしたメタファーを続けながら、エンジニアは、「徹底的にテスト可能な疑似コード」と呼ぶと、TLA+の概念と実用的な価値をより簡単に把握できることに気づいた。 形式手法は実践的ではないと広く見られていたため、最初は「形式」、「検証」、「証明」という言葉を使うのを避けた。また、我々は、最初に TLA が何を表すのかについて言及することは避けた。

このような活動によって、S3のチームから導入サポートの依頼があった。

結果として、2011年から現在に至るまで、AWSでは形式手法が用いられている。