Practical Verification of Peephole Optimizations with Alive

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

Abstract:

Compilers should not miscompile. Peephole optimizations, which perform local rewriting of the input program to improve the efficiency of generated code, are a persistent source of compiler bugs. We created 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 the various kinds of undefined behavior. Alive has found numerous bugs in the LLVM compiler and is being used by LLVM developers.

Published:

N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr. Practical Verification of Peephole Optimizations with Alive. Communications of the ACM, 61(2):84-91, Feb. 2018.

Download:

Editor
PDF

Bibtex:

@article{alive-cacm18,
  title =	{Practical Verification of Peephole Optimizations with Alive},
  author =	{Nuno P. Lopes and David Menendez and Santosh Nagarakatte and John Regehr},
  journal =	{Communications of the ACM},
  volume =	{61},
  number =	{2},
  publisher =	{ACM},
  pages =	{84--91},
  doi =		{10.1145/3166064},
  month =	feb,
  year =	2018
}

Copyright notice:

<-- Return