Automatic Validation of Improving Transformations and Related Applications

提案编号：CCR-9904943标题：改进转换和相关应用的代码的自动验证调查员：Robert van Engelen、David Whalley和Xin袁摘要：确保软件系统正确执行至关重要。这个过程的一个部分是确保编译器生成的机器代码能够准确地表示在源代码级指定的算法。这是一项艰巨的任务，因为优化编译器不仅将源代码翻译成机器代码，甚至可能对一个相对较小的程序应用数百或数千个代码来改进转换。该项目将使用两种方法来极大地简化代码改进转换的验证。首先，检查每次改进转换前后程序表示的等价性，而不是试图将源程序和目标程序直接等同。每个单独的代码改进转换通常只由几个更改组成。其次，只检查程序中已更改的区域，而不是检查整个程序表示。通过改进的转换改变的程序表示的区域通常非常小。这种等价性将通过证明区域对程序其余部分的影响在改进改造前后保持不变而得到证明。其好处包括更简单的编译器错误诊断和更可靠的编译器。

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.