第十四工房

Communications of the ACM、2015年4月号から。AWSで形式手法(Fomal Methods)を適用して成果を上げているとの記事の寄稿。

クラウドのサービスを利用することがあたりまえになってきた中、それらのサービスの品質が満足行くものか、一抹の不安を抱えながら、ということはよくある。本稿は、AWSでS3やDynamoDBなどの構築に携わった面々が、形式手法を適用して、簡単には見つからない設計バグの解消に取り組んだ事例を報告する。

バグを解消する、というと、幾多のレビューを受け、考えられるだけのテストケースと負荷試験を十分な時間を掛けて実施し、というのがよくあるが、AWSのように同時並行で多数の処理が動き、それぞれが複雑に作用し合うサービスでは、それだけでは十分でなかった。その解決を模索する中で、形式手法にたどりつき、DynamoDBのプロジェクトで成果を上げてから、S3をはじめ、他のプロジェクトに普及していったという。

トラブルが発生すると、どれだけの人と時間を投入して改善した、ミスを発生させた人員にはペナルティを課す、監視システムを充実させた、などの対応策を説明されることがあるが、これらで本当にトラブルがなくなるのか、納得するのは難しいのが本当のところ。その点、本稿にあるようなAWSの取り組みは本質に迫り、安心感を高める。

なお、Amazonが、自社のプロジェクトに適していると判断したのは、TLA+とそれを元にしたアルゴリズム記述言語のPlusCal。ちょっと見た感じ、記号論理学で習った記述に近しいやり方で、処理のロジック(アルゴリズム)を書き下している。

※TLA+の解説