Structuring Optimizing Transformations and
Proving Them Sound
Aditya Kanade, Amitabha Sanyal, and Uday Khedker
IIT Bombay, India
A compiler optimization is sound if the optimized program that it
produces is semantically equivalent to the input program. The proofs
of semantic equivalence are usually tedious. To reduce the efforts
required, we identify a set of common transformation primitives
that can be composed sequentially to obtain specifications of
optimizing transformations. We also identify the conditions under
which the transformation primitives preserve semantics and prove their
sufficiency. Consequently, proving the soundness of an optimization
reduces to showing that the soundness conditions of the underlying
transformation primitives are satisfied.
The program analysis required for optimization is defined over the
input program whereas the soundness conditions of a transformation
primitive need to be shown on the version of the program on which it
is applied. We express both in a temporal logic. We also develop a
logic called temporal transformation logic to correlate
temporal properties over a program (seen as a Kripke structure) and
its transformation.
An interesting possibility created by this approach is a novel scheme
for validating optimizer implementations. An optimizer can be
instrumented to generate a trace of its transformations in terms of
the transformation primitives. Conformance of the trace with the
optimizer can be checked through simulation. If soundness conditions
of the underlying primitives are satisfied by the trace then it
preserves semantics.