Discovery Sagaサイレントキーワード俯瞰

本研究の目的は検証付きコンパイラ(Verifying Compiler)をコンパイラ最適化に適用し、最適化の数理的な性質を明らかにし、適用の地平を拡大することにあった。検証付きコンパイラ(Verifying Compiler)は、もともとHoareの提唱したプログラムの正当性を併せて証明するコンパイラシステムとして21世紀の課題として提唱した概念である。本研究で目指すのは、コンパイラ最適化における上のような危機的状況に対応すべく最適化をその正しさの証明を込めて適用するコンパイラの構築であり、最適化検証つきコンパイラ(Optimization Verifying Compiler)と呼ぶべきものである。
本年度は特に、情報処理環境の急速な変化に対応し、Webを含む分散処理環境において「最適化」の知識がどのように抽出できるかの研究を行った。
具体的には、Folksonomyを対象にしてそこからプログラミングに有用なさまざまな概念を抽出することができた。抽出結果は直感的に正しいことを確認した。また分散環境における計算記述の形式化がセキュリティの記述と密接に関係することをあきらかにできた。具体的には、ワークフローの意味論の厳密な形式化をおこない、(形式化された)文書で表現する方法を提案した。
さらに、上と関係して具体的に最適性能のコードを探索するため、つまり「コンパイラ最適化を超えたパフォーマンスチューニング」について結果を得ることができた。具体的には数値計算に代表される性能を求める分野にプログラム変換の高階関数の理論を応用して、探索空間を広げることに成功した。

【研究分担者】
SATO Hiroyuki	The University of Tokyo	Information Technology Center	Associate Professor	(Kakenデータベース)