IronFleet: 分散システム検証の方法論
- 共有
-
- |
後で読む
マイリーディングリスト
Microsoftの研究者グループが論文“IronFleet: Proving Practical Distributed Systems Correct” (PDF)の発表に合わせて，非自明な分散システムの正当性を安全性(safety)と活性(liveliness)の観点から証明することで，方法論をマシン上で証明するためのソースコードを公開した。
複数のマシン上でコードが並列実行されることによるバグの可能性を原因とする，正当な分散システム構築の困難さに対処すべく，Microsoftリサーチチームでは，この種のシステムの自動検証を行う方法論としてIronFleetを開発した。分散型プロトコルの定義や検証といったレベルを超越して，IronFleetでは，分散システムの実装が中央集中型の仕様要求を充足し，“競合条件，大域不変条件の違反，整数値オーバーフロー，パケットの符号化と複合化に関する不一致，障害復旧のように通常実行されないコードパスでのバグ”が存在しないことを“保証”する。目標は，分散システムが“正しく”，常に適切な動作を行うかどうかを判断することだ。
IronFleetは，分散システムの安全性すなわち実行されるアクションの正当性と，活性すなわちアクションの有用性の両方を立証する。論文によれば，IronFleetはこれを次のように実現している。
構造的および記述的証明を行う方法論と，同種のシステム実装に有用な検証済みの汎用ライブラリを併用することにより，複雑な分散システムを包括的に検証します。構造的な面では，同一の自動定理証明フレームワーク内で２つの検証方式を併用することにより，両者のセマンティックギャップを回避しつつ，並行的な封じ込め戦略(containment strategy)を実施します。複雑性を除外したプロトコルレベルの並列性の論証にTLA方式のステートマシンの改良版[TLA - Temporal Logic of Actions]を，並列性を除外した複雑性の論証にFloyd-Hoare方式の不可欠性検証(imperative verification)を，それぞれ採用しています。また，並列性論証を単純化する目的で，マシンチェックによる複雑性縮小の実装を必須としています。そして最後に，常時有効なアクションを使ってプロトコルを構成することにより，活性の証明の大幅な簡略化を図っています。
対象とするシステムは，プログラムの機能的な正しさを判断するための言語およびプログラム検証ツールであるDafnyで記述する。検証後のコードは，.NETあるいはWindowsへの依存性を排除するために，C#あるいはアセンブリコードにコンパイル可能だ。C++など他の言語のコードにコンパイルするようにDafnyを拡張する方法も考えられる。
IronFleetは，分散型PaxosステートマシンのIronRSLと，共有型キーバリューストアであるIronKVの正当性を論証するために使用されている。IronFleetと論証対象システムのソースコードはGitHubで入手可能だ。
この記事に星をつける
- エディタータブ
- チーフエディタータブ
送信
送信
コミュニティコメント