CAREER: Verified Compilers for a Multi-Language World

职业：多语言世界的经过验证的编译器

• 批准号: 1453796
• 负责人: Amal Ahmed
• 金额: $ 50.81万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-05-01 至 2022-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1453796&HistoricalAwards=false
• 关键词: CAREER; Verified; Compilers; Multi; Language

Title: CAREER: Verified Compilers for a Multi-Language WorldCompilers play a critical role in the production of software. As such, they should be correct. That is, they should preserve the behavior of all programs they compile. Despite remarkable progress on formally verified compilers in recent years, these compilers suffer from a serious limitation: they are proved correct under the assumption that they will only be used to compile whole programs. This is an entirely unrealistic assumption since most software systems today are comprised of components written in different languages compiled by different compilers to a common low-level target language. The intellectual merit of this project is the development of a proof architecture for building verified compilers for today's world of multi-language software: such verified compilers guarantee correct compilation of components and support linking with arbitrary target code, no matter its source. The project's broader significance and importance are that verified compilation of components stands to benefit practically every software system, from safety-critical software to web browsers, because such systems use libraries or components that are written in a variety of languages. The project will achieve broad impact through the development of (i) a proof methodology that scales to realistic multi-pass compilers and multi-language sofware, (ii) a target language that extends LLVM---increasingly the target of choice for modern compilers---with support for compilation from type-safe source languages, and (iii) educational materials related to the proof techniques employed in the course of this project.The project has two central themes, both of which stem from a view of compiler correctness as a language interoperability problem. First, specification of correctness of component compilation demands a formal semantics of interoperability between the source and target languages. More precisely: if a source component (say s) compiles to target component (say t), then t linked with some arbitrary target code (say t') should behave the same as s interoperating with t'. Second, enabling safe interoperability between components compiled from languages as different as Java, Rust, Python, and C, requires the design of a gradually type-safe target language based on LLVM that supports safe interoperability between more precisely typed, less precisely typed, and type-unsafe components.

标题：职业生涯：多语言世界的经验证的编译器编译器在软件生产中发挥着关键作用。因此，他们应该是正确的。也就是说，它们应该保留它们编译的所有程序的行为。尽管近年来在正式验证的编译器方面取得了显著的进展，但这些编译器受到了严重的限制：它们被证明是正确的，假设它们将仅用于编译整个程序。这是一个完全不切实际的假设，因为今天的大多数软件系统都是由不同的编译器以不同的语言编写的组件组成的，这些组件被编译成一种通用的低级目标语言。这个项目的智力价值在于为当今的多语言软件世界开发了一种验证体系结构，用于构建经过验证的编译器：这种经过验证的编译器保证组件的正确编译，并支持与任意目标代码的链接，无论其来源如何。该项目更广泛的意义和重要性在于，组件的经过验证的编译几乎将使每个软件系统受益，从安全关键软件到网络浏览器，因为这些系统使用以各种语言编写的库或组件。该项目将通过开发(I)可扩展到现实的多遍编译器和多语言软件的验证方法，(Ii)扩展LLVM的目标语言-越来越多地成为现代编译器的选择目标--并支持从类型安全的源语言进行编译，以及(Iii)与该项目过程中使用的验证技术有关的教育材料的开发，实现广泛的影响。该项目有两个中心主题，这两个主题都源于将编译器正确性视为语言互操作性问题的观点。首先，组件编译正确性的规范要求源语言和目标语言之间的互操作性的形式化语义。更准确地说：如果一个源组件(比如S)编译成目标组件(比如t)，那么链接到某个任意目标代码(比如t‘)的t应该与S与t’互操作的行为相同。其次，要实现从Java、Rust、Python和C等不同语言编译的组件之间的安全互操作性，需要设计一种基于LLVM的逐渐类型安全的目标语言，该语言支持类型更精确、类型不太精确和类型不安全的组件之间的安全互操作性。

项目成果

The next 700 compiler correctness theorems (functional pearl)

• DOI: 10.1145/3341689
• 发表时间: 2019-07
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Daniel Patterson;Amal J. Ahmed

Graduality and parametricity: together again for the first time

渐进性和参数化：首次再次结合在一起

• DOI: 10.1145/3371114
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: New, Max S.;Jamner, Dustin;Ahmed, Amal
• 通讯作者: Ahmed, Amal

Under Control: Compositionally Correct Closure Conversion with Mutable State

受控：具有可变状态的组合正确的闭包转换

• DOI: 10.1145/3354166.3354181
• 发表时间: 2019
• 期刊: Principles and Practice of Programming Languages 2019 (PPDP ’19
• 作者: Mates, Phillip;Perconti, Jamie;Ahmed, Amal
• 通讯作者: Ahmed, Amal