Compositional compiler correctness via parametric simulations

Abstract

Die Verifikation von Compilern ist für die Konstruktion von vollständig verifizierter Software essenziell. Jedoch beschränkt sich die meiste bisherige Forschung (z.B. CompCert) auf das Szenario der Kompilierung von ganzen Programmen. Um separate Kompilierung und das Linken von Erzeugnissen verschiedener Compiler zu unterstützen, scheint es erforderlich einen kompositionalen Begriff von Compilerkorrektheit zu entwickeln, der modular (kompatibel mit Linken), transitiv (mehrphasige Kompilierung unterstützend), und flexibel ist (anwendbar auf Compiler mit verschiedenen Zwischensprachen oder unkonventionellen Transformationen). In dieser Arbeit formalisieren wir einen solchen Korrektheitsbegriff basierend auf parametrischen Simulationen, und entwickeln auf diese Art einen neuartigen Ansatz zur kompositionalen Compilerverifikation. 1. Wir führen die grundlegende Idee von parametrischen (Bi-)simulationen ein und stellen eine konkrete Instanz vor. Diese bildet eine kompositionale Technik zum Beweisen von Programmäquivalenzen einer höheren ML-ähnlichen Sprache S. 2. Dann betrachten wir eine Umgebung, in der S-Programme in systemnahen Code einer Maschinensprache T übersetzt werden. Wir verallgemeinern unsere Formulierung von PBs zu parametrischen interlingualen Simulationen (PILS), und demonstrieren dass PILS als Fundament von kompositionaler Compilerverifikation dienen können. Unsere PB- und PILS-Entwicklungen wurden mittels des Beweissystems Coq durchgeführt und korrekt bewiesen.

Compiler verification is essential for the construction of fully verified software, but most prior work (such as CompCert) has focused on verifying whole-program compilers. To support separate compilation and to enable linking of results from different verified compilers, it is important to develop a compositional notion of compiler correctness that is modular (preserved under linking), transitive (supports multi-pass compilation), and flexible (applicable to compilers that use different intermediate languages or employ non-standard program transformations). In this thesis, we formalize such a notion of correctness based on parametric simulations, thus developing a novel approach to compositional compiler verification. The thesis is roughly divided into two parts. 1. We introduce the basic idea of parametric (bi-)simulations (PBs) and present a concrete instance of it. This instance constitutes a compositional technique for proving equivalences of programs written in the same higher-order ML-like language S. 2. We then move from such a single-language setting to a setting where S programs are being compiled into low-level code of some machine language T. We generalize our PB formalization to parametric inter-language simulations (PILS) and demonstrate that PILS can serve as a foundation for compositional compiler verification. Both our PB and PILS developments have been carried out and proven correct using the Coq proof assistant