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