Translation Validation of Advanced Compiler Optimizations

New York University, New York NY

Investigators

Abstract

Title: Translation Validation of Advanced Compiler Optimizations PI: Lenore Zuck Proposal Number: CCR-0098299 This goal of the research is to advance the state of the art in ensuring the correctness of compilation in the presence of extensive optimization. This will be achieved via the use of translation validation where, rather than verifying the compiler itself one constructs a tool that formally confirms that the target code produced by each run of the compiler is a correct translation of the source program. The methods being developed will handle an extensive set of optimizations for modern architectures, ranging from high level loop optimizations that dramaically change the structure of a program to low level machine dependent optimizations, such a instruction scheduling. The research will first develop the theory of a correct translation. Special care will be taken to obtain a maximally faithful representation of hardware factors characteristic of modern architectures, such as instruction latencies, CPU resources, etc. The preferred (and often mandatory) approach is that the validator tool should derive all of this information automatically by a carefully analysis of the source and the target. A major component of the secondpart of the proposal will be dedicated to the development of heuristics and analysis techniques by which this task can be accomplished.