並行プログラム検証のための型システムとそのオペレーティングシステムの検証への応用

本年度の成果は1.デッドロック検証のための型システム、2.メモリ解放の正しさを検証するための型システムの二つである。1については、博士論文の成果であるデッドロック検証の型システムを整理し、論文として発表した。本型システムはロックへの破壊的代入が可能な参照と、入れ子構造でないロック獲得/解放プリミティブが扱える点で新規性がある。多くのプログラムがこの二つのプリミティブを用いて記述されているので、本研究はそれらのプログラムのデッドロック検証を扱う手法を提案した点で重要である。本型システムにおいては、ロックを解放する「義務」を線形型で、ロックの獲得順序を「ロックレベル」で、ロックへの参照へのアクセスを「分数権限」で管理することで、デッドロックが起こらないことを保証している。2に関しては、C言語のようにメモリ管理を手動で行う必要があるようなプログラミング言語に対して、正しくメモリ管理が行われていることを保証するための型システムを提案した。具体的には、獲得されたメモリがちょうど一度解放されることと、解放後にメモリへのアクセスがないことを、分数権限を用いて保証している。手動メモリ管理に伴うバグは、実用プログラムにおいても実際に数多くの障害をもたらしており、メモリ管理の正しさを保証することは、ソフトウェアの安全性向上において非常に重要である。なお、本研究については、実際に検証器を実装し、プログラムがある程度大きくなっても検証が現実的な時間で終了することを確認した。

本年度の成果は1.デッドロック検証のための型システム、2.メモリ解放の正しさを検証するための型システムの二つである。1については、博士論文の成果であるデッドロック検証の型システムを整理し、論文として発表した。本型システムはロックへの破壊的代入が可能な参照と、入れ子構造でないロック獲得/解放プリミティブが扱える点で新規性がある。多くのプログラムがこの二つのプリミティブを用いて記述されているので、本研究はそれらのプログラムのデッドロック検証を扱う手法を提案した点で重要である。本型システムにおいては、ロックを解放する「義務」を線形型で、ロックの獲得順序を「ロックレベル」で、ロックへの参照へのアクセスを「分数権限」で管理することで、デッドロックが起こらないことを保証している。2に関しては、C言語のようにメモリ管理を手動で行う必要があるようなプログラミング言語に対して、正しくメモリ管理が行われていることを保証するための型システムを提案した。具体的には、獲得されたメモリがちょうど一度解放されることと、解放後にメモリへのアクセスがないことを、分数権限を用いて保証している。手動メモリ管理に伴うバグは、実用プログラムにおいても実際に数多くの障害をもたらしており、メモリ管理の正しさを保証することは、ソフトウェアの安全性向上において非常に重要である。なお、本研究については、実際に検証器を実装し、プログラムがある程度大きくなっても検証が現実的な時間で終了することを確認した。