|
本研究では、プログラミング言語のデバッグのサポートやメモリ管理などのランタイムシステムをサポートするための静的型システム・プログラム解析の研究を行った。
デバッグのサポートに関しては、昨年度までに構築した並行プログラムのデッドロックフリーダムを保証する型システムを一般化し、その型チェッカを実装した。これにより、昨年度までよりもより広い範囲のプログラムのデッドロックフリーダムの保証を行なうことができ、並行プログラム中の、デッドロックを引き起こす可能性のある場所を静的にこれまで以上に絞り込むことができるようになった。
メモリ管理に関しては、「疑似線形型システム」および「リージョン推論によるメモリ管理とガーベジコレクション(GC)の融合」について研究を行なった。
「疑似線形型システム」は特定のデータがプログラム実行中に一回しかアクセスされないことを保証できる線形型システムを発展させ、より多くのデータについて静的情報に基づいて自動的にメモリ解放を行なえるように我々が考案した型システムである。本年度はその型システムの定式化および証明、それに基づくプログラム解析システムの実装・評価を行なった。実験結果から、プログラム中で動的に割り当てられるメモリのうち、大部分が本型システムに基づいて(GCなどの手法に頼らずに)自動的に解放できることが確認できた。
「リージョン推論によるメモリ管理とGCの融合」では、静的メモリ管理のもう一つの手法であるリージョン推論に基づくメモリ管理方式においてダングリングポインタが生じて通常のGCとの融合が因難であるとされてきた問題を、GC時に型情報を参照することによって解決する方法を定式化し、正当性の証明を行なった。
|
