S-Space College of Engineering/Engineering Practice School (공과대학/대학원) Dept. of Computer Science and Engineering (컴퓨터공학부) Theses (Master's Degree_컴퓨터공학부)
Verified Translation Validation For Register Promotion in LLVM
검증된 번역 검산 기술을 이용한 LLVM 컴파일러의 Register Promotion 최적화 검산
- 공과대학 컴퓨터공학부
- Issue Date
- 서울대학교 대학원
- 학위논문 (석사)-- 서울대학교 대학원 : 공과대학 컴퓨터공학부, 2018. 2. 허충길.
- Mainstream C/C++ compilers usually focus on efficiency though reliability is also important as well for compilers. Thus they perform various optimizations for performance, but many bugs are found in GCC and LLVM by recent random testing tools.
To increase the reliability of mainstream compilers without sacrificing their performance, I propose a practical approach for verified compilation using a verified extensible relational Hoare-logic (ERHL) validator. As this approach performs translation validation which separates compilation and validation, it does not sacrifice any compilation performance. Also, I can finally succeed to validate translations or identify compiler bugs because I insert proof generation code for validation directly in the compiler.
As a litmus test to show the possibility of this approach, I successfully validate register promotion in the sroa pass in LLVM 3.7.1. Translation validation for register promotion has enough to show possibility of validating the whole optimization passes in LLVM as register promotion is one of the most performance critical passes in LLVM. This is because register promotion promotes memory locations to LLVM registers and converts corresponding load and store instructions into register read and write operations, and many LLVM optimization focus on optimizing register operations, most of which are introduced in register promotion. Moreover, some of those LLVM registers are transformed into CPU registers which are magnitude faster to access than memory locations.
I validated translation of register promotion for SPEC CPU2006 benchmarks, LLVM Nightly Test, and five C projects, with 7.1M lines of code in total. There are only 10 failures in validation results, but all of them are due to the compiler bug which I found during this work.