2009 Fiscal Year Annual Research Report
型理論と線形計画法によるマルチスレッドプログラムの安全性検証
| Project/Area Number |
20700019
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
寺内 多智弘 Tohoku University, 大学院・情報科学研究科, 助教 (70447150)
|
|---|
| Keywords | ソフトウェア検証 / 型理論 / 型推論 / 線形計画法 / 権限計算 |
|---|
| Research Abstract |
本研究は、線形計画法と型理論を応用した、並行ソフトウェアの安全性(例えば、レースが起こらないなど)を検証する研究である。具体的には「分数権限計算」(Fractional Capability Calculus)という新しい概念を含んだ型システムを構築し、型推論問題を線形計画問題に帰着することにより高速に自動ソフトウェア検証を行う。
本年度は、以下の成果が得られた。
1.多相型による文脈依存な分数権限計算システム
従来の分数権限計算は文脈非依存であるため、異なる文脈で同じ関数が呼び出されるプログラムを正確に検証できない場合があった。我々は、parametric polymorphismという多相型の理論を分散権限計算に導入し、文脈依存であり、かつ多項式時間で推論可能なシステムを構築した。
2依存型の推論
従来の分数権限計算は通常の型システムと同じくプログラムの値に対して非依存なので、例えば、次のようなプログラムをレースがないと正しく検証できない:if(b){x++} || if(b){x++}(P||QはPとQが並列に動くプログラムを表す。)ブール値bに依存する分岐を判別できないためである。これを解決する手段として「依存型」(dependent types)という値に依存する型の概念があるが、自動的に推論するのは困難であった。我々は、モデル検査の研究で広められた、「反例を用いた自動抽象洗練化」(counter example-guided abstraction refinement)の理念に基づいた、自動的に、かつ効率よく依存型を推論する技術を開発した。
|
Research Products
(3 results)
