2011 Fiscal Year Annual Research Report
分散チェックポインティングを用いたネットワークアプリケーションのモデル検査
| Project/Area Number |
23300004
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
山本 光晴 千葉大学, 大学院・理学研究科, 准教授 (00291295)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 大学院・情報理工学系研究科, 教授 (30156252)
アルト シリル 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (30462831)
田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任教授 (60443199)
|
|---|
| Keywords | モデル検査 / チェックポインティング |
|---|
| Research Abstract |
本年度の研究成果はDMTCPにおける通信接続の復元のプロトタイプ作成と、予備実験としてのサンプルアプリケーションによる評価に大別される。
分散チェックポインティング実装としては当初の予定通り、DMTCPを使用することにした。DMTCPでは、チェックポインティングの対象となるプロセスをcoordinatorと呼ばれるプログラムの制御下におくことによって、(場合によっては複数ノードで動作している)複数プロセスの保存・復元を可能にしている。これらのプロセスの問の通信接続も保存・復元される。しかし、DMTCPにおける通信接続の復元は、coordinatorの制御下にあるプロセス同士の間に限られる。一方で、検証対象のプロセスを実行するモデル検査器は、検証の際に探索済みのスケジューリング履歴などの大域的な情報を保持しなければならないため、保存・復元の対象プロセスではなく、よってcoordinatorの制御下にはない。従って、DMTCPをネットワークアプリケーションのモデル検査に応用するためには、coordinatorの制御下にあるプロセスとないプロセスとの間の通信接続の復元にも対応させなければならない。この問題を解決するため、我々はcoordinatorの制御下に新たにプロキシプロセスを導入した。モデル検査器のかわりにプロキシプロセスが通信相手との間の通信接続を確立し、UNIXドメインソケットを通じてソケットディスクリプタをモデル検査器に渡す。保存時に一時的にモデル検査器側のソケットは切断されるが、プロキシプロセスが同じソケットを保持しているため、復元時には通信接続も復元される、これを再度UNIXドメインソケット経由でモデル検査器に渡す。
実際にこのプロトタイプを用いて、JavaによるSecure Shell実装であるJSchに含まれるファイル転送プログラムScpToを検証し、スレッドが適切に同期されていないことによる競合条件を発見することに成功した。また、バグを修正したScpToで検証が成功することも確認した。
研究協力者:レオンワタナキット・ワチャリン(東京大学→千葉犬学)
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
交付申請書に平成23年度実施計画として記載したDMTCPにおける通信接続の復元のプロトタイプ作成が予定通り達成できているため。
|
| Strategy for Future Research Activity |
国内外の関連する分野、特に実行時検証の分野の研究者との連携や、同じくJavaを使用するが、仮想計算機の差異などにより現状ではJava PathFinderを直接は利用できないAndroidアプリケーションへの応用の可能性を含め、企業との連携も視野に入れる。また、関連する科研費課題「クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法」との連携のため、UDPへの対応を行う。
研究計画の変更や研究を遂行する上での問題点は特段無い。
|
