Translation Validation of Advanced Compiler Optimizations

纽约大学扎克，Lenore D.该项目是一个项目的继续，该项目的最终目标是开发用于高级优化编译器的翻译验证的方法，重点是EPIC目标编译器和此类编译器的积极优化特性。所开发的方法将处理广泛的优化集合，并可用于为广泛的编译程序实现全自动证明器。以前的工作已开发：1.“正确翻译”的理论；2.“结构保持”优化的翻译验证的一般证明规则；3.TVOC--在EPIC编译程序(SGI Pro-)上实现证明规则并将证明义务发送给定理证明器(SRI的ICS)验证的工具；4.处理许多“结构修改”变换的证明规则，主要是循环优化；拟议的工作扩展了以前的工作如下：1.开发处理过程间和过程内优化的理论和支持工具。2.将在CVC的基础上建立一个特殊用途的定理证明器，该CVC将量身定做，以处理方法产生的验证条件。识别并构造推测性优化的运行时检查。此外，它还将执行编译时转换验证。4.将项目的范围扩展到机器相关的优化，涉及指令调度和(软件和硬件)流水线。该项目将向确保在诸如安全关键系统和汇编成硅片等最令人关切的正确性的领域中的编译器的极高水平的信心迈出重要的一步。

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.