Formally verified speculation and deoptimization in a JIT compiler
Formally verified speculation and deoptimization in a JIT compiler
复制标题
DOI：
10.1145/3434327
复制
发表时间：
2021-01
影响因子：
--
通讯作者：
Aurèle Barrière;Sandrine Blazy;Aurèle Barrière;Sandrine Blazy;O. Flückiger;David Pichardie
中科院分区：
文献类型：
--
作者：
Aurèle Barrière;Sandrine Blazy;Aurèle Barrière;Sandrine Blazy;O. Flückiger;David Pichardie
动态语言的即时编译器通常在可能在运行时无效的假设下生成代码，这允许将程序代码专门化到常见情况，以避免由于不常见情况而产生的不必要的开销。这种形式的软件推测需要在某些假设不成立时支持去最优化。本文提出了一种实时编译器模型，该模型采用中间表示法，明确了用于反优化的同步点和编译器推测所作的假设。我们还提供了几个常见的编译器优化，它们可以利用推测来生成改进的代码。在证明助手的帮助下，这些优化被证明是正确的。虽然我们的工作还没有证明本机代码生成，但我们演示了如何使用经过验证的优化在端到端设置中获得显著的速度提升。
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.