Translation Validation of Advanced Compiler Optimizations

高级编译器优化的翻译验证

• 批准号: 0456163
• 负责人: Lenore Zuck
• 金额: $ 11.38万
• 依托单位: University of Illinois at Chicago
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2004
• 资助国家: 美国
• 起止时间: 2004-08-15 至 2006-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0456163&HistoricalAwards=false
• 关键词: Translation; Validation; 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.

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