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

コンパイラ / コード最適化 / 時相論理 / 静的単一代入形式 / 網羅型データフロー解析 / 要求駆動型データフロー解析 / キャッシュ効率化 / 大域値番号付け / 最適化 / COINS / スカラー置換 / 部分冗長性除去 / 部分無用コード除去 / キャッシュ最適化 / 時相論理理 / CTL

COINSコンパイラの低水準中間表現に対し,双方向時相論理であるCTL-FVを用いて最適化のパターンと変換を記述し,そこからモデル検査により,C言語の最適化器を生成した.一方,通常形式上の部分冗長除去(PRE)を静的単一代入形式上で行うように変換する汎用的な手法を開発した.また,PREおよびPREに似た部分無用コード除去法の効率化と効果の向上を行い,PREの応用として,同じ配列を参照するロード命令のキャッシュヒット率を向上させる手法を実現した.

コンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 / 無用コード / データフロー解析 / 部分無用コード除去 / 最適化 / SSA形式

時相論理を用いたコンパイラ最適化器の生成系を作成した.これにより,従来は実用にならないと思われていたものが手書きのものに近づいた.また,コンパイラの最適化器が正しいかどうかを,時相論理を用いて検証する方法を開発,実装した.これは,モデル検査によりバグを報告する.一方,プログラムの実行経路によって実行されない式を除去する部分冗長除去の最適化を,要求駆動の性質を用いて,ループ不変式のループ外移動を投機的に行えるように拡張した.本手法を実装し,評価した結果,従来法より効率的に高速なコードを生成できることを示した.

コンパイラ / 最適化 / 静的単一代入形式(SSA形式) / 検証 / モデル検査 / 時相論理

1.研究の背景
コンパイラの分野では,SSA形式(静的単一代入形式)などの新しい内部表現への対応,それを用いた最適化,書き下したコンパイラ部品の検証が切望されている.
2.SSA形式における逆変換の評価と最適化の新しい手法の開発
(i)SSA形式から通常形式への逆変換法は,Briggsらの方法とSreedharらの方法が知られている主な方法であるが,これまでそれらを比較した研究がなかった.我々は,この2つとBriggsらの方法の改良版を実装し,SPECベンチマークを用いた実験により比較し,Sreedharらの方法が現在の技術水準では実際上最良であることを示した.
(ii)SSA形式での最適化については種々提唱されているが,まだ不十分な点が多い.たとえば部分冗長除去やコード移動のアルゴリズムでは,SSA形式のφ関数を越えてのコードの移動が困難で,単純な例でも最適化できない例が知られている.本研究では,この問題点を解決し,値番号付けを含む部分冗長コード移動のアルゴリズムを開発,実装した.
3.コンパイラの最適化器の検証
(i)コンパイラの最適化器の検査法の一つとして,最適化前後で各変数の値をトレースとして出力し,その後にそれらを比較照合する,という方法により,各種最適化器の正しさを確認する方法を開発し,実装した.
(ii)時相論理による最適化の記述から自動的に最適化器を作成する研究を行った.実装上の工夫を行い,従来研究と比べ,最適化時間を実用的な時間内に収めることができたのが特長である.
(iii)既存の最適化器が満たすべき条件を時相論理により記述しておき,実際に最適化器を動かした後に,記述した条件が満たされているかどうかをモデル検査によりチェックする方法を開発し,実装,評価を行った.これにより,既存の手書きの最適化器の正しさを検証することができる.さらに未知のバグも発見できた.

【研究分担者】
滝本宗宏	東京理科大学	理工学部	准教授	(Kakenデータベース)

【研究分担者】
滝本宗宏	東京理科大学	理工学部	講師	(Kakenデータベース)

【研究分担者】
滝本宗宏	東京理科大学	理工学部	講師	(Kakenデータベース)