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

SHF：Medium：作为主流编译器框架的一等公民的形式方法

• 批准号: 1955688
• 负责人: John Regehr
• 金额: $ 111.47万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-06-01 至 2024-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1955688&HistoricalAwards=false
• 关键词: SHF; Medium; Formal; Methods; First

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.

编译器和编译器样工具一直是提高程序员生产率高的重要组成部分。现在尤其如此，这是由于新应用程序，机器学习和AI等新的应用程序域的扩散，这些域促进了新硬件和新编程语言的开发。该项目开发了一个称为多级中间表示（MLIR）的开源编译器基础架构，该基础架构有望通过自动生成一些相对简单，高级的高级规格来自动生成一些最繁琐且易用的编译器代码，从而使编译器和编译器般的工具更易于构建。 MLIR支持特定于域的方言的创建，以便它可以用于解决各种问题。该项目探讨了如何使开发人员实现新的MLIR方言以正式指定方言中操作的含义，以支持自动生成重要工具，例如口译器，优化者和翻译验证器，这些工具使用自动定理供供者，以表明优化编译器没有犯任何错误。 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.