双方向CTLによるJava 最適化器の生成

情報処理学会 Web Site 参考文献24件

書誌事項

タイトル別名
  • ソウホウコウ CTL ニ ヨル Java サイテキカキ ノ セイセイ
  • Generating Java Compiler Optimizers Using Bi-directional CTL

この論文をさがす

抄録

近年，時相論理によるコンパイラ最適化器生成の研究が行われている．しかし，実際のプログラムを対象として最適化時間や目的コードの実行時間を提示した研究はない．本研究は従来研究の弱点を克服し，時相論理による記述からJava 言語の効率良い最適化器を生成するシステムを作成した．論理としては，分岐時相論理の1 つで過去時制と未来時制をともに扱える双方向CTL であるCTL-FV 9)を用いた．最適化変換を記す仕様記述も，従来法と異なり，条件式を満たす特定の番号の個々の命令文ではなく，命令文の集合を計算するようにしたので，複雑な最適化が容易に記述できるようになった．さらに，本研究は一時変数を記述できるようにするなど種々の実用化の工夫を行い，Java 言語に対する典型的なコンパイラ最適化器を実現した．本研究が実装したモデル検査器は何の変換も行わずに，過去時制と未来時制を直接扱えるため，十分な効率で動作する．従来，モデル検査器を用いた最適化器は実用的な時間では動作しないといわれていたが，実験により，本研究ではSPECjvm98 の7 つについて，4 秒～4 分で最適化が行えることを確認できた．また，通常の最適化器に近づいた性能を持った，CTL による最適化器の実装は本研究が初めてであるため，その可能性と問題点を明らかにした．生成される最適化器の処理時間を短くするための工夫や，記述のノウハウなど，本手法の改善に向けた種々の考察を加えた．

There have been several research works that analyze and optimize programs using temporal logic. However, no evaluation of optimization time or execution time of these implementations has been done for any real programming language. In this paper, we present a system that generates a Java optimizer from specifications in a kind of bidirectional temporal logic CTL-FV 9). We also present a new specification language based on the bidirectional CTL that can express typical optimization rules very naturally. By adding rewriting conditions to allow for temporary variables and considering real-world language features such as exceptions, the system can perform optimization of Java programs. We implemented a model checker that can check future and past temporal CTL operators symmetrically without any conversion. So far, a compiler optimizer using temporal logic was assumed to be impractical, because it consumes too much time. However, with our method, the generated Java compiler optimizer can compile seven of the SPECjvm98 benchmarks with a compile time from 4 seconds to 4 minutes. To our knowledge, our system is the first system that can make optimizers for real Java programs from specifications in CTL by using a model checker. So, the possibility and problems of this approach and consideration on how to overcome the problems is clarified by our work. We also gained insights into improving existing techniques for decreasing the compilation time and in specifying compiler optimizations.

収録刊行物

参考文献 (24)*注記

もっと見る

関連プロジェクト

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