Personal tools
You are here: Home Events LFCS seminar: Amal Ahmed: Compositional compiler verification for a multi-language world

LFCS seminar: Amal Ahmed: Compositional compiler verification for a multi-language world

— filed under: ,

  • LFCS Seminar
  • Upcoming events
When Oct 10, 2017
from 04:00 PM to 05:00 PM
Where IF 4.31/4.33
Add event to calendar vCal

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 at a level suitable for a general audience and present a generic compositional compiler correctness (CCC) theorem that I’ll 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 proof architectures for the future. 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 refactoring 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.


Document Actions