一句话：提出 TurboTV：基于 SMT 的分阶段翻译验证器，验证 V8 TurboFan JIT 编译的正确性并发现 LLVM 新误编译。
JS 引擎已成为众多软件系统的关键组成部分，而 JIT 编译的广泛采用使得引擎正确性难以保障。本文提出 TurboTV，一个面向 V8 中 JavaScript JIT 编译器 TurboFan 的翻译验证器（translation validation），其核心思想是用 SMT 编码形式化定义 TurboFan IR 的语义，从而检查某次具体编译是否语义正确。为提升验证效率，作者针对 JS JIT 编译器设计了分阶段验证策略，把整体正确性检查分解为若干更简单的子问题；同时利用 fuzzing 生成大量 JS 函数以触发 TurboFan 的各类优化遍并对其编译结果进行验证。作者在多种 JS 与 LLVM 程序集上评估：TurboTV 以较低误报率有效验证了大量 TurboFan 编译，发现了一个新的 LLVM 误编译；此外还展示了跨语言翻译验证能力——与现成的 LLVM 翻译验证工具协作，验证从 LLVM IR 到 TurboFan IR 的翻译链。
We present TurboTV, a translation validator for the JavaScript (JS) just-in-time (JIT) compiler of V8. While JS engines have become a crucial part of various software systems, their emerging adaption of JIT compilation makes it increasingly challenging to ensure their correctness. We tackle this problem with an SMT-based translation validation (TV) that checks whether a specific compilation is semantically correct. We formally define the semantics of IR of TurboFan (JIT compiler of V8) as SMT encoding. For efficient validation, we design a staged strategy for JS JIT compilers. This allows us to decompose the whole correctness checking into simpler ones. Furthermore, we utilize fuzzing to achieve practical TV. We generate a large number of JS functions using a fuzzer to trigger various optimization passes of TurboFan and validate their compilation using TurboTV. Lastly, we demonstrate that TurboTV can also be used for cross-language TV. We show that TurboTV can validate the translation chain from LLVM IR to TurboFan IR, collaborating with an off-the-shelf TV tool for LLVM. We evaluated TurboTV on various sets of JS and LLVM programs. TurboTV effectively validated a large number of compilations of TurboFan with a low false positive rate and discovered a new miscompilation in LLVM.
@inproceedings{paperbot11376,
title = {Translation Validation for JIT Compiler in the V8 JavaScript Engine},
author = {Seungwan Kwon and Jaeseong Kwon and Wooseok Kang and Juneyoung Lee and Kihong Heo},
booktitle = {ICSE},
year = {2024},
doi = {10.1145/3597503.3639189}
}