Practical Verification of Peephole Optimizations with Alive.
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 provi...
| Publicado en: | Communications of the ACM Vol. 61; no. 2; pp. 84 - 92 |
|---|---|
| Autores principales: | , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Feb2018
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=127712858&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 127712858 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Feb2018 vid: 61 iid: 2 pid: 68 pub: Association for Computing Machinery artinfo: ui: 127712858 10.1145/3166064 ppf: 84 ppct: 8 formats: tig: atl: Practical Verification of Peephole Optimizations with Alive. aug: au: Lopes, Nuno P. Menendez, David Nagarakatte, Santosh Regehr, John affil: Microsoft Research, UK Rutgers University, USA University of Utah, USA su: Compilers (Computer programs) Debugging Computer programming Programming languages Coding theory sug: subj: Compilers (Computer programs) Debugging Computer programming Programming languages Coding theory 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2018 holdings: @attributes: islocal: N |
|---|