Practical verification of peephole optimizations with alive

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

doi:https://doi.org/10.1145/3166064

Practical verification of peephole optimizations with alive

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

School of Arts and Sciences, Computer Science

Rutgers, The State University

Research output: Contribution to journal › Article › peer-review

7 Scopus citations

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.

Original language	American English
Pages (from-to)	84-91
Number of pages	8
Journal	Communications of the ACM
Volume	61
Issue number	2
DOIs	https://doi.org/10.1145/3166064
State	Published - Feb 2018

ASJC Scopus subject areas

Computer Science(all)

Access to Document

https://doi.org/10.1145/3166064

Cite this

@article{3027a98b48f1430c87b5330b62e00af0,

title = "Practical verification of peephole optimizations with alive",

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.",

author = "Lopes, {Nuno P.} and David Menendez and Santosh Nagarakatte and John Regehr",

note = "Publisher Copyright: {\textcopyright} 2018 ACM.",

year = "2018",

month = feb,

doi = "https://doi.org/10.1145/3166064",

language = "American English",

volume = "61",

pages = "84--91",

journal = "Communications of the ACM",

issn = "0001-0782",

publisher = "Association for Computing Machinery (ACM)",

number = "2",

}

TY - JOUR

T1 - Practical verification of peephole optimizations with alive

AU - Lopes, Nuno P.

AU - Menendez, David

AU - Nagarakatte, Santosh

AU - Regehr, John

PY - 2018/2

Y1 - 2018/2

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85041467987&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85041467987&partnerID=8YFLogxK

U2 - https://doi.org/10.1145/3166064

DO - https://doi.org/10.1145/3166064

M3 - Article

SN - 0001-0782

VL - 61

SP - 84

EP - 91

JO - Communications of the ACM

JF - Communications of the ACM

IS - 2

ER -

Practical verification of peephole optimizations with alive

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this