時相論理を用いたコンパイラ最適化器の生成・検証と別名を扱えるSSA形式高度最適化
【研究分野】ソフトウエア
【研究キーワード】
コンパイラ / 最適化器 / 検証 / 時相論理 / モデル検査 / 投機的部分冗長除去 / 無用コード / データフロー解析 / 部分無用コード除去 / 最適化 / SSA形式
【研究成果の概要】
時相論理を用いたコンパイラ最適化器の生成系を作成した.これにより,従来は実用にならないと思われていたものが手書きのものに近づいた.また,コンパイラの最適化器が正しいかどうかを,時相論理を用いて検証する方法を開発,実装した.これは,モデル検査によりバグを報告する.一方,プログラムの実行経路によって実行されない式を除去する部分冗長除去の最適化を,要求駆動の性質を用いて,ループ不変式のループ外移動を投機的に行えるように拡張した.本手法を実装し,評価した結果,従来法より効率的に高速なコードを生成できることを示した.
【研究代表者】
【研究分担者】 |
| 滝本 宗宏 | 東京理科大学 | 理工学部 | 講師 | (Kakenデータベース) |
|
【研究種目】基盤研究(B)
【研究期間】2007 - 2009
【配分額】18,850千円 (直接経費: 14,500千円、間接経費: 4,350千円)