2009 Fiscal Year Annual Research Report
時相論理を用いたコンパイラ最適化器の生成・検証と別名を扱えるSSA形式高度最適化
| Project/Area Number |
19300006
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
佐々 政孝 Tokyo Institute of Technology, 大学院・情報理工学研究科, 教授 (20016182)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
滝本 宗宏 東京理科大学, 理工学部, 講師 (00318205)
|
|---|
| Keywords | コンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 |
|---|
| Research Abstract |
1. 時相論理を用いたコンパイラ最適化器の検証
コンパイラの最適化器が正しいかどうかを,時相論理を用いて検証する方法を開発,実装した.これは,最適化前と最適化後のSSA形式中間コードを比較する.最適化前の中間コードを基にして,比較結果が異なっている場合には,ラベルに「追加」,「削除」,「置換」等8種類の情報を追加する.「追加」,「削除」,「置換」等が満たすべき仕様を時相論理の一種であるCTL論理によってあらかじめ記述しておき,これを用いてモデル検査を行う.モデル検査の結果,バグがあれば報告される.この手法の大きな特長は,既存の手書きの最適化器に適用できること,検証者が最適化アルゴリズムやその実装を知る必要がないこと,である.これにより,コンパイラ・インフラストラクチャCOINSの最適化のバグをいくつか発見することができた.
2. 質問伝播に基づく投機的部分冗長除去
プログラムの実行経路によって実行されない式を除去する部分冗長除去を,要求駆動の性質を用いて,ループ不変式のループ外移動を投機的に行えるように拡張した.本手法を適用することによって,他の解析やプログラム変形を行うことなく,任意のプログラム構造に対して,ループ内の実行コストをさらに低減できることを,実験の結果から明らかにした.
|
Research Products
(5 results)
