Automatic Validation of Improving Transformations and Related Applications

提案编号：CCR-9904943标题：代码改进转换的自动验证 及相关应用研究者：Robert货车Engelen，大卫沃利和袁昕摘要：确保软件系统正确执行是至关重要的。 这个过程的一部分是确保编译器产生的机器码能够准确地表示源代码级指定的算法。 这是一项艰巨的任务，因为优化编译器不仅将源代码翻译为机器代码，而且可能会将数百或数千个代码改进转换应用到即使是相对较小的程序。 这个项目将使用两种方法来极大地简化代码的验证，改进转换。 首先，将检查每个改进变换前后程序表示的等价性，而不是试图直接将程序和目标程序等同起来。 每一个单独的代码改进转换通常只包含几个更改。 第二，只检查程序中发生变化的区域，而不是整个程序表示。 被改进的转换改变的程序表示的区域通常是相当小的。 等价性将通过证明该区域对程序其余部分的影响在改进变换之前和之后保持不变来证明。 好处包括更简单的编译器错误诊断和更可靠的编译器。

Proposal Number: CCR-9904943Title: Automatic Validation of Code Improving Transformations and Related ApplicationsInvestigators: Robert van Engelen, David Whalley, and Xin YuanAbstract:Ensuring that software systems execute correctly is vital. One portionof this process is to ensure that the compiler produces machine codethat accurately represents the algorithms specified at the source codelevel. This is a formidable task since an optimizing compiler not onlytranslates the source code to machine code, it may apply hundreds orthousands of code improving transformations to even a relatively smallprogram. This project will use two approaches that dramatically simplifythe validation of code improving transformations. First, the equivalenceof the program representation before and after each improvingtransformation will be checked, rather than attempting to equate thesource and object programs directly. Each individual code improvingtransformation typically consists of only a few changes. Second, onlythe region of the program that has changed, as opposed to the entireprogram representation, will be checked. The regions of the programrepresentation that are changed by an improving transformation aretypically quite small. The equivalence will be shown by demonstratingthat the effects of the region on the rest of the program will remain thesame before and after the improving transformation. The benefits includesimpler diagnosis of compiler errors and more reliable compilers.