Amazon S3の軽量形式手法
本記事は、形式検証 / 形式手法 Advent Calendar 2021 の 19 日目の記事です。
Amazon S3が形式手法を採用した論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読みました。
論文全体については、yohei-aさんがブログ記事で主要な部分を訳してくれています。本記事では自分なりのまとめに加えて、自分の形式手法導入の経験から思うところについても書いてみます。
論文は、Amazon S3の新しいKey ValueストレージのShardStoreの正当性を軽量形式手法で検証した話です。論文の主張をまとめると、
- 実装に使用した言語（Rust）と同じ言語で仕様となるリファレンスモデルを記述した。
- 検証したい性質によってツールを使い分けた。機能的な正しさおよびクラッシュ整合性の検証には、リファレンスモデルを用いたProperty based testing, 並行実行の検証には（こちらも実装言語そのままで検査できる）ステートレスなモデル検査器を使用。
- 開発初期は形式手法の専門家がリードしたが、エンジニアリングチームを教育して、彼ら自身でリファレンスモデルを維持、開発できるようにした。
です。これを読むと「なるほど、これは良さそうだ」と思い挑戦したくなるかもしません。しかし、いざ適用するとなると、悩ましい選択に直面するでしょう。例えば、今回の例では
- 専用のモデリング言語か、実装言語か
- 検証すべき性質はどの程度にすると効果的か
- リファレンスモデルの抽象度はどの程度に保つか
などです。論文ではそのあたりもつぶさに解説してあり、大変参考になります。彼らは変更され続けるシステムのため、エンジニアリングチーム自身が維持できることを主眼に選択しました。個人的には、専用の言語でも教育すればふつうのエンジニアでも使用することはできるようになると思います。言語よりむしろ検証したい性質をどこまで書くか？の選択が難しく、そのあたりはどの言語でモデリングしても問題としては残ります。ただ、プログラミング言語を使うことでCIに導入するのが簡単だったでしょうし、単体テストのモックとしても使えた、ということでプラスの面も大きかったのでしょう。こういった設計選択には形式手法の専門家の経験、助言がかなり役に立ちます。
軽量とありますが、一部でモデル検査や証明を使っていて現実的に導入できるものを全方位で取り組んでるように見えます。自らモデル検査器を開発したり、つよつよな解決法も見られますが、本論文で紹介されている一部でも導入することで効果は得られるでしょう。関連する事例*1やツールも参考になりそうでした。
個人的に今回の事例が成功している要因として、以下が大きかったと思います。
- 世界中のシステムのインフラであるため高い品質が求められ、それを実現することにそれ相応の工数をかけることが妥当であるという合意形成がなされていそう。
- 実装は効率、ロバスト性など高い非機能要求を実現するために複雑である一方、抽象度をあげた仕様は比較的単純である。
- 導入初期に形式手法の専門家の援助があり、早い段階で結果で示すことができた。
特に最後の点が大きいと思います。どんな手法でもそうですが早く結果で示すことが一番効果的です。それを達成するのに専門家の支援は大きいと思いますが、一般の開発現場ではなかなか手に入らないというのが現実でしょう。しかし、こういった論文が公開させることでノウハウが共有されれば専門家の支援なくともうまくやれる現場が出てくるかもしません。
以下、重要そうだなと思ったポイントあげておきます。
- フルの形式手法を適用するには非現実的とかんがえて、より弱い正当性の保証をねらって軽量形式手法を適用した。
- 実行可能なリファレンスモデル。これはシステムの期待する振る舞いを定義する。実装言語と同じ言語で書かれ、エンジニアチーム自身がメンテナンス、サイズは実装の約1%。ユニットテストのモックとしても使われ、新しいコードを書くときに効果的に変更されるようにした。
- すべての検査は自動化されていて、検証のためのインフラはコンパクト（コードベースの12%）。従来のテスト手法やコードレビューでは見つけられない16個の不具合を発見。
- リファレンスモデルでは、限られた方法でしか失敗させられない（追加してないキーの読み出しに失敗するとか）。IOエラーやリソース枯渇のエラーはリファレンスモデルには省略した。Availabilityやパフォーマンステストを犠牲にすることになるが、モデルをシンプルに保つことを選択した。
- リファレンスモデルを実装言語と同じにしたのは設計上の選択。他のモデリング専用言語（Alloy, Promela, Pなど）を検討したが、エンジニアの認知コストと学習コストを抑えるための選択。
- リファレンスモデル自身の検証にPrustiを使用した。例えば、LSM-treeのリファレンスモデルでは、キーバリューのペアが削除させるのはdelete操作のときのみを証明した。
- リファレンスモデルと振る舞いが等しいことをどこまで検査するかは難しい。
- カバレッジを上げるために入力にバイアスをかけた。例えば、PutとGetの操作に渡されるキーが一致することは稀なので、ほとんどのGetは失敗する（成功するテストがほとんどされない）。Putしたキーが選ばれやすく確率をあげる。しかし、やりすぎてはいけない。そもそも形式手法を採用する目的は自分たちが想定してないことを見つけてくれることを期待しているので、バイアスをかけすぎて自分たちの想定内しかテストされないという事態は避けねばならない。
- Disk IOエラーの適合テストではチェックを緩めた。実装はどこでエラーが起きたかでその後の振る舞いが異なるが、それをリファレンスモデルで再現しようとすると複雑になるため。エラー時にはフラグを立てて、結果がある程度一致しないことを許した（例えば、エラー時のGetでは何もデータを返さないのを許容するが、誤ったデータを返すことは許容しない）。
- リソース枯渇に関してはプロパティベースなテストを適用しないことにした。実装に伴うメタデータなどのオーバーヘッドを抽象モデルに入れることが難しいので。
クラッシュ整合性を検査するのに、仕様として2.2節で説明したDependencyについてふたつの特性を定義した。
- 永続性。Dependencyがクラッシュする前に操作が永続的であったとならば、クラッシュ後に読み取り可能である
- 前進性。クラッシュがないシャットダウンの後は、すべてのDependencyは永続的であるべき*2
前進性は、決して完了しない操作をはじくことができる。実装が返すDependencyはクラッシュ整合性を満たすためにより強いこともありうるが、永続性により弱すぎないことを保証する。
- DirtyRebootという操作を追加してクラッシュを模擬。揮発性メモリのどこが永続化されるかコンポーネントレベルで指定可能にした。それより細かいブロックレベルの指定はテストが遅くなる割に効果が薄いのでデフォルトでは使用していない。
- Rust内に残るundafeのコードを検証するためにMiri interpreterを使用した。並行プリミティブをサポートするために手を加えた。
- デシリアライズの検証にはCruxを用いて、パニックが起こらないことを証明した。
- すべてのバグは自動化されたツールにより発見された。デバッグがエンジニアにより行われるのは従来どおりだが、ツールが最小の反例を示すことでそれを助けた。この手法がバグを防ぐことに有効だった。エンジニアたちはこの検査で見つけたバグをコードレビューで見つけられないと語った。
- 形式手法の専門家がふたりフルタイムで9ヶ月、3人目は3ヶ月参加。彼らはリファレンスモデルとテストハーネスの初期の開発をリードした。その後はエンジニアリングチーム自身（全員が形式手法の経験なし）が開発した。git blameによるとエンジニアリングチームによるコード編集はテストハーネスの18%。
- 本手法でもバグを見逃すことがある。実際、今回のツールでは見つけるべきバグが見つけられず、コードレビューのときに見つけたものがあった。これはキャシュを導入する変更で、はじめテストハーネスでのキャシュサイズを大きくしていたため見つけられなかった。キャシュサイズを小さくすると見つけられるようになった。この件がきっかけになり、カバレッジ計測を入れることになった。
- 開発の早い段階で導入すること。ひとつのコンポーネントからはじめて、リファレンスモデルを作ったらすぐにコードベースに統合し、エンジニアを教育機関すること。これにより、早期にバグを発見した。この結果、エンジニアの興味を強く引くことになった。
- リファレンスモデルをコードベースに統合しておくことは、時間の経過とともにコードが変更される状況において検証を有効に保つのに欠かせない。実装言語と同じRustでモデルを書くことはオーバーヘッドを少なくし、エンジニアに仕様を書かせるためのひとつの方法である。
