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