Speaker: Amal Ahmed
Abstract:
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. Unfortunately, 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. Worse, to check if these theorems are sensible, reviewers must understand a massive amount of formalism.
In this talk, I will survey recent results, explaining pros and cons of their compiler-correctness statements, and then 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. In particular, I’ll explain why compositional compiler correctness is, in essence, a language interoperability problem and that building truly compositional verified compilers demands that we design languages that give programmers control over a range of interoperability (linking) options.