Amal Ahmed
Talk: Compositional Compiler Verification for a Multi-Language World
- Date and Time
- October 30, 2018 at 12:00pm (lunch talk)
- Location
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, discussing 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. 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.
Bio
Amal Ahmed is an Associate Professor of Computer Science at Northeastern University. Her research interests include type systems and semantics, compiler verification, language interoperability, dependent types, and gradual typing. She is known for her work on scaling the logical relations proof method to realistic languages – with features like memory allocation and mutation, objects, and concurrency – leading to wide use of the technique, e.g., for correctness of compiler transformations, soundness of advanced type systems, and verification of fine-grained concurrent data structures. Her primary focus of late has been on developing an architecture for building correct and secure compilers that support safe inter-language linking of compiled code. Her awards include an NSF Career Award and a Google Faculty Research Award. She has served as program chair for ESOP and on the steering committees of ETAPS, ESOP, PLMW, and ICFP. She is also a frequent lecturer at the annual Oregon Programming Languages Summer School (OPLSS).