AWSにおける形式手法の適用2015年10月21日 10:56

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

How Amazon Web Services Uses Formal Methods

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

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

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

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

※TLA+の解説

スノーデン以後のプライバシー意識2015年10月21日 11:51

Communications of the ACMの2015年5月号から。

スノーデン以後のプライバシー意識

スノーデン以後の米国民のプライバシー意識についての調査報告。本稿によると2013年の暴露以後、プライバシーを守るという行動は高まりを見せたものの、すぐに元に戻り、現在ではむしろ低下しているという。

懸念はあるのかもしれないが、便利なものは使ってしまう、ということか。感覚としては、身内や近所で話をしているのと変わらないのかもしれないが、今の技術では見知らぬ人や機関がそれを記録して、利用することができるようになっている。本人が気にしないならよいのでは、という意見もあろうが、自由と独立を口にするなら意識的でありたい。

別稿になるが、知的財産権(Intellectual Property)についての記事で、Bill Gatesが言ったという格言が面白い。

Intellectual Property has the shelf life of a banana.
知的財産権の賞味期限は、バナナなみ(に短い)。

これを伸ばそうという動きについて議論するのだが、バナナの対極におかれたのが、Twinkiesというお菓子。少し前に、製造を止めるといって大きなニュースになっていた。