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.

标题：职业：多语言世界专家的验证编译器在软件生产中起着至关重要的作用。 因此，它们应该是正确的。 也就是说，他们应该保留其编译的所有程序的行为。尽管近年来在正式验证的编译器上取得了显着进展，但这些编译器受到严重限制：在假设它们仅用于编译整个程序的假设下，它们被证明是正确的。这是一个完全不现实的假设，因为当今大多数软件系统由不同编译器编写的不同语言编写的组件组成，该组件由不同的编译器编写为通用的低级目标语言。 该项目的智力优点是开发用于为当今多语言软件世界构建经过验证的编译器的证明体系结构：这种经过验证的编译器保证正确编译组件的编译并支持与任意目标代码相关联，无论其来源如何。该项目更广泛的意义和重要性是，验证组件的汇编几乎可以使每个软件系统（从安全至关重要的软件到Web浏览器）受益，因为这样的系统使用库或组件以各种语言编写。该项目将通过（i）一种证明方法来实现广泛的影响，该方法可以扩展到现实的多通编译器和多语言SOFWARE，（ii）扩展LLVM的目标语言 - 越来越多地支持现代编译器的目标 - 与类型的源语言和（III）材料相关的两种投射均与（III II）的材料相关的媒体材料的支持，并支持这两种材料，并在此方面使用（iii）的课程，该课程在这两个方面均在此过程中，该课程在此方面涉及这一范围，该课程在此方面涉及这一范围，该课程涉及这一范围，该课程涉及这一范围，该课程涉及这一范围，这些材料涉及这一范围，这些材料涉及这一范围，这些材料涉及该课程。从编译器正确性作为语言互操作性问题的视图中。首先，组件编译的正确性规范需要源和目标语言之间互操作性的正式语义。更准确地说：如果源组件（例如s）编译到目标组件（例如t），则与某些任意目标代码（例如t'）链接的t应与与t互操作的s相同。其次，从与Java，Rust，Python和C不同的语言中启用安全互操作性，需要根据LLVM的逐渐型号安全的目标语言来设计，该目标语言支持更精确键入，更精确的键入，类型-Unsafe组件之间的安全互操作性。

项目成果

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