ハクソク

世界を動かす技術を、日本語で。

Amazon Web Servicesにおけるシステムの正確性実践

360日前原文(cacm.acm.org)

概要

  • AWS は信頼できるサービス提供のため、 システムの正確性 を最重視
  • TLA+やP言語 など形式手法の導入で、開発初期にバグ発見・性能最適化を実現
  • 軽量形式手法 （プロパティベーステスト、ファジング等）も積極活用
  • Fault Injection Service で障害注入テストを顧客にも提供
  • メタスタビリティ など新たなシステム障害への対応も進展

AWSにおける形式手法の活用

  • AWS では、信頼性・セキュリティ・耐久性・可用性のために システムの正確性 を重視
  • TLA+ の利用により、開発初期で伝統的なテストでは見逃すバグを発見
  • 正確性担保により、 積極的な性能最適化 も安心して実施可能
  • 以前は ユニットテスト 中心だったが、今は 形式手法 を開発工程に統合
  • 形式手法の活用で 開発速度 と コスト効率 を両立

TLA+とP言語の導入

  • TLA+ は抽象度が高く、 数学的記述 が特徴
  • 一部エンジニアには難解だったため、より親しみやすい P言語 を導入
  • P言語 は状態機械ベースで、 分散システム設計 に適合
  • Amazon S3やDynamoDB、Aurora等の設計検証に活用
  • PObserve ツールで、テスト・本番両方で設計仕様との整合性を検証

軽量形式手法の実践

  • プロパティベーステスト をAmazon S3のShardStore開発で活用
    • 正確性仕様・カバレッジ指向ファジング・障害注入・最小化を組み合わせ
  • 決定的シミュレーションテスト で分散システムの複雑な動作を制御して検証
    • スケジューラ拡張で順序のファジングや全探索も可能
    • shuttleやturmoil等のOSSとして公開
  • 継続的ファジング でAuroraのデータシャーディング機能を検証
    • SQLクエリやトランザクションを自動生成し、非シャーディング版と比較
    • 障害注入と組み合わせて、原子性・一貫性・分離性も検証

Fault Injection Service（FIS）の提供

  • 2021年 に Fault Injection Service をローンチ
  • APIエラーやI/O停止等の障害を 本番環境 にも注入可能
  • 顧客自身がレジリエンスや可用性を検証できる環境を提供
  • Prime Day準備で733件のFISテストを実施
  • 障害注入と形式仕様を組み合わせることで、 バグ発見力 を強化

メタスタビリティと新たな障害形態への対応

  • 一度異常状態に陥ると通常の操作では回復しない メタスタビリティ障害 が注目
  • 負荷増加→輻輳→グッドプット低下→回復不能の流れが典型
  • 多くの分散システムで、タイムアウト・リトライ等で発生しやすい
  • 従来の「安全性」「活性」だけでは捉えきれない新たなシステム挙動への対応が必要

まとめ

  • AWS は形式手法と軽量形式手法の両輪で、 正確性・性能・開発速度 を高次元で両立
  • P言語 や FIS 等の独自ツール・サービスで、社内外のエンジニアリングを支援
  • 今後も メタスタビリティ 等の新しい課題に積極的に取り組む方針

Hackerたちの意見

すごいな。数年前にレスリー・ランポートとやり取りしてたことがあるんだけど（彼のバリダンの原理に関する論文とかね）。今日、彼のウェブサイトに行ったら、TLA+やPlusCalについてたくさんのことがわかったよ。彼は今でもそれを維持してるんだね：https://lamport.azurewebsites.net/tla/peterson.html?back-lin... こういう数学をプログラミングに持ち込んだ人が、AWSや他の産業で使われるシステム設計言語を作るのは、全く理にかなってると思う。もっと分散システムを作る人たちが、彼が作ったものを使ってくれたらいいのに。大規模なシステムでは正しさを証明することがめっちゃ重要だからね。

└

