【研究分野】情報学基礎

【研究領域課題番号】23220001 (KAKENデータベースで見る）

【研究キーワード】

高階モデル検査 / プログラム検証 / データ圧縮 / 高階文法 / 型システム / 関数型プログラム / 関数型言語 / 高階再帰スキーム / 型理論

【研究成果の概要】

本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。

【研究種目】基盤研究(S)

【研究期間】2011-05-31 - 2016-03-31

【配分額】137,540千円 (直接経費: 105,800千円、間接経費: 31,740千円)

【研究分野】情報学基礎

【研究領域課題番号】20240001 (KAKENデータベースで見る）

【研究キーワード】

ソフトウェア検証 / 型システム / 高階モデル検査 / 資源使用法検証 / プログラム解析 / 型理論 / 述語抽象化 / メモリ使用法解析 / モデル検査 / 高階再帰スキーム / 資源使用法解析 / ツリーオートマトン

【研究成果の概要】

本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.

【研究種目】基盤研究(A)

【研究期間】2008 - 2010

【配分額】49,270千円 (直接経費: 37,900千円、間接経費: 11,370千円)

【研究分野】ソフトウエア

【研究領域課題番号】17300003 (KAKENデータベースで見る）

【研究キーワード】

プログラム検証 / プログラム解析 / 型理論 / 関数型プログラム / 並行プログラム / 情報流解析 / 型システム / デッドロック / 資源使用法解析 / プログラム等価性 / 線形最適化問題 / 割り込み / 双模倣 / プログラム変換 / XML

【研究成果の概要】

本研究の目的は,ソフトウェアの信頼性向上のため,型理論などの数理科学的手法に基づいたプログラムの検証手法を発展させることにあった.特に,これまでの申請者らによる検証手法を改良・発展させ,現実のプログラムの検証を可能にすることに主眼をおいた.
3年間の主要な成果は以下のとおり.以下のいずれの研究においても実際にプログラム検証器のプロトタイプを作成し有効性を確認している.
1.関数型プログラムの検証手法
以前から,ファイルやメモリなどの計算資源を正しいプロトコルでアクセスするかどうかを検証するための資源使用法解析について研究を行っていたが,例外処理機構を扱っていないなど,実際のプログラミング言語とは開きがあった.そこで,従来の我々の検証手法を拡張し,例外処理機構に対応できるようにした.また,従来の型を用いた自動検証手法では,一般に解析精度が粗かったため,依存型の自動推論手法を考案することにより,精度のよい解析を自動で行えるようにした.
2.並行プログラムの検証手法
以前からπ計算を対象として,デッドロックなどの自動解析手法を研究していたが,実用化する上での解析精度,実際の言語が提供するプリミティブとの開きなどがあった.そこで,前者の問題をモデル検査などとの融合によって改善した.また,後者の問題に対処するため,ポインタや割り込みなどが入った言語に対する解析手法も考案した.
3.情報流解析
プログラムが機密情報を漏らさないかどうかを検証する情報流解析について研究を行った.従来から型を用いた情報流解析手法は提案されていたが精度が問題だったため,本研究ではモデル検査手法と融合させることにより,高速かつ精度のよい解析を可能にした.

【研究種目】基盤研究(B)

【研究期間】2005 - 2007

【配分額】12,160千円 (直接経費: 10,900千円、間接経費: 1,260千円)

【研究分野】計算機科学

【研究領域課題番号】13680397 (KAKENデータベースで見る）

【研究キーワード】

コンパイラ最適化 / ループアンローリング / 性能予測 / 型システム / 最適化の検証 / Optimization Verifying Compiler / Grid / 分散環境 / 性能の定量的解析 / データフロー方程式 / 型理論 / 形式的記述 / ループアンローミング / イディオム認識 / プログラミング言語環境 / 自動チューニング

【研究成果の概要】

本研究課題は「最適化を適応的に適用するコンパイラの研究」というタイトルのもと、3年計画で実施されたものである。本研究の申請時、すでに計算プラットフォームは単一プロセッサから分散環境にまで広いスペクトルを持っていた。実行側のプログラムはこの広い計算環境のスペクトルをカバーすることが求められている。したがってプログラミング言語を翻訳してプラットフォームごとに量適なコードを出力するコンパイラ、特にオブティマイザの負担は非常に重くなっている。しかし、これら計算環境では性能を決めるファクターがますます複雑化している。例えばデータアクセスに関して言えば単一プロセッサ/並列プロセッサ環境においてはキャッシュの振舞いは性能を決める大きなファクターになる。これは原理的に静的に解析可能であるもののその複雑さからごく荒い近似で満足せざるを得ない。また分散環境においては、原理的に静的に解析不可能なネットワークと計算ノードとのインタラクションの解析をしなければならず、これもしばしば現実と大きくずれる近似で満足せざるを得ない。このようにコンパイラの最適化においては、現在静的/動的ともに荒い近似モデルを使わざるを得ず、自然に最適化の議論は性能が向上するか否かを中心とした定性的なものにならざるを得なかった。しかしお互いに効果を殺し合うような最適化が多く提案されている現状を考えれば今後はより精度の高いモデルを構築して定量的な議論をすることが最適化の効果を高めるために必須である。
以上の問題意識をもって、本研究では1.性能に影響を与えるファクターを反映し、性能を精度良く近似できるモデルを研究すること、具体的に単一CPU環境におけるブロッキングの幅とアンローリングの段数の決定、分散環境における最適な通信パターンの動的決定を目標とした。2.さらにそれを数値計算ライブラリに適用してインストール時、実行時にそれぞれ最適性能を引出すようなソースの変形をふくむ最適化を行うことを目標とした。3.加えて、本研究の適用範囲を広げることも目標にした。
本研究の実施によって上の目標を達成する多くの成果をあげることができた。詳しくは成果リストを参照することにして、アンローリングに関して非常に精度のよい性能の理論モデルを得たこと、また数値計算ライブラリに関して多くの経験を得たことは特筆すべきである。また副成果として、GCCのアンローリングに関するバグを発見し、修正している。今日、コンパイラ最適化は(1)適用の正しさの証明と、(2)実際に性能があがることの証明を数理的に行うことを求められるようになってきている。ここ数年の間に急速に問題意識が立ち上がり、コンパイラ最適化のVerificationということばで多くの研究者を集めるまでになった。佐藤はこれにVerifying Compilerというキーワードを与えている。今後の展開として、本研究の成果を出発点としてVerifying Compilerの展開を予定している。

【研究種目】基盤研究(C)

【研究期間】2001 - 2003

【配分額】3,500千円 (直接経費: 3,500千円)