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或c++等计算机语言竞争的性能。即时编译器与批处理编译器的区别在于，它们可以在程序执行时观察程序的操作，并检查其状态。了解程序的状态和过去的行为，使编译器能够执行改进性能的推测性优化。这项研究的知识价值在于设计了一种技术，用于对即时编译器执行的转换的正确性进行推理。该项目更广泛的意义和重要性在于它对工业实践的影响。这项研究的结果将适用于商业的即时编译器，如JavaScript和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