We present TurboTV, a translation validator for the JavaScript (JS) just-in-time (JIT) compiler of Chromium. 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 that checks whether a specific compilation is semantically correct. We formally define the semantics of IR of TurboFan (JIT compiler of Chromium) and its SMT encoding. Furthermore, we propose two novel techniques to effectively apply translation validation to TurboFan. First, we design a staged strategy by carefully assuming that JS does not have undefined behaviors. This allows us to decompose the whole correctness checking into simpler ones. Second, we propose a generation-based strategy for translation validation of JIT compilers. Due to its dynamic nature, it is hard to apply translation validation in a traditional way. Thus, we generate a large program corpus curated to cover diverse optimization passes and validate their compilation. We evaluate TurboTV on various sets of JS programs and demonstrate the effectiveness of our approach.
이 논문은 자바스크립트 JIT (Just-In-Time) 컴파일러에 대한 번역 검산을 주제로 한다. 자바스크립트 엔 진은 여러 소프트웨어 시스템에서 중요한 부분이 되었지만, JIT 컴파일러의 도입 이후로 그들의 정확성을 보장하는 것은 매우 어려워졌다. 우리는 번역 검산과 만족 가능성 이론을 활용하여 이를 해결하고자 하였다. 이 논문에서는 Chromium의 JIT 컴파일러인 TurboFan 중간 언어의 의미, 그리고 이를 SMT로 인코딩하여 컴파일의올바름을보이는방법을소개한다. 그리고여기에더해번역검산의효율성을높일수있는두 기법도 제안한다. 첫째는 단계적 검산이다. 언어에 정의되지 않은 동작이 없다면 번역 검산은 보다 단순한 두 검산으로 분해될 수 있다. 우리는 자바스크립트 표준을 참고하여 이를 가정하였고, 검산을 단순화할 수 있었다. 둘째는 생성 기반 검산이다. JIT 컴파일러는 컴파일 결과가 실행 시점에 동적으로 결정되므로 전통적인 검산 전략을 택하기는 어렵다. 이 연구에서는 여러 최적화 경로를 탐색하는 프로그램을 생성하고, 이들을 검산하는 방법을 고안하였다. TurboTV는 이러한 아이디어를 구현한 번역 검산기이며, 우리는 다양한 자바스크립트 프로그램을 대상으로 이를 평가하여 그 효과성을 보였다.
