Zuck, Lenore D. New York University
The is a continuation of a project whose ultimate goal is to develop a methodology for the translation validation of advanced optimizing compilers, with an emphasis on EPIC-targeted compilers and the aggressive optimizations characteristic to such compilers. The methods developed will handle an extensive set of optimizations and could be used to implement fully automatic certifiers for a wide range of compilers. Previous work has developed: 1. the theory of a "correct translation"; 2. a general proof rule for translation validation of "structure preserving" optimizations; 3. TVOC -- a tool that implements the proof rule on an EPIC compiler (SGI Pro-64) and sends the proof obligations to be verified by a theorem prover (SRI's ICS.) 4. a proof rule for dealing with many "structure modifying" transformations, mostly loop optimizations; The proposed work extends the previous work as follows: 1.develop the theory, and the supporting tools, that deal with inter- and intra-procedural optimizations. 2. build a special-purpose theorem prover will be built on top of CVC that will be tailored to handle the verification conditions generated by the methodology. 3. identify and construct run-time checks of speculative optimizations. In addition, it will perform a compile-time validation of the transformation. 4.Extend scoppe of project to machine-dependent optimizations, involving instruction scheduling and (software as well as hardware) pipelining. This project will provide a major step towards ensuring an extremely high level of confidence in compilers in areas, such as safety-critical systems and compilation into silicon, where correctness is of paramount concern.
