Sciweavers

ENTCS
2007

Structuring Optimizing Transformations and Proving Them Sound

13 years 3 months ago
Structuring Optimizing Transformations and Proving Them Sound
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 p...
Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Aditya Kanade, Amitabha Sanyal, Uday P. Khedker
Comments (0)