SHF: SMALL: Intermediate Languages for Safe and Efficient Compilation

University Of Oregon Eugene, Eugene OR

Investigators

Abstract

The importance of compiler verification is well established, especially for high-security and high-assurance applications. Regardless of how confident we are in our source code, no amount of program verification can survive the compilation process if the compiler introduces its own bugs and security flaws. Even though verified compilers are a reality today, many of the techniques employed by today's compiler writers have not made it into a formal system. This undermines confidence in a correctness proof of an optimizing compiler. The intellectual merit of this research is the design and implementation of intermediate languages that address both safety and efficiency concerns. The work focuses on the Glasgow Haskell compiler. However, the development is not tied to a specific language but focuses on a more general framework. The broader impact of the research consists of improving the approaches to verified compilation; providing a solid semantics for all stages of the compiler makes verification more compositional and makes verifying more complex compilers feasible. The project impacts more than just intermediate languages, because the broader lessons learned can be incorporated into source languages themselves. The work represents an important step toward extending current languages with proving capabilities by formally addressing the difficult challenge of integrating dependent types and effects. Functional language implementations rely heavily on effects for efficiency. Haskell, for example, is a pure functional language but its implementation uses memoization that involves reassignment. Intermediate languages that adequately represent implementation techniques must support effects. Making effects explicit not only increases confidence in compiler correctness, but also presents more opportunities for optimizations to produce better code. Whereas current research has focused on pushing high-level features down the compilation pipeline, the goal here is to also pull low-level features up the pipeline. Finding the right balance between high and low levels is challenging, since one wants to exploit low-level features to enhance efficiency without ruining the advantages of purity and ultimately hindering more than helping optimizations. The key to design useful intermediate languages is not that programs are necessarily pure, but that they use benign effects, namely effects that guarantee functional behavior. The guiding principle is to keep a strong connection with proof theory in the design and models of intermediate languages, especially the ones with mixed calling conventions.