J_Java_PathFinder

ドキュメント(単なる本家の全訳です)

しかし、この元のドキュメントめっちゃわかりにくいなあ。訳もひどいがそもそもの文章があまりにわかりにくい。あまり国語(書いた人にとっては英語か)を学んでないと見た。文章が構造化されておらず、話がとびまくり。内容の説明とその内容の実現方式がどう難しかったが、ごっちゃに書かれている。ちゃんと書け。

Java PathFinder?(JPF)とは？

以前は，「JPFはJavaのバイトコードに対するな明示的状態ソフトウェアモデルチェッカ*1」と答えていた．しかし，現在，JPFは，まるでアーミーナイフのように，あらゆる種類の実行環境の検証が可能なソフトウェアであるといえる．あなたが形式手法を良く知らないのなら，JPFは以下の処理をするものであると考えるとよい．JPFは，対象のプログラムを一度(通常のVMはもちろん一度だけしか実行しません)だけでなく，理論的に可能なすべての入力によって実行を繰り返すことにより，実行経路上で潜在的に生じえるデッドロックや補足されない例外のような違反がないかどうかをチェックする．もし，このような違反を発見した場合，JPFは，どのような実行によってこの違反に達したのかという，実行経路を示す．またJPFは，問題にたどり着くすべての実行ステップにおける情報を保持しており、この点で，JPFは通常のデバガと異なる．

JPFは，何をチェックできるのだろうか？

JPFはどのような種類の不具合を見つけることができるのであろうか？JPFをただインストールしただけの状態でも，JPFはデッドロックと補足されない例外(たとえば NullPointerExceptions?やAssertionErrors?)を発見することができる．さらに，あなたが自分自身でプロパティクラスやリスナエクステンションを実装すれば，他の特性(たとえば，リソースの競合など)のチェックもできるようになるのである．では，JPFが対象にできるプログラムはどのようなものであろうか？ JPFのVMは，プラットフォーム依存のネイティブコードを実行することはできない．よって，一般論で言えば，JPFはネイティブメソッドの呼び出しをしないJavaプログラムのみを対象にすることができる．この制約は，テスト対象のアプリケーションにおいて，どのような標準ライブラリを利用することができるかに関しての制約となる．ネイティブコードを呼び出すライブラリを利用できるようにするために，JPDは，Model Java Interface(MJI)を用意している．しかし，現時点ではjava.awtやjava.netは対応しておらず，java.ioの一部に対応しているのみである．もう一つの制約として，アプリケーションの大きさがある．JPDが実行状態を保持するため，なんら状態の抽象化をしない場合，おおよそ～10kloc程度(もちろんコードの中身によるが)のアプリケーションでないと効率的にチェックができない．標準ライブラリの利用制限とプログラムコードの大きさの制限から，JPFは，主に完全な手続き的プログラムで記述されたモデルであるようなアプリケーションに利用されている．JPFは，特にJavaプログラムのコンカレンシーの検証に利用される．つまり，スケジュールされた連続処理の網羅的な探査のために使われる．

モデル検証とテスト

なぜJPFは普通のテストでは不可能なことができるのであろうか？それは、JPFが「非決定性」を扱うことができるからである。一方、テストドライバーは、たとえば、処理の実行順序などの非決定性を制御できない。というのも、その制御は、実行環境(VM)が制御するからである。また、ランダムな入力データのような非決定性も、提供するAPIを用いたユーザの実装によって簡単に実現可能である。非決定性をシミュレートすることは単にすべての非決定的な選択をシステマティックに実現するだけではない。バックトラッキングと状態の一致判定が可能になるということである。

バックトラッキングとは、JPFが実行状態の履歴を保持し、まだ実行していない処理が残っていないかを判断することである。たとえば、JPFがプログラムの終了状態に達したとする。その場合、JPFは、履歴を元に実行状態を「後戻り」することにより、まだ実行していない実行順序の処理発見することができる。このような処理は、理論的には、単にプログラムを開始状態から再実行するという機構で実現できるが、バックトラッキングは、状態を上手に保持していえば、はるかに効果的な機構である。
状態の一致判定とは、無駄な処理をしないためのもう一つの工夫である。プログラムの実行状態は、主にヒープとスレッドスタックのスナップショットで構成される。JPFが動作している間、JPFは、新しい実行状態ごとに、過去に同じ状態がなかったかどうかをチェックする。そして、同じ状態が存在した場合、現在の実行経路による処理を続けることが無駄であるので、JPFは最も近い実行していない非決定的選択までバックトラックする。

