Séminaire des équipes de recherche
Compositional Compiler Verification for a Multi-Language World
- Date : 27/09/2017
- Lieu : Inria de Paris, Salle Jacques-Louis Lions 2, bâtiment C - 10h30
- Intervenant(s) : Amal Ahmed (Northeastern University)
Verified compilers are typically proved correct under severe restrictions on what the compiled code may be linked with, from no linking at all to linking with only the output of the same compiler.
But such assumptions don't match the reality of how we use these compilers as most software today is comprised of components written in different languages compiled by different compilers to a common target.
A key challenge when verifying correct compilation of components -- or "compositional" compiler correctness -- is how to formally state the compiler correctness theorem so it supports linking with target code of arbitrary provenance, as well as verification of multi-pass compilers. Recent results state their correct-component-compilation theorems in remarkably different ways, yielding pros and cons that aren't well understood. Worse, to check if these theorems are sensible, reviewers must understand a massive amount of formalism.
In this talk, I will survey recent results and present a generic compositional compiler correctness (CCC) theorem that we argue is the desired theorem for any compositionally correct compiler. Specific compiler-verification efforts can use their choice of formalism "under the hood'' and then show that their theorems imply CCC. I'll discuss what CCC reveals about desired properties of proof architectures going forward. I'll argue that compositional compiler correctness is, in essence, a language interoperability problem: embedding a single-language fragment in a multi-language system affects the notion of program equivalence that programmers use when reasoning about their code and that compiler writers use when reasoning about the correctness of compiler optimizations. For viable solutions in the long term, we must design languages that give programmers control over a range of interoperability (linking) options.