興味がある人へのちょっとしたヒントだけど、エクステンデッド・シンキングを使ったクロード・オーパスは、既存のコードをTLA+の仕様に変換するのがすごく得意みたい。個人的なRustプロジェクトで複数のバグを見つけたことがあるし（180度ターンできるスネークゲームとか）、仕事でも小さなC++コンポーネントを確認したことがあるよ（ロックや生存性に関する特定のプロパティを持つキューとか）。他のモデルも試したけど、オーパス以外では構文や仕様の論理で問題が出てばかりだった。

└

大規模なシステムでは正しさを証明することがめっちゃ重要。小規模でも良いけど、SSHやターミナルみたいな重要で広く使われているユーティリティでは特にね。

└

大規模なシステムでは正しさを証明することがめっちゃ重要。そんなことはできないよ… モデルチェッカーは、仕様があなたが書いたプロパティを満たしていると言ってるけど、探索した有限状態空間の中でね…

面白そうだけど、AWSで働いたことがないし、TLA+やPにも詳しくないから、どちらかの「Hello World」例を見てみたかったな。それがないと、良い設計やテストプロセスで捕まえられるはずのことに、余計な苦労が増える気がする。記事の中に基本的な例があれば、これらが実際に何をするのかをもっと理解できたのに。

└

フォーマルメソッドを使う全体の目的は、テストでは絶対にすべてをキャッチできないからだよ。

└

TLA Plusの例のリポジトリはすごく良いよ：https://github.com/tlaplus/Examples。DieHard問題みたいなシンプルなものから始めるのをおすすめする。

└

テストは特定の問題のクラスの具体的なインスタンスを扱い、その実装がこれらのインスタンスに対して正しいことを証明します。形式的検証は全体のクラスを証明します。例えば、アナグラムを返す関数があって、テストでいくつかの単語のペアに対して正しいことが証明されるかもしれません。でも、すべての単語に対して証明するには形式的検証が必要です。そうすることで、未定義の動作やライブラリのバグによる厄介なエラーを見つけることができるんです。なぜなら、それらの意味を証明できないからです。

└

良いデザインがここでたくさんの重い作業をしているね。TLA+/Pluscalの目的は、デザインの健全性の証明を持つことなんだ。

決定論的シミュレーション。AWSで広く使われているもう一つの軽量な方法は、決定論的シミュレーションテストで、分散システムを単一スレッドのシミュレーター上で実行し、スレッドのスケジューリング、タイミング、メッセージの配信順序などのすべてのランダム性のソースを制御するんだ。特定の失敗や成功シナリオに対してテストが書かれるんだけど、例えば分散プロトコルの特定の段階での参加者の失敗とかね。システム内の非決定性はテストフレームワークによって制御されて、開発者が興味深いと思う順序（過去にバグを引き起こしたものなど）を指定できるようになってる。テストフレームワークのスケジューラーは、順序のファジングやテストするすべての可能な順序を探索するために拡張できるんだ。これを実現する良いオープンソースライブラリって、言語に依存しないものはあるかな？できそうだね、ツールをいくつか入れたコンテナを立ち上げるだけで。これらのツールは、テストがいつ実行されるかを知るためのミドルウェアが必要で、テストが実行されるときに、ネットワーキングやストレージなどの「決定論的」なものを作るんだ。このやり方は、アンチテーゼがやってることに近いけど、まだオープンソースのものは見たことがないな。もちろん、テストをうまく書けばI/Oをスタブアウトできるけど、それは手間だし、みんながうまくテストを書くわけじゃないからね（もちろん、そうするべきだけど、アプリケーションより上のレイヤーでこの決定論がある方がいいと思う）。ちょっと余談だけど、AIにはあまり期待してないけど、テストはAIが輝く分野の一つだと思う。プロンプト中のフィードバックループが実際のアプリケーション要件に基づいて進められるから、テストの実装（AIによって駆動される）、要件（プロンプトによって駆動される）、そして「世界」（実際にテストされるコードによって駆動される）が、理論的な理想に向かって進む手助けができるといいな。もしAIが何かをもたらしてくれるなら、フォーマルな検証をもっと実現可能にして、ソフトウェアをより厳格な分野にしてくれることを願ってる。

