Mon 15 Jun 2015 10:05 - 10:30 at PLDI Main BLUE (Portland 254-255) - Distinguished Papers Chair(s): Steve Blackburn

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

Mon 15 Jun

pldi2015-papers
09:00 - 11:00: Research Papers - Distinguished Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Steve BlackburnAustralian National University
pldi2015-papers143435160000009:00 - 09:15
Day opening
Steve BlackburnAustralian National University , David GroveIBM Research
pldi2015-papers143435250000009:15 - 09:40
Talk
Pavel PanchekhaUniversity of Washington, Alex Sanchez-SternUniversity of Washington, James R. WilcoxUniversity of Washington, Zachary Tatlock
Media Attached
pldi2015-papers143435400000009:40 - 10:05
Talk
Danfeng ZhangCornell University, Andrew Myers, Dimitrios VytiniotisMicrosoft Research, Cambridge, Simon Peyton JonesMicrosoft Research, Cambridge
Media Attached
pldi2015-papers143435550000010:05 - 10:30
Talk
Nuno P. LopesMicrosoft Research, David MenendezRutgers University, Santosh NagarakatteRutgers University, John RegehrUniversity of Utah
Media Attached
pldi2015-papers143435700000010:30 - 10:50
Talk