번역 검산 문서를 먼저 참고하면 본 문서의 내용을 이해하는 데 많은 도움이 될 것이다.
현재 자바스크립트 (JavaScript)는 전 세계 대부분의 웹을 구성하고 있는 주요한 프로그래밍 언어이다. 브라우저는 웹 페이지에 존재하는 자바스크립트 코드를 브라우저 내의 자바스크립트 엔진으로 실행하여 사용자에게 웹 환경을 제공한다. 자바스크립트 엔진은 자바스크립트 코드를 직접 바이트 코드 단위로 실행하는 인터프리터와, 성능 향상을 위해 자바스크립트를 기계 코드로 컴파일 하여 실행하는 JIT 컴파일러로 이루어져 있다. 대표적인 자바스크립트 엔진으로는 구글의 V8이 존재하며 해당 엔진은 크롬, Microsoft Edge, Node JS, Electron 등 다양한 곳에서 사용되고 있다. 자바스크립트 엔진의 JIT 컴파일러에 버그가 존재한다면 브라우저가 의도되지 않은 동작을 하여 많은 문제를 발생할 수 있다. 하지만 JIT 컴파일러 내부가 매우 복잡하고, 자주 변화하기 때문에 이를 검증하는 것은 매우 어려운 일이다. 따라서, 번역 검산이라는 기술을 통하여 V8 자바스크립트 엔진의 JIT 컴파일러인 TurboFan이 올바른 최적화를 수행하는지 검사하는 시스템인 TurboTV가 제안되었다. 본 문서에서는 TurboTV가 어떻게 컴파일러의 올바른 최적화를 검사하는지 설명하고자 한다.
다른 AOT 컴파일러 (gcc, LLVM, ...)와 달리, JIT 컴파일러는 프로그램의 런타임 중 컴파일을 진행한다. AOT 컴파일러를 위한 번역 검산은 컴파일 실행 단계에서 결합되여 사용이 가능하지만, JIT 컴파일러는 그 특성상 컴파일 시간에 더욱 민감하기 때문에 현장에서 사용되는 단계에서 번역 검산을 사용하기가 어렵다. 따라서 JIT 컴파일러를 위한 번역 검산은 컴파일러의 개발, 유지 보수 단계에서 해당 컴파일러가 올바른 최적화를 수행하는지 검사하기 위해 사용되어야 한다.
TurboFan이 자바스크립트 코드를 컴파일 할 때, 자바스크립트 코드를 TurboFan 중간 언어(TurboFan IR)로 번역하고, 중간 언어 상에서 최적화를 진행한다. 모든 최적화가 끝나면 중간 언어를 기계 코드로 최종적으로 번역하여 모든 과정이 끝마치게 된다. TurboTV의 목표는 TurboFan이 최적화 과정에서 프로그램의 의미가 보존되는지 검사하는 것이기 때문에, 각 최적화 단계마다 중간 언어의 의미가 동일한지(보존되는지) 번역 검산을 수행한다. 각 최적화 단계에서 TurboFan 중간 언어 프로그램을 엄밀하게 논리식으로 변환하고, 해당 프로그램의 의미가 최적화 과정에서 보존되었는지 Z3를 활용하여 확인한다.
정의되지 않은 행동(Undefined Behavior, UB)은 번역 검산에서 복잡성을 증가시키는 주요 원인이다. UB가 존재하는 언어에 대한 번역 검산에서는 두 프로그램의 의미간의 부분집합(포함) 관계를 계산해야 한다.
//최적화 전 프로그램
int foo(int i) {
int arr[1] = {0,};
return arr[i];
}//최적화 후 프로그램
int foo(int i) {
return 0;
}위의 최적화 전후 프로그램 예시에서 최적화 전의 프로그램은 i가 0이 아닐 때는 정의되지 않은 행동을 한다. 최적화 후의 프로그램은 i가 0이 아닐 때도 여전히 0을 반환한다. 이 때, 0 역시 정의되지 않은 행동의 부분 집합이기 때문에 위의 최적화는 올바른 최적화이다. 이처럼 정의되지 않은 행동은 번역 검산을 복잡하게 만든다.
TurboTV는 번역 검산에서 정의되지 않은 행동 검사와 의미 동일성 검사를 분리하여 단계적으로 수행하며 성능을 획기적으로 향상 시켰다. 자바스크립트 표준에는 정의되지 않은 행동이 존재하지 않기 때문에 자바스크립트 프로그램 역시 정의되지 않은 행동이 없다. 그렇기에 자바스크립트 코드가 번역된 TurboFan 중간 언어 역시 정의되지 않은 행동이 없어야 한다. 따라서 TurboTV의 단계적 번역 검산 과정은 다음과 같다.
- TurboFan 중간 언어 프로그램에서 정의되지 않은 행동이 존재하는지 검사한다.
- 정의되지 않은 행동이 존재하지 않다면 두 프로그램의 반환값이 동일한지 검사한다.
TurboFan 중간 언어 프로그램에 정의되지 않은 행동이 존재한다는 것은 TurboFan의 번역이 잘못 되었음을 의미하기에 그 자체로 버그이다. 만약 정의되지 않은 행동이 없다면 두 프로그램의 반환 값이 같다면 의미가 동일한 것이기 때문에 간단하게 두 프로그램의 의미 동일성을 판별할 수 있다. TurboTV는 이 단계적 번역 검산을 통하여 번역 검산 속도를 획기적으로 늘릴 수 있었다.
-
TurboTV와 퍼징의 결합: TurboTV는 퍼징과 결합하여 다양한 TurboFan의 최적화를 검사할 수 있다. 퍼저가 무작위 자바스크립트 코드를 생성하면, TurboTV는 TurboFan이 해당 코드를 컴파일하는 과정에서 최적화가 올바르게 일어나는지 검사할 수 있다. 기존 퍼저들은 프로그램의 충돌만으로 소프트웨어의 버그를 탐지하지만, TurboTV는 컴파일러의 잘못된 최적화같이 더 넓은 범위의 버그를 탐지할 수 있다.
-
교차 언어 번역 검산: TurboTV는 Alive2와 결합하여 LLVM에서 TurboFan으로 이어지는 두 컴파일러에 걸친 과정을 번역 검산할 수 있다. LLVM은 LLVM 중간 언어를 웹어셈블리(Wasm)으로, TurboFan은 Wasm을 TurboFan 중간 언어로 번역할 수 있다. 그렇기에 두 번역 검산기를 활용한다면 같은 언어에서 이루어지는 최적화 뿐만이 아니라 다른 언어(Wasm)로 번역하는 과정까지 번역 검산을 할 수 있게 된다. TurboTV는 교차 언어 번역 검산을 통해서 LLVM의 백엔드에서 실제 버그를 발견하였다.
TurboTV는 TurboFan의 올바른 최적화를 효과적으로 검사할 수 있고, 여러 방향으로 확장될 수 있음을 보이기 위해 실험들을 수행하였다.
- 최근 보고된 TurboFan 최적화 버그 8개 대상으로 오탐 없이 정확하게 버그를 탐지하였다.
- 576개의 TurboFan 유닛 테스트, 196,000개의 자바스크립트 코드 대상으로 전체의 90% 가 1초내로 번역 검산 되었으며, 1%의 오탐만이 발생됐다.
- 퍼저의 오류 검출기로 사용되었을 때, 총 7일 간의 퍼징에서 약 36%만의 부하를 보여주며 퍼징과 결합되어 사용될 수 있음을 보여 주었다.
- LLVM 유닛 테스트를 대상으로 교차 언어 번역 검산을 수행한 결과 LLVM Wasm 백엔드에서 1개의 실제 버그를 발견하였다.
본 문서에서는 V8 자바스크립트 엔진의 JIT 컴파일러인 TurboFan의 올바른 최적화 검사를 위해 번역 검산을 활용한 TurboTV를 소개하였다. TurboTV는 TurboFan 중간 언어를 엄밀하게 정의하고, 단계적 번역 검산을 통해 빠르고 정확하게 TurboFan의 특정 최적화가 올바른지 검사할 수 있다. 실제로 TurboTV는 무작위로 생성된 196,000개의 자바스크립트 코드 대상의 번역 검산에서 전체의 90%를 1초 이내에 완료하고 1%의 오탐만을 발생시키며 매우 우수한 성능을 보여주었다. 또한 퍼징과 결합하고, 다른 번역 검산기와 결합하여 더 넓은 대상을 번역 검산할 수 있는 확장성 역시 보여주었다. 실제로 Alive2와 결합된 교차 언어 번역 검산을 통해서 LLVM Wasm 백엔드에서 버그를 발견할 수 있었다. 더 자세한 내용은 TurboTV 홈페이지와 논문에서 확인할 수 있다.