Automatic Generation and Verificaiton of Optimizers

Objective
There have been studies on proving the correctness of specification of optimizing transformations commonly carried out by a compiler. However, these approaches have been less than satisfactory because the methods have a limited applicability and are not fully automated. Further, the correctness of implementations of optimizers with respect to the specifications is still open to question. We solve the first problem by developing a fully automated method for verifying specifications which cover a larger class of optimizations. The second problem can be partly alleviated by constructing an optimizer generator. This will read in the specification of an optimization and automatically gen- erate the corresponding optimizer, much alike the parser generator YACC, which generates parsers from context free grammars. Instead of showing the correctness of each individual implementation, one now has to show the correctness of the generator, that it correctly implements any optimization specification. The trustworthiness of the generator can be established through repeated use thereby enhancing the trustworthiness of optimizers leading to increased trustworthiness of compilers.

Project Deliverables
An optimizer generator which will take as input specification of an optimization. The specification would include
  • The analysis requirements.

  • The transformations and associated conditions.

  • The certification objectives (viz. profitability, safety, consistency etc.)

The generator would automatically generate an implementation of the optimizer which can be plugged into a GCC included compiler. A methodology for generating verification conditions which can be proved by theorem provers.