並列索引構造の形式検証

並列データ構造の検証作業にとりかかった。具体的には、証明士を雇用した上で、並列データ構造の一つである並列キューについて、証明検査器Coqの中にモデルを作った。すなわち、証明検査器Coqに解釈できる形式で共有メモリによる仮想並列計算機を実装し、この並列仮想計算機で実装できる並列キューを実装し、さらにこの並列キューが直列可能性という性質を持っていることを証明するために必要な補題を洗い出した。これは、並列キューが正しい理由についての人間の直観を、機械に読める形式に書き写したことに相当する。実は、直列可能性を主張するために、並列ではない版のキューも実装して、並列版と並列ではない版のキューの動作を比較した。また、並列データ構造の使い道の一つのデータベースを検証する際にもっとも重視するべきなのは、ソフトウェアの中でも悪意ある外部からの攻撃にさらされる入力解釈の部分であるので、検証つき可逆読み書き器用の証明ライブラリを作成した。可逆読み書き器は、書いて読むと元に戻るという性質がある、文字列の書き出し器と読み込み器の組である。例として関係データベースの問い合わせ言語であるSQLの一部について、可逆読み書き器を作成し検証した。他に、部分構造論理の一つであるアーベル論理を並列計算に応用するという、2013年3月にPLACESというワークショップで発表した内容についてのpost-proceedingの原稿を書き、再度の査読を受け、掲載された。

並列データ構造の検証作業にとりかかった。具体的には、証明士を雇用した上で、並列データ構造の一つである並列キューについて、証明検査器Coqの中にモデルを作った。すなわち、証明検査器Coqに解釈できる形式で共有メモリによる仮想並列計算機を実装し、この並列仮想計算機で実装できる並列キューを実装し、さらにこの並列キューが直列可能性という性質を持っていることを証明するために必要な補題を洗い出した。これは、並列キューが正しい理由についての人間の直観を、機械に読める形式に書き写したことに相当する。実は、直列可能性を主張するために、並列ではない版のキューも実装して、並列版と並列ではない版のキューの動作を比較した。また、並列データ構造の使い道の一つのデータベースを検証する際にもっとも重視するべきなのは、ソフトウェアの中でも悪意ある外部からの攻撃にさらされる入力解釈の部分であるので、検証つき可逆読み書き器用の証明ライブラリを作成した。可逆読み書き器は、書いて読むと元に戻るという性質がある、文字列の書き出し器と読み込み器の組である。例として関係データベースの問い合わせ言語であるSQLの一部について、可逆読み書き器を作成し検証した。他に、部分構造論理の一つであるアーベル論理を並列計算に応用するという、2013年3月にPLACESというワークショップで発表した内容についてのpost-proceedingの原稿を書き、再度の査読を受け、掲載された。