Translation Validation of Advanced Compiler Optimizations

点击翻译按钮获取中文摘要

ABSTRACT0306538Zuck, Lenore D.New York UniversityThe is a continuation of a project whose ultimate goal is to develop amethodology 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.