| Project/Area Number |
11J00571
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
末永 幸平 京都大学, 情報学研究科, 日本学術振興会特別研究員(PD)
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2011: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | プログラム検証 / 並行プログラム / 型システム / メモリリーク / 型推論 / 形式手法 / 自動検証 / プログラム解析 |
|---|
| Research Abstract |
本年度は共有メモリ型並行プログラムに対して、メモリ、ロック、スレッド等のリソースが回収されずにプログラムが終了することはないという性質を検証するための手法を設計した。具体的には(1)並行プログラムの静的検証手法の理論的基盤の構築(2)検証アルゴリズムの定義(3)検証アルゴリズムの実装を行った。(1)については共有メモリ型並行プログラムをモデル化する手続き型言語の構文と意味論を定義した。その上で、この言語で記述されたプログラムに対する型システムを定義し、その健全性(プログラムが型付け可能であれば、いかなるスケジューリングや実行経路においてもリソースは必ず回収される)を証明した。このステップは先行研究(末永・小林 APLAS 2008)において提案した、ポインタ型を所有権によって拡張し、その所有権によってポインタの指す先のメモリへのアクセス権限と、そのメモリを解放する義務を表現した型システムをベースとして、その拡張を行った。本研究では、先行研究の型システムをロック型とスレッド型で拡張し、メモリと同様にロックとスレッドが正しく解放されることを保証している。ロックによる同期を介して所有権を受け渡すことができるように、ロック型には獲得可能型環境が付加される。プログラムは、ロックの生成、アンロック操作を行なう際には獲得可能型環境に記述された所有権を自らが保有する所有権からロックに付託し、ロックの獲得、回収を行なう際には獲得可能型環境に記述された所有権を自らのものとする。これにより、ロックを介したスレッド間の所有権の受け渡しを一貫して行なうことが可能となっている。スレッド型についても同様に、スレッドが終了した際に保有している所有権を獲得可能型環境として付加している。この型システムについて健全性を証明した。(2)については、受入研究者及び受入研究室の学生と共同で自動的にプログラムが型付け可能かどうかを判定する検証アルゴリズムを設計した。この型システムを用いた自動検証において困難な点は、適切な獲得可能型環境をいかに推論するかである。このために、検証を(1)獲得可能型環境の定義域の推論(2)型に関する制約の所有権制約への還元(3)所有権制約の解消の3ステップに分けた。1つ目のステップにおいては、獲得可能型環境を表す変数を制約言語に導入し、その定義域に関する集合の包含関係の制約を生成した上で、その制約を不動点反復アルゴリズムによって解消する。2つ目のステップにおいては、1つ目のステップにおいて得られた情報を元にして型環境変数を具体化し、型環境に関する制約を型に関する制約に還元した上で、その制約をさらに所有権変数に関する制約に還元する。3つ目のステップにおいては、所有権変数に関する制約を既存の制約ソルバーに入力として与え、充足可能性を判定する。これにより、初めに入力として与えられたプログラムが型付け可能であるかどうかが可能となる。(3)については、前項に述べたアルゴリズムの実装と実験を受入研究室の学生が主体となって行った。これにより、前項のアルゴリズムの動作を確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の予定通り、並行プログラムのためのリソースリーク解析のための型システムの形式化を完了させ、型推論アルゴリズムを定義し、その実装までを得ることができた。また、ここまでの成果を論文としてまとめて提出したところである。
|
| Strategy for Future Research Activity |
今年度は本研究の着想の妥当性を確認するために問題設定においていくつかの単純化を行なっている。具体的には(1)ロックやスレッドをメモリ内に格納し、そのポインタを受け渡すことはない(2)構造体が存在しない等である。単純化によって今年度研究範囲から外した内容を扱えるようにすることは今後の重要な課題である。また、今回の実装はC言語をモデル化したより容易な言語を対象しているため、Cプログラムを直接扱える検証器を実装し、より大きなプログラムを用いて実験することも重要な課題である。
|
