Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Volume 9 / Issue 3

available in:   HTML (96 kB) PDF (257 kB) PS (183 kB)
 
get:  
Similar Docs BibTeX   Write a comment
  
get:  
Links into Future
 
DOI:   10.3217/jucs-009-03-0191

 

Using Program Checking to Ensure the Correctness of Compiler Implementations

Sabine Glesner (Institute for Program Structures and Data Organization University of Karlsruhe, Germany)

Abstract: We evaluate the use of program checking to ensure the correctness of compiler implementations. Our contributions in this paper are threefold: Firstly, we extend the classical notion of black-box program checking to program checking with certificates. Our checking approach with certificates relies on the observation that the correctness 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 checking 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.

Keywords: certificates, code generation, compiler, compiler architecture, compiler generators, implementation correctness, program checking

Categories: D.2.4, D.3.4, F.3.1, F.4.2