形式手法 (Formal Methods) についての調査
AWSがFormal Methodsを使っているというので、見てみる。分散アルゴリズムの検証に、形式手法が有効だったという話である。調べてみると、ACMの記事になる4年も前から、発表されていたらしい。
- 論文によると
- How Amazon Web Services Uses Formal Methods | April 2015 | Communications of the ACM
- AWSでは、2011年からFormal Methodsを使って、重要な分散システムのアルゴリズム設計を行っている。また、外部公開I/Fを単純化して提供することで、大規模な分散システムでサービスを提供できる秘訣となっている。AWSでは、顧客のデータを保護するために、フォールトトレラントな分散アルゴリズムを使っている。また、分散アルゴリズムはたくさんあるが、それらを組み合わせるのは難しい。
- TLA+は、プログラマがそのまま使うには記法になじみが無く使いにくい。しかし、TLA+の第二言語のPlusCalは、C言語に近くなじみやすい。とはいえ、記述の問題からTLA+を使っている開発者もいる。
- Formal Methodsを身に着けるのは大変といわれているが、ことTLA+に関してはそうでもない。AWSの開発者は、Formal Methodsの使い方を数週間程度で習得している。
- Formal Methodsの使い方としては、2つ考えている。一つ目は、障害をなくするという目的で使っている。もう一つの性能に関する問題は、ハードリアルタイム等の論理で対処すべきであるが、AWSのような複雑なシステムでは現状適用できていない。
- AWSにおけるFormal Methodsの取り組みは、SIGCOMM 2011でのChordにおけるAlloyの適用事例(Zaveによる)を見て、適用できるかを検討したことに発する。しかし、Alloyを使ってみたが表現等に制限がありAWSでは使用に耐えなかった。要件に合うFormal Methodsを探していたところ、TLA+に出会った。TLA+では、Paxos等の分散アルゴリズムを記述することが出来る。同僚にも、使うことを勧めたが、時間が取れずFormal Methodsを適用する取り組みは広がらなかったがまもなくニーズが出てくることになる。
- AWSではじめに有用性が実証されたのはDynamoDBである。レプリケーションとフォールトトレランスの仕組みを実装した。その検証ではフォールトインジェクション等を行った。さらに、アルゴリズムについてTLA+で記述し検証した。なお、TLA+の学習および記述は2週間程度で完了した。そして検証し、さまざまな障害を検出した。
- DynamoDBの成功をうけ、S3でも適用が開始された。その際、TLA+ではなく、PlusCalの適用のほうが生産性が良い場合があることも発見された。このため、TLA+だけでなくPlusCalも使われている。
- 別の論文も見てみる
- Obsolete URL
- これによると、1000行以内のTLA+もしくはPlusCalのコードを作成してモデル検証を行っているように見える。
- QconSFでのAmazonのテスト技術の進展に関する講演
- The Evolution of Testing Methodology at AWS: From Status Quo to Formal Methods with TLA+
- 講演者のTim Rath氏はDynamoDBにFormal Methodを適用した人。AWSの製品では初めての適用であった(はじめの論文より)。話の筋としては、今までの(非形式)手法での限界を示して、形式手法が良いという流れになっている。
- 一般的なテスト戦略
- 開発者 Unit Tests/Integration Tests
- リリーステスト Functional Tests/Performance Tests/Stress Tests/Failure Tests
- Test Adequency Criteria(7分)
- Status Quo(現状)とPerfect Criteriaを紹介
- Better testing of distributed algorithm(12分)
- Development start with specification(13分)
- 仕様をあらかじめ書く方法
- アルゴリズム(algorithm invariant)を確認する戦略
- Testing Starts with Development(15分)
- TDDプロセスへの疑問など
- コードカバレッジを拡張する戦略として紹介
- Assert system invariants(17分)
- Generative Testing(20分)
- さまざまなパラメータを入れてみて状態のテストを行う。
- HaskellのQuickCheckの逸話等を引用
- In Process Clusters(25分)
- Informal Proofs(34分)
- Formal Methods(36分)
- アルゴリズムを詳細に記述する必要がある。ツールで検証する。
- TLA+(39分)
- 現在の状態と次の状態を書くだけ
- 新卒のエンジニアでも2週間程度で習得できている。
- Real World Examples
- 当たり前なんだけど、We're hiringの文字があり、先端技術でも実用技術に落とし込んで使うという宣伝のようにも感じた。
- QA(48分)
- TLA+とコードの関係性をどうやって担保しているのか等々
- 2012年8月のTLAの研究会での発表論文にて
- http://tla2012.loria.fr/contributed/newcombe-slides.pdf
- Amazonのさまざまなレベルのエンジニアに対して、Formal Methodsを適用してもらったことがわかる。余談だが、DynamoDBは、Javaで出来ていることがわかる。
- 2011年10月の論文にて(12th International Workshop on High Performance Transaction Systems (HPTS))
- http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf
- TLA+やAlloyを学習する場合の入門資料等が36ページ近辺に記載されている。
- TLA+について
- Temporal Logic of Actionsの略でTLAと称する。Temporal Logicは日本語では時相論理と呼ぶ。
- First Order LogicとZermelo-Frankel set theory(ZF集合論)に基づいた記法である。
- TLA+のバイブルであるSpecifying Systemは、階段が低く作ってあって、多少の数学の心得があれば出来るように感じた。数学の導入ですら、2つの章かつ途中で例をはさんで入れているので、かなりゆっくり丁寧な説明のように感じる。もっとも、中島教授の資料で書いてあるように、産業界に広く受け入れられているZ記法ベースなので、導入されている数学記号が少なくわかりやすいという背景もある。
- PlusCalについて
- そのほか
- 形式手法は大まかに2つにわかれExplicit Model CheckerとSymbolic Model Checkerに分かれる。そして、SPINは、前者になり、AlloyおよびTLA+は、後者になる。で後者のほうが扱える状態が多いということらしい(土屋教授資料の29ページ辺り)
- 参考資料
- 概要
- 土屋教授の形式手法の紹介http://ws.cs.kobe-u.ac.jp/~masa-n/ses2011/ses2011_tutorial4.pdf
- 住井教授の形式手法の紹介(RSA2010)http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/RSA.ppt.pdf
- 中島教授の形式手法一覧紹介http://www.nii.ac.jp/TechReports/07-007J.pdf
- 形式手法ツール一覧
- TLA+
- 概要
- The TLA+ Home Page
- Specifying Systems(TLA+のバイブル。とはいえ、TLA+は新しくなっているので、次の資料で補足が必要)
- TLA+ Version 2
- TLA+の最新版の解説
- Model Checking TLA+ Specifications - Microsoft Research(Model Checking TLA+ Specifications)
- ソースコード
- TLAスクリプト例
- TLA適用事例
- AWS
- How Amazon Web Services Uses Formal Methods | April 2015 | Communications of the ACM
- Obsolete URL
- The Evolution of Testing Methodology at AWS: From Status Quo to Formal Methods with TLA+
- http://tla2012.loria.fr/contributed/newcombe-slides.pdf
- 2012年8月の発表資料
- HPTS - 2011 Agenda
- 2011年10月の発表資料(Newcombeのものがそれ)
- Other
- AWS
- VIM用のスクリプト
- PlusCal
- Obsolete URL
- http://research.microsoft.com/en-us/um/people/lamport/tla/c-manual.pdf(PlusCal Users manual for c-manual)
- http://research.microsoft.com/en-us/um/people/lamport/pubs/dcas.pdf(double-compare-and-swap, DCAS)
- An Example of Using PlusCal to Find a Bug
- Obsolete URL
- 概要
- ブログより
- AWSでEBSをやっている方のブログ(はじめの論文の著者の一人)
- AWS-VPのブログ
- Challenges in Designing at Scale: Formal Methods in Building Robust Distributed Systems – Perspectives
- Amazon DynamoDBの規模等が書いてある。単一リージョンで毎秒数百万のクエリ発行に耐え、ミリ秒以内の応答時間を実現している。
- 分散DBチームを中心にTLA+やPlusCalを使っている。フォールトトレラント分散アルゴリズムは、レプリケーション、コンシステンシ、コンカレンシー制御、プロビジョニング、そしてオートスケールの検証に用いられている。
- Challenges in Designing at Scale: Formal Methods in Building Robust Distributed Systems – Perspectives
- TLA+やPlusCalを使ってみた方のブログ
- AWS関係者
- はじめの論文の著者
- https://www.linkedin.com/in/brianbeckman
- その他
- 概要
