Amal Ahmed (Northeastern University, USA)
Title: Compositional Compiler Verification for a Multi-Language World
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.
Speaker 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).
Isil Dillig (University of Texas, Austin, USA)
Abstract: In contrast to program analysis where the goal is to verify that a program satisfies a given specification, the goal of program synthesis is to generate a program that, by construction, satisfies its specification. Despite the obvious duality between these two problems, the fields of program synthesis and analysis have thus far largely utilized very different techniques. In this talk, we argue that the concept of abstraction that has been the bedrock of program analysis for decades also plays a foundational role in program synthesis. In particular, just as abstractions allow us to efficiently construct correctness proofs in verification, we show that the same concept allows us to efficiently search for correct-by-construction programs in synthesis. Based on this idea, we describe a general-purpose synthesis framework where the abstract semantics of the target programming language drives the search for the desired program.
Speaker Bio: Isil Dillig is an Associate Professor of Computer Science at the University of Texas at Austin where she leads the UToPiA research group. Her current research interests include program analysis, synthesis, and automated logical reasoning. Dr. Dillig is a Sloan Fellow and a recipient of an NSF CAREER award. Her research has been recognized with various awards, such as an OOPSLA distinguished paper award, an ETAPS best award, and CACM research highlight distinctions. Outside of work, she enjoys hiking, scuba diving, and photography.
Viktor Vafeiadis (MPI-SWS, Germany)
Abstract: In the multicore/multiprocessor setting, different threads have diverging views of the shared memory, which are only weakly consistent with one another. For example, threads A and B may disagree on the order that two shared memory operations have happened; say A has seen the effect of operation C but not of operation D, while B has seen the effect of D but not of C. There has been a lot of work of specifying exactly how different can the views of two threads be–both at the architecture level with formal models for x86, ARM, and Power, and the programming language level with the C/C++ and Java memory models. In this talk, I will discuss what all this work entails for program correctness. How can we specify a concurrent library, say a queue or a set, in the weak memory model setting? What reasoning principles can we use to verify such a library?
Speaker Bio: Viktor Vafeiadis is a tenured faculty member at the Max Planck Institute for Software Systems (MPI-SWS). He got his PhD from the University of Cambridge in 2008, working on the combination of separation logic and rely-guarantee reasoning, for which he received the ACM SIGPLAN distinguished dissertation award. After postdoc positions at Microsoft Research and at the University of Cambridge, in October 2010 he joined MPI-SWS, where he has worked on verified compilation and weak memory concurrency.