Provably correct peephole optimizations with alive

Nuno P. Lopes, David Menendez, Santosh Nagarakatte, John Regehr

Research output: Contribution to journalArticlepeer-review

22 Scopus citations

Abstract

ompilers 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. This paper presents 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 that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures-but largely hides-the detailed semantics of three different kinds of undefined behavior in LLVM. We have translated more than 300 LLVM optimizations into Alive and, in the process, found that eight of them were wrong.

Original languageEnglish (US)
Pages (from-to)22-32
Number of pages11
JournalACM SIGPLAN Notices
Volume50
Issue number6
DOIs
StatePublished - Jun 2015

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Alive
  • Compiler Verification
  • Peephole Optimization

Fingerprint Dive into the research topics of 'Provably correct peephole optimizations with alive'. Together they form a unique fingerprint.

Cite this