| Project/Area Number |
09780245
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
小林 直樹 東京大学, 大学院・理学系研究科, 講師 (00262155)
|
|---|
| Project Period (FY) |
1997 – 1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1998: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1997: ¥1,500,000 (Direct Cost: ¥1,500,000)
|
|---|
| Keywords | 型システム / 線形型 / メモリ管理 / リージョン推論 / 並行プログラミング言語 / デッドロック / リ-ジョン推論 |
|---|
| Research Abstract |
本研究では、プログラミング言語のデバッグのサポートやメモリ管理などのランタイムシステムをサポートするための静的型システム・プログラム解析の研究を行った。
デバッグのサポートに関しては、昨年度までに構築した並行プログラムのデッドロックフリーダムを保証する型システムを一般化し、その型チェッカを実装した。これにより、昨年度までよりもより広い範囲のプログラムのデッドロックフリーダムの保証を行なうことができ、並行プログラム中の、デッドロックを引き起こす可能性のある場所を静的にこれまで以上に絞り込むことができるようになった。
メモリ管理に関しては、「疑似線形型システム」および「リージョン推論によるメモリ管理とガーベジコレクション(GC)の融合」について研究を行なった。
「疑似線形型システム」は特定のデータがプログラム実行中に一回しかアクセスされないことを保証できる線形型システムを発展させ、より多くのデータについて静的情報に基づいて自動的にメモリ解放を行なえるように我々が考案した型システムである。本年度はその型システムの定式化および証明、それに基づくプログラム解析システムの実装・評価を行なった。実験結果から、プログラム中で動的に割り当てられるメモリのうち、大部分が本型システムに基づいて(GCなどの手法に頼らずに)自動的に解放できることが確認できた。
「リージョン推論によるメモリ管理とGCの融合」では、静的メモリ管理のもう一つの手法であるリージョン推論に基づくメモリ管理方式においてダングリングポインタが生じて通常のGCとの融合が因難であるとされてきた問題を、GC時に型情報を参照することによって解決する方法を定式化し、正当性の証明を行なった。
|
