Portal de Periódicos da CAPES

Using Program Checking to Ensure the Correctness of Compiler Implementations

2003; Verlag der Technischen Universität Graz; Volume: 9; Linguagem: Inglês

0948-695X

Sabine Glesner,

Software Testing and Debugging Techniques

We evaluate the use of program checking to ensure the correctness of com- piler implementations. Our contributions in this paper are threefold: Firstly, we extend the classical notion of black-box program checking to program checking with certifi- cates. Our checking approach with certificates relies on the observation that the correct- ness of solutions of NP-complete problems can be checked in polynomial time whereas their computation itself is believed to be much harder. Our second contribution is the application of program checking with certificates to optimizing compiler backends, in particular code generators, thus answering the open question of how program check- ing for such compiler backends can be achieved. In particular, we state a checking algorithm for code generation based on bottom-up rewrite systems from static single assignment representations. We have implemented this algorithm in a checker for a code generator used in an industrial project. Our last contribution in this paper is an integrated view on all compiler passes, in particular a comparison between frontend and backend phases, with respect to the applicable methods of program checking. Compiler correctness is a necessary prerequisite to ensure software correctness and reliability as most modern software is written in higher programming lan- guages and needs to be translated into native machine code. In this paper, we ad- dress the problem of implementing compilers correctly. Recently, program check- ing has been proposed as a method to achieve this goal. Program checking has been successfully applied to compiler frontends while its application to compiler backends has remained as an open problem. We close this gap. Therefore we pro- pose a novel checking method which we call program checking with certificates .I t is particularly suited for checking the results of optimization problems. We have applied program checking with certificates to code generation, a phase in op- timizing compilers which transforms intermediate representations into machine code. In this paper, we present our checking algorithm for such code genera- tors as well as a case study with experimental results proving the practicality of our approach. Moreover, we summarize previous work about frontend check- ing and compare it with our insights concerning backend checking. Thereby we