└

DSTには歴史的に2つの大きな採用の課題があったんだ。(1) 以前は、シミュレーションフレームワークの一つに全システムを組み込まなきゃいけなかったし、依存関係を持たないようにしなきゃいけなかった。(2) 弱い検索や入力生成で自分を騙すのが簡単すぎて、実際には何も重要なことをテストしてないのに、全てのテストが合格に見えちゃう。君が言うように、Antithesisはこの2つの問題を解決しようとしてるけど、すごく難しいんだよね。任意のソフトウェアに決定論を適用する信頼できる方法を知ってる人はいないと思う。FacebookのHermitプロジェクトは、決定論的なLinuxユーザースペースでこれを試みたけど、結局は放棄されたんだ。（実は、私たちもハイパーバイザーを書く前に同じことを試したけど、うまくいかなかった。）決定論的なコンピュータは、テストだけじゃなくて一般的に役立つ技術の基本なんだ。いつか誰かがそれを作るだろうし、私たちのものをオープンソースにするかもしれないね。

└

https://apple.github.io/foundationdb/testing.html https://www.youtube.com/watch?v=4fFDFbi3toc

P言語について気になったことがあるんだけど、初期の頃、MicrosoftでWindowsのUSBスタックで実際に使われるCコードを生成するために使われていたってこと？でも今はもうプロダクションコードを生成するためには使われてないのかな？ここでその質問をしたんだけど、トークでも同じ質問があったと思う：https://news.ycombinator.com/item?id=34284557 生成されたコードがカーネルで使われるなら、リソース制約の少ないクラウドでも使えるんじゃないかな。

└

Azureで使われているCoyoteは、P#の進化版で、Pの進化版だったみたいだね。

すごい記事だね！インフラのコントロールプレーンを作るなら、状態遷移機を使うのは必須だよね。でもPは必須だったのかな？ちょっとわからないな。私たちは13年以上インフラのコントロールプレーンを作ってきて、毎回Rubyで構築してきたんだ。それがすごくうまくいったよ。https://www.ubicloud.com/blog/building-infrastructure-contro...

ちょっと気になるんだけど、誰か自分の分散サービスでFISを使ったことある？使おうか考えてるんだけど、そういう実験を扱った実際の経験がないんだよね。

92%の統計は本当に興味深いね！クラスターがダウンするのは、滅多に派手なクラッシュじゃないんだ。むしろ、「無害な」リトライが状態を漏らし続けて、運命の金曜日の午前2時にすべてが壊れるんだ。明らかに、明白な災害よりも、平凡で静かな失敗にもっとエンジニアリングの時間を予算に入れるべきだね。そこに問題が隠れてるんだ。

└

それか生存者バイアスかな：大きな問題は解決されたから問題を引き起こさないけど、解決されていない小さな問題がランダムに大きな問題を引き起こすことがある。

記事で説明されている内容よりも、PromelaとSPINはより高いレベルにあると言ってもいいかな？

└

私（著者の一人）は約10年前にPromelaを使って分散システムの仕事をしたことがあるけど、あんまりドメインに合ってる感じはしなかったな。面白いアイデアはあるし、いつか再訪する価値はあるかもね。

S3は、私が見た中で最も素晴らしいソフトウェアの一つだよ。数年前に、全システムに強い読み書き後の整合性を追加したってこと？信じられないほどのソフトウェアエンジニアリングだね。https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-rea...

└

Google Cloud StorageはS3のずっと前からあったよ。GCSはかなり考え抜かれた、しっかりした製品に見えるね。

より軽量な半形式的アプローチ（プロパティベースのテスト、ファジング、ランタイムモニタリングなど） うん、プロパティベースのテストとファジングが形式的手法と関係があるのはわかるけど、ランタイムモニタリングを「半形式的アプローチ」と呼ぶのはちょっと無理がある気がする。

└

PObserveみたいなものでのランタイムモニタリングは半形式的アプローチだよ。普通のアラームやメトリクスだけじゃないからね。