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).
Azalea Raad (MPI-SWS, Germany)
Title: Correctness in a weakly consistent setting
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 the views of two threads can be – both at the architecture level with formal models for x86, ARM, and Power, and at the programming language level with 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: Azalea Raad is a post-doctoral researcher at the Max Planck Institute for Software Systems (MPI-SWS). She received her PhD from Imperial College London in 2017 under the supervision of Professor Philippa Gardner, working on specifying and verifying concurrent programs in the sequential consistency setting. She joined MPI-SWS in July 2017, where she has worked on semantic models for weak memory concurrency in different contexts, including software transactional memory and non-volatile memory.
Bernhard Scholz (University of Sydney)
Soufflé: A Datalog Engine for Static Analysis
Abstract: Soufflé is an open-source system for developing static program analyses in a declarative fashion. An analysis is expressed in a Datalog-like logic language. From the logic specification of the analysis, Soufflé synthesizes a highly efficient, parallel C++ program. Soufflé is currently being employed for industrial-strength static analysis problems, including large-scale program analysis and security analysis of cloud networks.
In this talk, will give an overview of the underlying technology of Soufflé, how to write Datalog-based static analyses, and present some industrial use-cases that are written in the Soufflé language. We will go beyond the scope of Soufflé as well, and discuss the performance challenges of modern Datalog engine, and possible techniques that help to solve the performance bottlenecks.
Speaker Bio: Bernhard Scholz is Associate Professor in Computer Science at The University of Sydney. His research interests are in programming languages. Before joining The University of Sydney, he worked for the Vienna University of Technology, and the University of Vienna in academic/research roles. He has held various visiting professorships at the University of Victoria, BC, Canada, Yonsei University, South Korea, and at the Sun Microsystems Laboratories. He had an extended stay at Oracle Labs, Brisbane, working as a Visiting Professor/Consulting Member of Staff on new techniques for declarative techniques for static program analysis.