一句话：在 Coq 中实现并验证带效应的 JIT，动态复用 CompCert 后端生成经证明的本机代码。
现代 JIT 编译器常混合解释执行与动态本机代码生成，并依赖栈上替换等机制；它们组件繁多且具有不纯效应，因此形式化验证一直较少。本文提出一个可在 Coq 中实现并形式验证的模型 JIT，能够动态生成经过验证的本机代码。针对 JIT 中无法直接写入 Coq 的不纯部分，作者提出一套证明方法学来界定、规约并推理这些效应。其核心思路是复用已有的本机代码生成证明，因而在动态编译中成功复用了 CompCert 及其正确性证明。原型可从 Coq 抽取并执行，为验证完整 JIT 提供了一条基于 CompCert 后端的可行路径。
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution, interpretation can be initially used. But after a while, JITs dynamically produce native code for parts of the program they execute often. Although some time is spent compiling dynamically, this mechanism makes for much faster times for the remaining of the program execution. Such compilers are complex pieces of software with various components, and greatly rely on a precise interplay between the different languages being executed, including on-stack-replacement. Traditional static compilers like CompCert have been mechanized in proof assistants, but JITs have been scarcely formalized so far, partly due to their impure nature and their numerous components. This work presents a model JIT with dynamic generation of native code, implemented and formally verified in Coq. Although some parts of a JIT cannot be written in Coq, we propose a proof methodology to delimit, specify and reason on the impure effects of a JIT. We argue that the daunting task of formally verifying a complete JIT should draw on existing proofs of native code generation. To this end, our work successfully reuses CompCert and its correctness proofs during dynamic compilation. Finally, our prototype can be extracted and executed.
@article{paperbot2054,
title = {Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler},
author = {Aurèle Barrière and Sandrine Blazy and David Pichardie},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571202}
}