Centralization と ClassLoader

Centralization とは, 複数プロセスが協調して動くアプリケーションをモデル検査にかけたいときに, それぞれのプロセスを1スレッドとして1つのアプリケーションに押しこむことで, 検証可能にする技法のこと. 当然ながら内部実装が見えているときに限る.

例えば, Java PathFinder は Java のプログラムを直接検証できるモデル検証器であるが, その実態は Java VM のハックなので, 複数の VM にまたがってしまっていたらどうしようもない.

さて, 実際に Java PathFinder で centralization をするにはどうすればいいか. ほとんどは単純にスレッドを立てればいいが, static フィールドだけは, 共通になるとまずいので問題が生じることがよく知られているらしい. この辺 http://staff.aist.go.jp/c.artho/teaching/smc/todai-4.pdf にも書いてある. 解決法は配列を作ってスレッドIDごとに別々にすればいいらしい.

最近知ったのだが, 別の ClassLoader を用意してそちらでロードするようにすれば JVM 上で別のクラスとして扱われるらしく, static フィールドも別になるそうだ. なので, こんな書き換えも別にいらなかったりするのでは, と, ふと思った. ただやってみてはいない.

そういえば, 元も子もないことを言うと, プログラムを自分で書き換えてしまったら Java のプログラムを直接検証できるという持ち味が完全に失われてはいまいか? と思う. 自動書き換えツールが必要では.