2007 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 | コンパイラ / 最適化 / 時相論理 / 検証 / SSA形式 |
|---|
| Research Abstract |
1.コンパイラにおける時相論理を用いた最適化器の生成と最適化器の検証の研究
(1)コンパイラにおける時相論理を用いた最適化器の生成の研究
この研究では,時相論理の一つである双方向CTLを用いて最適化器を記述し,そこからモデル検査により最適化器を生成した.従来研究として,Laceyら(2004)のようなCTLなどの論理を用いて最適化器を生成する研究もあるが,従来研究では,理論的な側面に重点が置かれており,Pascalのサブセットなど簡単な言語だけしか扱えない,扱える最適化の種類が非常に限られている,時相論理の記述から生成した最適化器の効率が悪く,最適化時間や最適化されたコードの実行時間などの定量的なデータが得られていない,など克服すべき課題が多かった.本研究ではこれらの問題を解決したシステムを作成した.
(2)コンパイラにおける手書きの最適化器の検証の研究
最適化された中間コードに対し,時相論理で記述した仕様が満たされているかどうかを検証する方法を実現した.これは,まず,既存の手書きの最適化器を用い,それにアスペクト指向プログラミングの手法を用いて中間表現を変更する部分にマークをつけるように修正する.一方,個々の最適化について,中間コードが満たすべき仕様を時相論理で記述しておく.各フェーズの最適化後にその仕様が満たされているかどうかをモデル検査により検証する.これにより,最適化のバグを見つけることができた.
2.配列に対するSSA形式最適化の新しい方式の実装
配列をSSA形式で扱う方法は長らく研究されていたが,実用性にはほど遠かった.本研究では,RusらのFortran向けの手法をC言語向けに改良し,実装して実験を行った.結果はベンチマークにより異なるが,配列の最適化の結果,目的コードの実行時間が最大10%速くなる例もあった.
|
