2008 Fiscal Year Annual Research Report
型理論と線形計画法によるマルチスレッドプログラムの安全性検証
| Project/Area Number |
20700019
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
寺内 多智弘 Tohoku University, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | ソフトウェア検証 / 型理論 / 型推論 / 線形計画法 / 権限計算 |
|---|
| Research Abstract |
本研究は、線形計画法と型理論を応用した並行ソフトウェアの安全性を検証する研究である。具体的には「分数権限計算」(Fractional Capaility Calculs)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。本年度は、以下の成果が得られた。
1. バッファ使用量の検証
MPIプログラムなど、プロセス同士がメッセージパッシングで通信・同期をとる並行プログラムでメッセージがバッファされる場合、バッファが限度サイズ以上使用されると、バッファオーバーフローが起きたり例外が発生するなどの問題がある。このようなソフトウェアに対し、型推論と線形計画法を用いてバッファの使用量上限を求めるという多項式時間のアルゴリズムを開発した。
2. レースコンディンションの防止
マルチスレッドプログラムにおいて、異なるスレッドが共有変数を同時にアクセスし、少なくとも一方がその変数に書き込んでいる状態をレースコンディンションと呼ぶ。我々は、型推論と線形計画法を用い、プログラム実行時にレースが起こらないか検証する多項式時間のレース検証アルゴリズムを開発した。従来のレース検証アルゴリズムに比べ、セマフォやシグナルなどロック以外の同期プリミティブにも対応するなど、性能の向上に成功した。
3. Observation Determinismの検証
機密情報を含んだ並行ソフトウェアにおいて、スレッドのスケジューリングから外部に機密情報が漏洩してしまう場合がある。機密情報が漏洩しないことを保障する十分条件の一つに、Observational Determinismという概念がある。Observation Detarminismは、外部から見える実行結果が機密情報にもスレッドのスケジューリングにも依存しないという性質である。我々は、型推論と線形計画法を応用することによってメッセージパッシングなどを含んだ幅広い並行ソフトウェアのObservational Determinismを効率的に(多項式時間で)検証することに成功した。
|
