SHF: Medium: Formal Methods as a First-Class Citizen of a Mainstream Compiler Framework

University Of Utah, Salt Lake City UT

Investigators

Abstract

Compilers and compiler-like tools have always been an important part of achieving high programmer productivity. This is especially true now due to the proliferation of new application domains, such as big data, machine learning, and AI, that are spurring the development of new hardware and new programming languages. This project develops an open-source compiler infrastructure, called multi-level intermediate representation (MLIR), that promises to make compilers and compiler-like tools easier to build by automatically generating some of the most tedious and error-prone kinds of compiler code from a relatively simple, high-level specification. MLIR supports the creation of domain-specific dialects so that it can be used to solve different kinds of problems. The project explores how to enable developers implementing a new MLIR dialect to formally specify the meaning of operations in the dialect, in order to support automated generation of important tools such as interpreters, optimizers, and translation validators, which use an automated theorem prover to show that an optimizing compiler did not make any mistakes. The project's broader agenda is to push the mathematical foundations of compilation into practice, in an important open-source compiler toolchain, so that the benefits of formal-methods-driven software development can impact a large number of users. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.