Translation Validation of Advanced Compiler Optimizations

Zuck，Lenore D.纽约大学这是一个项目的继续，其最终目标是开发高级优化编译器的翻译验证方法，重点是EPIC目标编译器和这种编译器的积极优化特性。 开发的方法将处理一个广泛的优化集，并可用于实现全自动认证的广泛的编译器。“正确翻译”理论; 2.“结构保持”翻译验证的一般证明规则 优化;3. TVOC --一个在EPIC编译器（SGI Pro-64）上实现证明规则的工具，并将证明义务发送给定理证明器（SRI的ICS）进行验证。4.一种处理多种“结构修改”的证明规则 转换，主要是循环优化;建议的工作扩展了以前的工作如下：1.发展的理论，和支持工具，处理间和内过程优化。 2.建立一个特殊用途的定理证明器将建立在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.