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

Displayed time zone: Tijuana, Baja California change

09:00 - 11:00
Distinguished PapersResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Steve Blackburn Australian National University
09:00
15m
Day opening
Opening and Welcome
Research Papers
Steve Blackburn Australian National University , David Grove IBM Research
09:15
25m
Talk
Automatically Improving Accuracy for Floating Point Expressions
Research Papers
Pavel Panchekha University of Washington, Alex Sanchez-Stern University of Washington, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle
Media Attached
09:40
25m
Talk
Diagnosing Type Errors with Class
Research Papers
Danfeng Zhang Cornell University, Andrew Myers , Dimitrios Vytiniotis Microsoft Research, Cambridge, Simon Peyton Jones Microsoft Research, Cambridge
Media Attached
10:05
25m
Talk
Provably Correct Peephole Optimizations with Alive
Research Papers
Nuno P. Lopes Microsoft Research, David Menendez Rutgers University, Santosh Nagarakatte Rutgers University, John Regehr University of Utah
Pre-print Media Attached
10:30
20m
Talk
One Minute Madness
Research Papers