理論的に、明示的状態モデル検証はきわめて厳密なやり方である。なぜならすべての選択を探索するからであり、ソフトウェアに何らかの問題があれば必ず発見できる。残念ながら、ソフトウェアのモデル検証は、この厳密性のために10kloc程度の小さなプログラムに対してのみ適応が可能である。なぜなら、複雑なプログラムになると、状態数はコンピュータが計算できる限界を上回ってしまうからである。この問題は状態爆発として知られており、原子的な処理から構成される複数のプロセスがどのような実行順序をとりうるかを考えるとわかりやすい。

状態爆発の例:

JPFは状態爆発に起因するスケーラビリティの問題を3つの方法で解決している。一つ目は検索戦略を選択できるようにしていること、二つ目は、状態数の削減、3つ目は状態保持のための必要なメモリ量の削減である。

探索戦略が選択可能であることは、すべての状態を検索することができないという問題を、問題を早く見つけるように検索を方向付けることによって解決しようという考え方である。この考え方は、モデルチェッカーを証明のためでなく、デバッグのために用いるということを前提にしている。方法としては、注目する特性に関係のある状態に達する可能性を考慮した順序や選択で探索をヒューリスティックに実行することによる。このヒューリスティック性の処理は、JPFのコアプログラムにハードコーディングされておらずプラグイン形式のクラスとして実装されている。
蓄積すべき状態数の削減とは、スケーラビリティを改良する方法としてよくやるやり方であり、ＪＰＦでは、多くの方式を利用している。
- ヒューリスティックな選択生成は、状態によっては、非決定的な選択をすべて試行する必要がない場合があることを利用している。閾値によって振る舞いが変化するような非決定的なfloatの入力を考えてみよう。float型では、すべての可能な値を試行するのは不可能である*2。しかし、システムの振る舞いをチェックすることに関して言うなら、閾値より小さい値か、閾値か、閾値より大きい値かの3種類を試すだけで十分かもしれない。このようなヒューリスティックな処理は、特定のアプリケーションの要求に対応するために簡単に拡張できると良い。
- 半順序の関係を利用した削減は、コンカレントなプログラムにおいて状態空間を削減するためにもっとも有効な方式である。この方式では、異なるスレッドの動作に影響を与える命令のコンテキストスイッチのみを考えるというものである。たとえば、異なるスレッドからアクセスが可能なオブジェクトに対するPUTFIELDインストラクション*3などが相当する。この方式をユーザの実装に頼らず自動的に実現することは難しいが、JPFの半順序関係の削減は、Javaのバイトコードを利用しており、ガベージコレクタを用いて実現している。
- ホストVMの使用。 JPFは、Javaで実装されたJVMの一種である。つまり、JPFはホストとなるJVM上で動作していることになります。注目する特性に関係のないプログラム部分に対しては、状態をすべて追跡するJPFで実行するのではなく、状態を保持しないホストとなるJVMに処理させたほうが良い。Model Java Interface(MJI)は、IOのシミュレートや他の標準ライブラリの機能を扱うため、特にホストJVMの利用が適している。
- 状態の抽象化。デフォルトの動作として、JPFはすべてのヒープ、スタック、スレッドの変化を保持している。しかし、このことは、二つの実行状態が、ある種のアプリケーションの観点から見て異なるかどうかを決定するだけのためなら時として大きなオーバヘッドをである。たとえば、データ構造をその形によってのみ分析することにより状態一致を判定すれば、状態を削減することができる。この方式が、JPFで利用されている。

拡張性

今まで示したJPFの特徴からわかるように、JPFはもはやクラシカルなモデル検証ではないことは明らかである。JPFを動的でランタイム指向の検証目的として実行システムのフレームワークとして考える人もいるであろう。JPFは、ある種のアプリケーションやある種の特性に特化して採用することにより、ソフトウェアモデル検証のシステマティックなスケーラビリティの問題を克服しようとしている。であるから、将来的な開発を駆動する設計方針は拡張性である。ここでは、二つの拡張の機構を示す。一つ目は検索/VMLリスナ、二つ目はModel Java Interface(MJI)である。

検索/VMLリスナは、JPFの内部状態モデルを拡張し、より複雑な特質をチェックことを可能とし、直接的な検索を行ったり、単に実行状態の統計情報を収集するために便利な方式を与える。この方式は、リスナにバイトコードのインストラクションの実行やフォワード/バックトラックの進行のような、JPF内部のイベントに対してサブスクライブさせるようなイベントオブザーバパターンによって実現される。

リンク

JavaPathfinder 本家