Automatically Checking the Correctness of Program Analyses and

Dr. Lerner is from the University of Washington
The reliability of any program depends on the reliability of all the tools that are used to process it, including compilers, static and dynamic checkers, and source-to-source translators. Unfortunately, these program manipulators are hard to get right, even for experts in the field of program analysis. It takes years before a new compiler is stable enough for programmers to trust it, and even then there are no guarantees about the compiler's correctness.

In this talk, I describe a technique for providing strong correctness guarantees about the core part of any program manipulator, the program analyses and transformations. Our approach introduces a domain-specific language, Rhodium, in which program analyses and transformations are expressed. Aside from reducing the potential for errors by making program manipulators easier to write and maintain, the restricted domain of Rhodium makes it amenable to rigorous static checking that would be impossible otherwise. In particular, once written in Rhodium, program analyses and transformations can be checked for correctness automatically, before they are even run once.

In addition to leading to more trustworthy program manipulators, the Rhodium system also provides a practical foundation for making these program manipulators safely extensible. Oftentimes, it is the end programmer who has the application-domain knowledge and the coding-pattern knowledge necessary to implement useful checkers and optimizations. The Rhodium system empowers end programmers with the ability to add their own domain-specific analyses and transformations to existing program manipulators, without fear of breaking them.