Production compilers such as GCC and LLVM are large complex software systems, for which achieving a high level of reliability is hard. Although testing is an effective method for finding bugs, it alone cannot guarantee a high level of reliability. To provide a higher level of reliability, many approaches that examine compilers' internal logics have been proposed. However, none of them have been successfully applied to major optimizations of production compilers.
This paper presents Crellvm: a verified credible compilation framework for LLVM, which can be used as a systematic way of providing a high level of reliability for major optimizations in LLVM. Specifically, we augment an LLVM optimizer to generate translation results together with their correctness proofs, which can then be checked by a proof checker formally verified in Coq. As case studies, we applied our approach to two major optimizations of LLVM: register promotion mem2reg and global value numbering gvn, having found four new miscompilation bugs (two in each).
Fri 22 Jun
|14:00 - 14:25|
Brandon Bohrer, Yong Kiam TanCarnegie Mellon University, USA, Stefan MitschCarnegie Mellon University, USA, Magnus O. MyreenChalmers University of Technology, Sweden, André PlatzerCarnegie Mellon UniversityMedia Attached
|14:25 - 14:50|
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Youngju SongSeoul National University, Juneyoung LeeSeoul National University, Sanghoon ParkSeoul National University, South Korea, Mark Dongyeon ShinSeoul National University, South Korea, Yonghyun KimSeoul National University, South Korea, Sungkeun ChoSeoul National University, South Korea, Joonwon ChoiMassachusetts Institute of Technology, USA, Chung-Kil HurSeoul National University, Kwangkeun YiSeoul National UniversityMedia Attached
|14:50 - 15:15|
Ronghui GuColumbia University, Zhong ShaoYale University, Jieung KimYale University, USA, Xiongnan (Newman) WuYale University, Jérémie Koenig, Vilhelm SjöbergYale University, Hao ChenYale University, David CostanzoYale University, Tahina RamananandroMicrosoft Research, n.n.Media Attached
|15:15 - 15:40|
Marcelo TaubeTel Aviv University, Israel, Giuliano LosaUniversity of California at Los Angeles, USA, Kenneth L. McMillanMicrosoft Research, Oded PadonTel Aviv University, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university, James R. WilcoxUniversity of Washington, Doug WoosUniversity of WashingtonMedia Attached