Aditya Kanade

A compiler optimizer analyzes and transforms programs to improve their performance. This allows programmers to focus on functionality of programs without having to bother about efficiency of the generated code. Optimizers have therefore become an integral part of the modern compilers. However, a mistake in the design or the implementation of an optimizer can proliferate in the form of bugs in the softwares compiled through it.

The issue of soundness of optimizers is addressed at two levels: (1) One time guarantees are obtained at the design level by verifying optimization specifications and (2) run-time guarantees are obtained at the implementation level by validating optimizations performed. In this report, we present an approach which is uniformly applicable at both the levels.

Optimizations with similar objectives comprise of similar program transformations. Consequently, their proofs of semantic equivalence also consist of similar patterns. To simplify specification, we structure optimizing transformations as sequential compositions of primitive program transformations. For each primitive, we identify soundness conditions which guarantee that the transformation is semantics preserving. Proving soundness of an optimization therefore reduces to merely showing that the soundness conditions of the underlying primitives are satisfied. This avoids repeated proofs of semantic equivalence.

We use a temporal logic to specify program analyses and soundness conditions. Since programs are transformed step-by-step, we need to correlate temporal properties across transformations of programs. We therefore develop a logic called Temporal Transformation Logic and use it to verify optimization specifications.

We also propose a novel validation scheme. An optimizer can be instrumented to generate a trace of its execution in terms of predefined transformation primitives. If the trace conforms with the execution and soundness conditions of each of the primitive in the trace are satisfied then the optimizer preserves semantics of the particular input program.

We have developed a system for proving optimizing transformations sound (SPOTS). It consists of a PVS based framework for specification and verification and a framework to validate optimizer implementations in GCC v4.1.0. We have applied both the frameworks to several optimizations.

PhD thesis, Dept of Comp Sc and Engg, IIT Bombay, 2007, © Aditya Kanade.
Advisors: Uday P. Khedker and Amitabha Sanyal

PDF.