並行プログラムのための型理論に基づく利便性の高い静的検証手法

本年度は共有メモリ型並行プログラムに対して、メモリ、ロック、スレッド等のリソースが回収されずにプログラムが終了することはないという性質を検証するための手法を設計した。具体的には(1)並行プログラムの静的検証手法の理論的基盤の構築(2)検証アルゴリズムの定義(3)検証アルゴリズムの実装を行った。(1)については共有メモリ型並行プログラムをモデル化する手続き型言語の構文と意味論を定義した。その上で、この言語で記述されたプログラムに対する型システムを定義し、その健全性(プログラムが型付け可能であれば、いかなるスケジューリングや実行経路においてもリソースは必ず回収される)を証明した。このステップは先行研究(末永・小林 APLAS 2008)において提案した、ポインタ型を所有権によって拡張し、その所有権によってポインタの指す先のメモリへのアクセス権限と、そのメモリを解放する義務を表現した型システムをベースとして、その拡張を行った。本研究では、先行研究の型システムをロック型とスレッド型で拡張し、メモリと同様にロックとスレッドが正しく解放されることを保証している。ロックによる同期を介して所有権を受け渡すことができるように、ロック型には獲得可能型環境が付加される。プログラムは、ロックの生成、アンロック操作を行なう際には獲得可能型環境に記述された所有権を自らが保有する所有権からロックに付託し、ロックの獲得、回収を行なう際には獲得可能型環境に記述された所有権を自らのものとする。これにより、ロックを介したスレッド間の所有権の受け渡しを一貫して行なうことが可能となっている。スレッド型についても同様に、スレッドが終了した際に保有している所有権を獲得可能型環境として付加している。この型システムについて健全性を証明した。(2)については、受入研究者及び受入研究室の学生と共同で自動的にプログラムが型付け可能かどうかを判定する検証アルゴリズムを設計した。この型システムを用いた自動検証において困難な点は、適切な獲得可能型環境をいかに推論するかである。このために、検証を(1)獲得可能型環境の定義域の推論(2)型に関する制約の所有権制約への還元(3)所有権制約の解消の3ステップに分けた。1つ目のステップにおいては、獲得可能型環境を表す変数を制約言語に導入し、その定義域に関する集合の包含関係の制約を生成した上で、その制約を不動点反復アルゴリズムによって解消する。2つ目のステップにおいては、1つ目のステップにおいて得られた情報を元にして型環境変数を具体化し、型環境に関する制約を型に関する制約に還元した上で、その制約をさらに所有権変数に関する制約に還元する。3つ目のステップにおいては、所有権変数に関する制約を既存の制約ソルバーに入力として与え、充足可能性を判定する。これにより、初めに入力として与えられたプログラムが型付け可能であるかどうかが可能となる。(3)については、前項に述べたアルゴリズムの実装と実験を受入研究室の学生が主体となって行った。これにより、前項のアルゴリズムの動作を確認した。

本年度は共有メモリ型並行プログラムに対して、メモリ、ロック、スレッド等のリソースが回収されずにプログラムが終了することはないという性質を検証するための手法を設計した。具体的には(1)並行プログラムの静的検証手法の理論的基盤の構築(2)検証アルゴリズムの定義(3)検証アルゴリズムの実装を行った。(1)については共有メモリ型並行プログラムをモデル化する手続き型言語の構文と意味論を定義した。その上で、この言語で記述されたプログラムに対する型システムを定義し、その健全性(プログラムが型付け可能であれば、いかなるスケジューリングや実行経路においてもリソースは必ず回収される)を証明した。このステップは先行研究(末永・小林 APLAS 2008)において提案した、ポインタ型を所有権によって拡張し、その所有権によってポインタの指す先のメモリへのアクセス権限と、そのメモリを解放する義務を表現した型システムをベースとして、その拡張を行った。本研究では、先行研究の型システムをロック型とスレッド型で拡張し、メモリと同様にロックとスレッドが正しく解放されることを保証している。ロックによる同期を介して所有権を受け渡すことができるように、ロック型には獲得可能型環境が付加される。プログラムは、ロックの生成、アンロック操作を行なう際には獲得可能型環境に記述された所有権を自らが保有する所有権からロックに付託し、ロックの獲得、回収を行なう際には獲得可能型環境に記述された所有権を自らのものとする。これにより、ロックを介したスレッド間の所有権の受け渡しを一貫して行なうことが可能となっている。スレッド型についても同様に、スレッドが終了した際に保有している所有権を獲得可能型環境として付加している。この型システムについて健全性を証明した。(2)については、受入研究者及び受入研究室の学生と共同で自動的にプログラムが型付け可能かどうかを判定する検証アルゴリズムを設計した。この型システムを用いた自動検証において困難な点は、適切な獲得可能型環境をいかに推論するかである。このために、検証を(1)獲得可能型環境の定義域の推論(2)型に関する制約の所有権制約への還元(3)所有権制約の解消の3ステップに分けた。1つ目のステップにおいては、獲得可能型環境を表す変数を制約言語に導入し、その定義域に関する集合の包含関係の制約を生成した上で、その制約を不動点反復アルゴリズムによって解消する。2つ目のステップにおいては、1つ目のステップにおいて得られた情報を元にして型環境変数を具体化し、型環境に関する制約を型に関する制約に還元した上で、その制約をさらに所有権変数に関する制約に還元する。3つ目のステップにおいては、所有権変数に関する制約を既存の制約ソルバーに入力として与え、充足可能性を判定する。これにより、初めに入力として与えられたプログラムが型付け可能であるかどうかが可能となる。(3)については、前項に述べたアルゴリズムの実装と実験を受入研究室の学生が主体となって行った。これにより、前項のアルゴリズムの動作を確認した。