Provably Correct Peephole Optimizations with Alive

Compilers should not miscompile. Our work addresses problems in developing peephole optimizations that perform local rewriting to improve the efficiency of LLVM code. These optimizations are individually difficult to get right, particularly in the presence of undefined behavior; taken together they represent a persistent source of bugs. In this talk, I’ll present Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code to be used directly by LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong. Alive is open-source and actively used by LLVM developers.

Joint work with David Menendez, Santosh Nagarakatte, and John Regehr.

http://web.ist.utl.pt/nuno.lopes/pubs/alive-pldi15.pdf

Nuno Lopes is currently a researcher at MSR Cambridge. He holds a PhD from the University of Lisbon, and has previously interned at MSR Redmond, Apple’s LLVM team, Max Planck Institute, and the Institute for Systems and Robotics Lisbon. Nuno’s research interests include software verification, compilers, and mixing the two.