Christophe Alias, (CR Inria), Laure Gonnord (MCF Lyon 1), Yannick Zakowski, (CR Inria, contact person)
Prerequisites
- Notions in compilers and linear algebra.
- Strong interest for both applied and theoretical research.
Overview
Optimizing compilers fundamentally rely on static analyses to infer the information required to justify optimizations. The more precise the analysis, the more agressive the possible optimization. Through this course, we propose to look through three different lenses at the problematic of designing static analyses for compilers.
Part 1: the Polyhedral Model, cornerstone of hardware compilation (Christophe Alias)
The first angle we will discuss addresses the need for parallelism. Since the end of Dennard scaling, hardware architectures indeed rely more and more on parallelism to gain performances. In high-performance computing, single-core CPU have been replaced by multi-core, and the r is to use more and more hardware accelerators like GPU, many-core or FPGA (programmable hardware). In embedded systems, hardware accelerators are typically embedded together with the CPU on the same chip, called a System-on-Chip.
This part focuses on the design of hardware accelerators. Producing efficient implementations while keeping the development effort reasonable indeed requires new tools to tackle the increasing complexity of modern systems. To this end, the current trend in hardware design is to generate at least large parts of the hardware from usual programming languages such as C. This is called "High-Level Synthesis" (HLS), or "hardware compilation". One of the challenges in hardware compilation is the extraction of parallelism: the source program is given in sequential form, and the generated hardware must be highly parallel to be efficient.
We will present the main theoretical tool used to solve this problem, the polyhedral model, and study several static analyses that leverage this model.
Part 2: Abstract Interpretation, a general framework for sound, decidable analyses (Laure Gonnord)
The Rice theorem never ceases to loom over the compiler designer: the dream for perfect analyses is hopeless. One is therefore coerced into trading away at least one of the completeness, correctness or generality of the analysis. When one takes the position to give up on completeness, a new challenge arises: how to design sound analyses that remain as precise as possible, while being computationally as efficient as possible?
Abstract Interpretation is a rich mathematical framework providing tools, techniques and principles to design and reason about such sound analyses. At its core reside the notion of abstraction: the analysis designer carefully crafts a mathematical domain that only retains the information about the concrete state that she deems vital. Once this domain is fixed, an efficient abstract interpreter operating over this abstract state can be implemented, while retaining a formal semantic connection to the underlying operational semantics of the language.
Through this part, we will introduce the framework of abstract interpretation, study its mathematical foundation, and take a closer look at several popular abstract domains. In particular, we will see how to specialize the framework of abstract interpretation for its specific use as part of an optimizing compiler.
Part 3: Verified Static Analyses, the art of formally proving correct our analyses (Yannick Zakowski)
Any program analysis comes with a promise: any invariant they return are worthy of their name, they will hold dynamically at the program point concerned in any execution. But whose to hold accountable the designer of the analysis of this promise?
In this part of the course, we will study how to exculpate ourselves from this question by proving formally that our analysis is correct. Such endeavor is relevant to any analysis meant to be used in a critical environment, but has found in recent years a particular echo in the context of verified compilation, the discipline of programming compilers and formally proving that they preserve the semantics of programs.
We will through this portion of the course introduce the Coq proof assistant and discuss together the detail of formally stating the correctness of an analysis with respect to the formal semantics of the language. We will investigate decidability issues that take significance when formalizing abstract interpretation in a constructive logics, and we will build together a toy analyzer formally proved correct. Finally, we will discuss the recent development of constructive Galois connection that aim to address these issues.
References
Hardware Compilation:
- Philippe Coussy and Adam Morawiec, “High-Level Synthesis: from Algorithm to Digital Circuit”
- Joao M.P. Cardoso, Pedro C. Diniz, “Compilation Techniques for Reconfigurable Architectures”
- Jingling Xue, “Loop tiling for parallelism”.
Abstract Interpretation:
- Xavier Rival and Kwangkeun Yi, “Introduction to Static Analysis — An Abstract Interpretation Perspective”
- Patrick and Radhia Cousot, founding paper of the domain
Formal verification: