先進的型システムに基づく並列プログラミング言語のデバッガ及びメモリ管理の研究

1998 Fiscal Year Annual Research Report

• Project/Area Number: 09780245
• Research Institution: The University of Tokyo
• Principal Investigator: 小林 直樹 東京大学, 大学院・理学系研究科, 講師 (00262155)
• Keywords: 型システム / 線形型 / メモリ管理 / リージョン推論 / 並行プログラミング言語 / デッドロック

Research Abstract

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

Research Products

• [Publications] Naoki Kobayashi: "Quasi-Linear Types" Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages(POPL'99). 29-42 (1999)
• [Publications] Eijiro Sumii and Naoki Kobayashi: "A Generalized Deadlock-free Process Calculus" Proceedings of Workshop on High-Level Concurrent Language(HLCL'98),Electronic Notes on Theoretical Computer Science,Elsvier publishers. 16-3. 55-77 (1998)
• [Publications] Hideki Kariya and Naoki Kobayashi: "リージョン推論に基づくメモリ管理の下でのガーベジコレクション" 日本ソフトウェア科学会全国大会論文集. 337-340 (1998)
• [Publications] Naoki Kobayashi: "Quasi-Linear Types" Technical Report TR98-02,Dept.of Info.Sci.,Univ.of Tokyo. 1-41 (1998)