Code Optimization by Model Generation in Temporal Logic

DOI

Bibliographic Information

Other Title
  • 最適条件の時間論理記述を用いたモデル生成器によるコード最適化

Abstract

We propose a new method of automatic code optimization in compilers. First, we define a simple language similar to an intermediate language, and CTL*-FV which is an extension of CTL* to describe the specification of program control flow. Control flow can be considered as a model of this logic. Second, we present a procedure to obtain the conditions for the code to have the same meaning as the code which is to be optimized, and we also give logical formulae of necessary condition for optimization, such as the lack of dead code, etc. We obtain the optimized code by generating the models that satisfies these conditions with a model generator. Finally, we define the partial order of efficiency between programs, and show the codes obtained by this method are equivalent in this order.

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top