一句话：提出显式化去优化同步点与推测假设的 JIT 中间表示，并在证明助手中验证若干推测优化。
动态语言的即时（JIT）编译器常基于可能在运行时失效的假设生成代码，以此针对常见情形特化程序、规避冷路径开销，但这类软件推测必须能在假设失败时进行去优化。本文提出一个模型化的 JIT 编译器，其核心是一个中间表示：它显式地刻画了用于去优化的同步点以及编译器推测所依赖的假设。基于该表示，作者给出若干可借助推测生成更优代码的常见编译器优化，并在证明助手中机器化地证明了这些优化的正确性。尽管工作尚未覆盖原生代码生成的验证，但论文展示了如何将已验证的优化嵌入端到端流程，从而获得显著的性能加速。
Just-in-time compilers for dynamic languages routinely generate code under assumptions that may be invalidated at run-time, this allows for specialization of program code to the common case in order to avoid unnecessary overheads due to uncommon cases. This form of software speculation requires support for deoptimization when some of the assumptions fail to hold. This paper presents a model just-in-time compiler with an intermediate representation that explicits the synchronization points used for deoptimization and the assumptions made by the compiler's speculation. We also present several common compiler optimizations that can leverage speculation to generate improved code. The optimizations are proved correct with the help of a proof assistant. While our work stops short of proving native code generation, we demonstrate how one could use the verified optimization to obtain significant speed ups in an end-to-end setting.
@article{paperbot1179,
title = {Formally verified speculation and deoptimization in a JIT compiler},
author = {Aurèle Barrière and Sandrine Blazy and Olivier Flückiger and David Pichardie and Jan Vitek},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434327}
}