AWSにおける形式手法

AWSにおける形式手法の記事(https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf)を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。

  • 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である
  • アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた
  • 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる

以下は、読んでいる途中で書きだした要点。

  • AWSでは2011年以降形式仕様とモデル検査を使用している
  • 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレステスト、フォルトインジェクションテストなどだけでは確信を得るには不十分だった
  • システム設計で厄介な(見つけにくい)バグを見つけるには正確な記述が必要。従来のダイヤグラムは曖昧でテストできない。一方、ソースコードは非曖昧であるが詳細すぎる
  • そこで見つけたのがTLA+. TLA+ではシステムが持つべき特性と設計を同じ言語でかける。あらゆる抽象度で記述できて、検証は数学を使って推論してもいいし、モデル検査で検査してもいい
  • 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤りだった
  • アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた
  • 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる
  • 形式手法適用の良い効果として、良い設計のやり方が身につく。たいていのエンジニアがやる、正常ケースを考える、それから思いつく異常ケースに対応するでは網羅できない。システムが持つべき特性を書いてから設計し、検査する。その方がずっと設計エラーが少なくなる
  • 形式仕様を書くことでシステム稼働中ずっと恩恵が得られる。リリース後の機能追加やパフォーマンス改善のため変更を加えるときは「この変更は安全か?」を常に問われる。形式仕様とモデル検査がなければこの質問に自信をもって答えられない
  • こうした形式仕様とモデル検査を使った検証を経て開発者がシステムについて深く理解することができることも大きな利点のひとつ
  • テスト可能な形式仕様はすばらしいドキュメントでもある
  • 形式仕様で扱えなかった問題として、「徐々に低下するパフォーマンス問題」がある。これは論理的な誤りではないが、ユーザ視点からすると問題となる。TLA+ではリアルタイム安全性として応答時間の上限を扱うことができるが、OSやネットワークなどのハードウェアリアルタイムをサポートしていないインフラ上のソフトウェアには適さない。結局、その部分については別の手法を使った
  • 形式手法を始める前は、バグの発見のためにアサートを使っていたが、アサートはバグの影響を最小限に留めようとするが、ユーザデータの損失などを引き起こしたあとの状態からは回復させられない。これらのバグは避けなければならない
  • 最初は形式手法は候補ではなかったが、Pamela Zaveの論文で現実世界の問題に適用されていることを知り調査開始
  • 最初はAlloyを検討したが、自分たちのユースケースでは表現力が不足しているとしてTLA+を採用するに至る
  • DEC/Compaqにおけるキャッシュコヒーレンスの実例があったのもTLA+を採用するのに後押しになった
  • TLA+の表現力の高さはモデル検査の使用を考えるときに逆にその検査器の言語に変換できないことが考えられたが、実際には問題にはならなかった
  • 2012年、アマゾンはDynamoDBをローンチする。このDynamoDBでの適用が最初の大きな成功。
  • 開発者であるT.R.はフォルトインジェクションのテスト、ストレステストを行うも、それだけでは不十分とし設計を検証するためにTLA+を使う。TLA+で仕様を書き、TLCモデル検査で検証を行った。それにより、他の方法では見つけられなかった厄介なバグを発見。これは設計レビュー、コードレビュー、テストをすべてかいくぐってきたバグ。T.R.はこれらのバグを直して修正版のアルゴリズムをすべてモデル検査で検証。
  • T.R.曰く、形式仕様の記述と検査によるやり方は信頼できるし、非形式的な証明を書いたり検査するのに比べて時間もかからない。TLA+を使った方が市場へのリリースは早くできる
  • T.R.はDynamoDBローンチ後も新機能やパフォーマンス改善のときには既存のモデルに変更を加えて検査した
  • DynamoDBでの成功後、これをもっと広めるために社内のエンジニア向けに「設計をデバッグする」というタイトルでプレゼンする。エンジニアの先入観をさけるため、「形式」「検証」「証明」という用語は避けた。
  • プレゼン後、S3のチームが興味を示す。このチームでは状態遷移図で書かれたドキュメントがあり、これを網羅的にテストするJavaコードがあったが、もちろんこれはTLA+で置き換え可能。開発者のF.Z.は自分たちの問題にはTLA+よりPulsCalがより生産的として、そちらを使用。F.Z.はモデル検査で2つのバグを発見
  • その後マネジメントがTLA+を後押し。F.Z.は他のチームが仕様記述するのを手伝った。TLA+が早く広まった要因の一つは、この学んだ人がすぐに教える側に回れることにもある。
  • B.M.はすでに発見されていたバグの修正に関する仕様を記述して検査。それによりこの修正が別のバグを含んでいることを発見。さらにアルゴリズムのドキュメントの曖昧性をいくつか発見した。
  • M.B.とM.D.もPlusCalとTLA+を使用。M.B.はPlusCalで3つのバグを発見、M.D.はロックフリーの検査をPlusCalで行った。
  • Amazonでは、従来の設計文書をインクリメンタルにTLA+とPlusCalを使った記述に変更していった。この過程では、モデル検査をしたり仕様を書ききる前にシステムに関する重要な気付きが得られる。あるアルゴリズムでは、これにより大幅な最適化の案が得られた。
  • さらに最近になってTLA+はデータモデリングの優れたツールでもあることが分かった
  • TLA+を学ぶエンジニアはしばしばこう問う「検証した設計から実行可能な正しいコードはどうやって得るのか?」と。答えは「得られない」だ。しかし、形式手法はいくつもの方法で助けてくれる。例えば、
    • 形式手法は正しい設計を得るのを助けてくれる。正しい実装を得るにはまず正しい設計が必要。誤った設計からは誤った実装しか生まれない。
    • 形式手法は設計を深く理解することを助けてくれる。正しい実装は設計への深い理解から生まれる
    • 形式手法は、開発者が自己診断する実装を得るのを助けてくれる。システムが満たす不変条件がアサートで書かれる。形式手法はこの不変条件を見つけるのを助けてくれる。これにより良いアサートが組み込まれ、コードの品質が向上する
  • やりたいことは高い抽象度で書かれた仕様に対して、実装がその仕様を満たすか検証する、もしくは、仕様からコード生成することだが、既存の静的解析ツールは局所的な問題を指摘するだけでシステムワイドな検証をしてくれない
  • AWSにおいて形式手法は大成功を収めた。他の手法では発見できなかったバグを発見し、今では多くのチームがTLA+で仕様を書いている。経営陣もTLA+の使用を後押し。
  • 設計者は(検査したい)システムの振る舞いをモデルで表現する必要があるが、これは獲得するのが難しいという課題もある