SHF:Small: Bringing Extensibility and Performance to Verified Compilers

SHF:Small：为经过验证的编译器带来可扩展性和性能

• 批准号: 1219172
• 负责人: Sorin Lerner
• 金额: $ 40万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-10-01 至 2016-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1219172&HistoricalAwards=false
• 关键词: SHF; Small; Bringing; Extensibility; Performance

The compiler is a tool that is central to the development of software. Its role is to translate the human-readable code written by a programmer into machine code that a computer can understand. Because the compiler creates the actual machine code that runs on the computer, a faulty compiler can lead to catastrophic failures, including errors in medical devices, in fly-by-wire aviation software, and in automotive systems. This research will lead to more reliable compilers, which in the end will increase our confidence in the software that has now become ubiquitous and safety-critical in our daily lives.This project will develop new techniques for building compilers to ensure the utmost level of rigor and reliability, so that we can know with certainty that the machine code running on the computer does exactly what the programmer intended it to do. To achieve this goal, the principal investigator will investigate ways of using proof assistants to implement formally verified compilers. More specifically, the research will explore techniques for making formally verified compilers like Compcert generate better code, so that they can be more competitive with mainstream compilers like GCC and LLVM. Furthermore, the research will also investigate ways of decreasing the proof burden, so that verified compilers like Compcert can be developed and updated more easily. In the end, this research will enable formally verified compilers to become more mainstream, so that they can used more broadly by programmers.

编译器是软件开发至关重要的工具。 它的作用是将程序员写入的人类可读代码转换为计算机可以理解的机器代码。 由于编译器创建在计算机上运行的实际机器代码，因此编译器可能会导致灾难性故障，包括医疗设备，逐线航空航空软件中的错误和汽车系统中的错误。 这项研究将导致更可靠的编译器，最终将提高我们对现在已经变得无处不在的软件的信心，该软件在我们的日常生活中变得无处不在，至关重要。该项目将开发新的技术，以确保确保在计算机上运行的机器代码可以确切地知道程序员的最大程度的严格性和可靠性，以确保我们能够确切地知道程序员的意图。 为了实现这一目标，主要研究人员将调查使用证明助手实施正式验证的编译器的方法。 更具体地说，该研究将探讨用于制造诸如CompCert（CompCert）正式验证的编译器的技术，可以生成更好的代码，以便它们可以与GCC和LLVM等主流编译器更具竞争力。 此外，该研究还将研究减轻证明负担的方法，以便可以更轻松地开发和更新经过验证的编译器。 最后，这项研究将使经过正式验证的编译器能够变得更加主流，以便它们可以被程序员更广泛地使用。