Generating java compiler optimizers using bidirectional 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 specications in temporal logic. The specication is simpler, and the generated optimizers run more eciently than previously reported work. We implemented a new model checker for a bidirectional CTL (computation tree logic), a branching temporal logic. The model checker can check future and past temporal CTL operators symmetrically without any conversion. We also present a new specication language based on the bidirectional CTL that can express typical optimization rules very naturally. By adding rewriting conditions and handling of temporary variables, the system can perform optimization of Java programs. 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 all seven of the SPECjvm98 benchmarks with a compile time from 15 seconds to 5 minutes. We also gained insights into improving existing techniques for decreasing the compi-lation time and expertise in specifying compiler optimizations.