Lectures

Compiler Bugs: Detecting Them and Understanding Their Impact and Dynamic Symbolic Execution with KLEE

Cristian Cadar

(1) In this talk, I will first describe the challenges of meaningfully testing compilers, and then survey some of the main techniques that have been successfully applied in this space. I will also discuss the impact of compiler bugs from several perspectives: the security risks of compiler bugs, the extent to which they affect the correctness of deployed software, and the difficulty of debugging software affected by them. The talk is primarily targeted to those who are new to the area of compiler testing, but it will also include several parts useful to a more specialist audience.

(2) Dynamic symbolic execution has gathered a lot of attention in recent years as an effective technique for generating high-coverage test suites and finding deep errors in complex software applications. In this tutorial-style presentation, I will introduce the main concepts of dynamic symbolic execution and exemplify them in the context of our KLEE symbolic execution infrastructure. The talk is primarily targeted to those who have no direct experience with dynamic symbolic execution and KLEE, but the talk will also include several parts useful to a more specialist audience.


Easy SSA Building - C2 Style and High Performance from understanding the Low Levels

Cliff Click

(1) How the HotSpot C2 JIT builds and optimizes SSA form quickly and simply. No fancy algorithm needed!

(2) A talk on X86 processor performance, with a live code-along session looking at the performance tradeoff between Bandwidth and Garbage Collection. Bring your laptop & fav Java IDE; Java code and ~2.7G dataset provided.


Types for Dynamic Languages

Jeffrey S. Foster

Dynamic languages are flexible, fun to use, and have a great power-to-code-weight ratio. But the lack of static typing can impede software development, make code maintenance harder, and lead to bugs that lurk in code for a long time. In these lectures, I will discuss some of the technical challenges and solutions for adding static typing to Ruby, a dynamic programming language. I will begin by presenting the basics of static type systems and type checking. Then I will discuss extensions required to statically type check the language constructs in Ruby and other dynamic languages. Next, I will show how to use type-level computations to perform static typing in the presence of powerful dynamic language features like metaprogramming. Finally, I will talk about type inference and discuss challenges and solutions for inferring usable, rather than most general, types.


Sparse abstract interpretation for compilers

Laure Gonnord

Proving the absence of bugs in a given software (problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers).
In a first part of the lecture, I will present a basic crash course on classical abstract interpretation, that has demonstrated its pertinence for software verification, and make a first assessment on the (quasi)impossibility of using the framework "as this" in production compilers.
In the second part, I will present some experiences in the design of scalable "sparse" static analyses inside compilers, and try to make a synthesis about the general framework we, together with my coauthors, used to develop them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.


What should a programming language implementation be? and Where the wild pointers are

Stephen Kell

(1) A box that goes fast? A comfortable space to work in? A unifying overlord that "rules" all software? An obedient servant? An intelligent collaborator? A window onto a wider world? In this relatively high-level lecture I'll examine different attitudes to this question, as manifest in different real language implementations over history, and use these to explain or hypothesise some directions of ongoing and future work. One theme will be how the goal of serving human beings is, curiously, slipping further down the agenda even while machine resources are more plentiful than ever.

(2) "A linker, a debugger and a garbage collector walked into a bar, all looking for the manager." In this relatively low-level lecture I'll cover why these systems are all different facets of the same strangely-shaped coin, why the folklore dichotomy of "managed vs unmanaged" is obscuring useful points in the design space, why this is hurting our ability to build tools and offer usable interoperability among languages/implementations, and one possible evolutionary approach for doing better. An emergent theme will be that language implementations are arguably in need of an "hourglass architecture" rather like the Internet's, and that handling of pointers, in their many guises, is the main unresolved challenge.


Beyond polyhedra: optimizing irregular programs

Milind Kulkarni

In these lectures, I will focus on the problem of compile-time scheduling optimizations that restructure computations to improve locality and parallelims. Traditional approaches to this problem reason about loop structures and schedules in terms of polyhedra, but there has been little success in extending such approaches beyond loop-based programs. I will start by briefly introducing the basic concepts used in reasoning about and transforming loop programs. I will then argue that there are interesting scheduling transformations that can be done for non–loop based programs, in particular recursive traversla programs such as those that arise in graphics, data mining, and simulation. I will survey recent work from the last decade on designing and implementing these transformations. Then, I will discuss recent advances in developing unified frameworks for representing, reasoning about, and transforming programs that deal with loops and recursion. Time permitting, we will also use one of these frameworks to explore and design a new transformation for recursive programs.


Formal Methods for Machine Learning Pipelines

Caterina Urban

Formal methods can provide rigorous correctness guarantees on hardware and software systems. Thanks to the availability of mature tools, their use is well established in the industry, and in particular to check safety-critical applications as they undergo a stringent certification process. As machine learning is becoming more and more popular, machine-learned components are now considered for inclusion in critical systems. This raises the question of their safety and their verification. Yet, established formal methods are limited to classic, i.e. non machine-learned software. Applying formal methods to verify systems developed by machine learning pipelines has only been considered recently and poses novel challenges in soundness, precision, and scalability. In this lecture, we will provide an overview of the formal methods developed so far for machine learning pipelines, highlighting their strengths and limitations. We will present several approaches through the lens of different software properties and targeting software across all phases of a machine learning pipeline, with a focus on abstract interpretation-based techniques. We will then conclude by offering perspectives for future research directions in this context.


Introduction to reactive programming in SKIP

Julien Verlaguet

Ever wanted to codegen something only to realize that your workflow had become unusable? Who wants to wait minutes for their build to finish?
Nobody ...
We want our tools in general (and our programming languages in particular) to be fast. We want to be able to iterate on our code without waiting. In other words, we want our tools to be reactive!
In this lecture, we will explore how to build a reactive compiler for a small programming language using the programming language SKIP. By the end of the class, you should be able to write tools that incrementally update, not in seconds, but in milliseconds when a change occurs.