SHF: Small: Foundations of Just-in-Time Compilation

SHF：小型：即时编译的基础

• 批准号: 1618732
• 负责人: Jan Vitek
• 金额: $ 44.98万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2021-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1618732&HistoricalAwards=false
• 关键词: SHF; Small; Foundations; Just; Time

Modern programming languages ranging from Java to Matlab rely on just-in-time compilation techniques to achieve performance competitive with computer languages such as C or C++. What sets just-in-time compilers apart from batch compilers is that they can observe the programs actions as it executes, and inspect its state. Knowledge of the program's state and past behavior, allows the compiler to perform speculative optimizations that improve performance. The intellectual merits of this research are to devise techniques for reasoning about the correctness of the transformations performed by just-in-time compilers. The project's broader significance and importance are its implications to industrial practice. The results of this research will be applicable to commercial just-in-time compilers for languages such as JavaScript and R.This project develops a general model of just-in-time compilation that subsumes deployed systems and allows systematic exploration of the design space of dynamic compilation techniques. The research questions that will be tackled in this work lie along two dimensions: Experimental -- explore the design space of dynamic compilation techniques and gain an understanding of trade-offs; Foundational -- formalize key ingredients of a dynamic compiler and develop techniques for reasoning about correctness in a modular fashion.

从Java到MATLAB的现代编程语言依赖于及时的编译技术来与C ++等计算机语言竞争性能。设定了即将到来的编译器与批处理编译器不同的是，他们可以在执行程序并检查其状态时观察程序的行动。了解程序的状态和过去行为，允许编译器执行提高性能的投机优化。这项研究的智力优点是设计技术来理解即将到来的编译器执行的转换的正确性。该项目对工业实践的影响更大。这项研究的结果将适用于JavaScript和R.R.等语言的商业即时编译器，该项目开发了一个即时编译的通用模型，该模型涵盖了已部署的系统，并允许系统地探索动态编译技术的设计空间。这项工作将解决的研究问题沿两个维度：实验 - 探索动态汇编技术的设计空间并了解权衡；基础 - 形式化动态编译器的关键要素，并开发以模块化方式推理正确性的技术。

项目成果

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

Contextual dispatch for function specialization

函数专业化的上下文调度

• DOI: 10.1145/3428288
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Flückiger, Olivier;Chari, Guido;Yee, Ming-Ho;Ječmen, Jan;Hain, Jakob;Vitek, Jan
• 通讯作者: Vitek, Jan

World age in Julia: optimizing method dispatch in the presence of eval

Julia 的世界时代：在 eval 存在的情况下优化方法调度

• DOI: 10.1145/3428275
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Belyakova, Julia;Chung, Benjamin;Gelinas, Jack;Nash, Jameson;Tate, Ross;Vitek, Jan
• 通讯作者: Vitek, Jan