形式手法による分散システムの検証 accepted

Abstract

本セッションでは、形式手法 (formal methods) を用いた分散システムの設計および実装について解説します。形式手法は、数学的な表現を用いて対象となるシステムを定式化することにより、システムの挙動の「正しさ」を厳密に保証するための方法論です。受講対象は予備知識を持たない初心者を想定しており、具体例を通して形式手法の基本的なアイデアを知ることを目標とします。

分散システムのメリットとデメリット

近年、複数のコンポーネントが非同期的に連携して動作する分散システムは決して珍しいものではなくなりました。正しく設計された分散システムは、集中システムとは比較にならないフレキシビリティとスケーラビリティを発揮します。人気 OSS の中にも分散型の設計を取るものは多数見られ、一昔前のように一部の専門家だけに任せておくだけでなく、すべてのエンジニアにとって一種の基礎教養になっているといってよいでしょう。

しかし同時に、分散システムの設計や実装には特有の難しさがあります。複数のコンポーネントがそれぞれ独立して動作するとき、システム全体としての動作パターンは組み合わせ爆発的に複雑になり、人間が頭の中で扱える範囲を容易に超えてしまいます。また、動作のタイミングに依存するタイプのバグはそもそも再現すること自体が難しく、ソースコードに対する古典的なテストで検出することは原理的に困難です。

分散システムを検証する戦略

分散システムに内在する難しさを克服する手法として、いわゆるカオステスト (chaos testing) が利用されることがあります。カオステストは、実際の環境上で故意に障害を発生させることにより、システムの可用性や復元性を継続的に担保するための仕組みです。システムのライフサイクルを「開発」「テスト」「運用」の三段階に分類するとしたら、カオステストは、「テスト」のフェイズで保証することが難しい分散システムの性質を「運用」のフェイズで肩代わりする手法と言えるでしょう。

それでは、逆の考え方をするとどうなるでしょうか? すなわちシステムが期待通りに動作することを「運用」フェイズで確かめるのではなく、逆に「開発」フェイズやさらにその前段階である設計の中に織り込むことができたら? 実際に出来上がったものを動かしてみるのではなく、いわゆる「仕様バグ」の段階で機械的に検出することができたら? これが実現すれば、当然ながら運用中に発見されるよりも影響が少なく済み、最終的なシステムの信頼性も向上することが期待できます。

形式手法の威力

このアイデアを実現する手段の一つとして、形式手法が知られています。形式手法は、数学的な理論に基づいてシステムを厳密な形式で表現することで、従来のテストでは確認できないようなシステムの振る舞いを保証するための方法論です。先に挙げたような、システムの組み合わせ爆発的な複雑化が起こる状況においても、適切な抽象化を行うことで、背景にある理論を援用した効率的な検証が可能になります。

本セッションでは、シンプルな分散アルゴリズムを例として取り上げ、その性質がどのように形式化されるかについて理論と具体例の両面から解説を行います。より具体的には、オートマトン時相論理 (temporal logic) をベースとした形式化を通じて、例えば以下のような性質を扱います。

  • 複数のコンポーネントが共有データにアクセスする。各コンポーネントがそれぞれロック・アンロックのロジックを実装しているとき、同時に動作させてもデータが不整合に陥るパターンが存在しないか?

  • 遅延が発生するネットワーク間で複数のコンポーネントが接続されている。特定のプロトコルでコンポーネント同士が通信するとき、最終的にデータが正しく伝達されるか?

いずれも、従来のテストでは記述しづらい条件です。形式手法の強みは、このような条件を あいまいさのない形で表現し、機械的に、かつ実際にアプリケーションを実行することなく静的に検証することができる 点にあります。

なお、セッション中にはいくつかの検証ツールも登場しますが、ツールの使い方の解説は目的としません。主題はあくまでも「いかにして検証可能な形でシステムを定式化するか」の考え方をお伝えすることです。

想定する受講者層

本セッションは初心者を対象にしており、形式手法に関する予備知識は仮定しません。分散システムに関する知識も基本的には必要ありませんが、何かしらの分散アルゴリズムに触れた経験があれば、より興味深く聞いて頂けると思います。

補足

申請者は、これまでにも複数のカンファレンスで形式手法に関する登壇を行っています。

特に July Tech Festa 2018 の発表は分散システムを扱う点で今回のプロポーザルと似ていますが、前回の発表でツールの比較に時間を割いたのに対し、今回のプロポーザルは理論的な側面に焦点を当てており、対照的・相補的な内容になっています。

Session Information
Confirmed confirmed
Starts On 8/31/19, 1:00 PM
Room Centennial Hall A
Session Duration 50 min session
Spoken Language Japanese
Interpretation Unavailable
Slide Language Japanese