Translation Validation of Advanced Compiler Optimizations

[0306538]纽约大学zuck， Lenore d .这是一个项目的延续，其最终目标是开发高级优化编译器的翻译验证方法，重点是针对epic的编译器和这些编译器的积极优化特征。所开发的方法将处理广泛的优化集，并可用于实现各种编译器的全自动认证器。以前的工作已经发展：1；“正确翻译”理论；2. 2 .“保结构”优化的翻译验证通用证明规则；TVOC——一个在EPIC编译器（SGI Pro-64）上实现证明规则的工具，并将证明义务发送给定理证明者（SRI的ICS）进行验证。4. 一个用于处理许多“结构修改”转换的证明规则，主要是循环优化；建议的工作扩展了以前的工作如下：1.发展理论和支持工具，处理程序间和程序内优化。2. 构建一个特殊用途的定理证明器将构建在CVC之上，该证明器将被定制以处理由方法生成的验证条件。识别并构建推测性优化的运行时检查。另外，它将执行转换的编译时验证。将项目范围扩展到与机器相关的优化，包括指令调度和（软件和硬件）流水线。该项目将为确保编译器在某些领域（如安全关键系统和编译到硅中）具有极高的可信度迈出重要的一步，在这些领域，正确性是最重要的。

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.