PLDI 2015 – Proceedings

36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), June 13–17, 2015, Portland, OR, USA

Frontmatter

Research Papers

Distinguished Papers
Mon, Jun 15, 09:00 - 11:00 (Chair: Steve Blackburn)

Automatically Improving Accuracy for Floating Point Expressions
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock
(University of Washington, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-61-p doi:

Diagnosing Type Errors with Class
Danfeng Zhang, Andrew C. Myers, Dimitrios Vytiniotis, and Simon Peyton-Jones
(Cornell University, USA; Microsoft Research, UK)
Article: pldi15main-mainpldi15-312-p doi:

Provably Correct Peephole Optimizations with Alive
Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr
(Microsoft Research, UK; Rutgers University, USA; University of Utah, USA)
Article: pldi15main-mainpldi15-74-p doi:

Correctness
Mon, Jun 15, 14:00 - 15:40 (Chair: Jens Palsberg)

Automatic Error Elimination by Horizontal Code Transfer across Multiple Applications
Stelios Sidiroglou-Douskos, Eric Lahtinen, Fan Long, and Martin Rinard
(Massachusetts Institute of Technology, USA)
Article: pldi15main-mainpldi15-186-p doi:

Light: Replay via Tightly Bounded Recording
Peng Liu, Xiangyu Zhang, Omer Tripp, and Yunhui Zheng
(Purdue University, USA; IBM Research, USA)
Article: pldi15main-mainpldi15-245-p doi:

Many-Core Compiler Fuzzing
Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson
(Imperial College London, UK; University College London, UK)

aec-badge-pldi Article: pldi15main-mainpldi15-181-p doi:

Verification
Mon, Jun 15, 14:00 - 15:40 (Chair: Nate Foster)

Verification of Producer-Consumer Synchronization in GPU Programs
Rahul Sharma, Michael Bauer, and Alex Aiken
(Stanford University, USA; NVIDIA Research, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-68-p doi:

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Peter Gammie, Antony L. Hosking, and Kai Engelhardt
(NICTA, Australia; Purdue University, USA; UNSW, Australia)

aec-badge-pldi Article: pldi15main-mainpldi15-279-p doi:

Verifying Read-Copy-Update in a Logic for Weak Memory
Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis
(Carnegie Mellon University, USA; MPI-SWS, Germany)
Article: pldi15main-mainpldi15-195-p doi:

Optimization
Mon, Jun 15, 16:00 - 17:15 (Chair: Michelle Mills Strout)

LaminarIR: Compile-Time Queues for Structured Streams
Yousun Ko, Bernd Burgstaller, and Bernhard Scholz
(Yonsei University, South Korea; University of Sydney, Australia)
Article: pldi15main-mainpldi15-197-p doi:

Optimizing Off-Chip Accesses in Multicores
Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay
(Pennsylvania State University, USA; Intel, USA)
Article: pldi15main-mainpldi15-188-p doi:

Improving Compiler Scalability: Optimizing Large Programs at Small Price
Sanyam Mehta and Pen-Chung Yew
(University of Minnesota, USA)
Article: pldi15main-mainpldi15-37-p doi:

TOPLAS
Mon, Jun 15, 17:15 - 17:40 (Chair: Michelle Mills Strout)

Verification of a Cryptographic Primitive: SHA-256 (Abstract)
Andrew W. Appel
(Princeton University, USA)
Article: pldi15main-toplaspldi15-1-p doi:

Concurrency I
Mon, Jun 15, 16:00 - 17:40 (Chair: Santosh Nagarakatte)

Asynchronous Programming, Analysis and Testing with State Machines
Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Akash Lal, and Paul Thomson
(Imperial College London, UK; Microsoft Research, India)

aec-badge-pldi Article: pldi15main-mainpldi15-205-p doi:

Synthesizing Racy Tests
Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan
(Indian Institute of Science, India; Purdue University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-231-p doi:

The Push/Pull Model of Transactions
Eric Koskinen and Matthew Parkinson
(IBM Research, USA; Microsoft Research, UK)
Article: pldi15main-mainpldi15-199-p doi:

Synthesis I
Tue, Jun 16, 09:15 - 10:55 (Chair: Kathleen Fisher)

Efficient Synthesis of Network Updates
Jedidiah McClurg, Hossein Hojjat, Pavol Černý, and Nate Foster
(University of Colorado at Boulder, USA; Cornell University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-142-p doi:

Efficient Synthesis of Probabilistic Programs
Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy
(Microsoft Research, India; IIT Delhi, India)
Article: pldi15main-mainpldi15-150-p doi:

FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples
Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn
(University of Massachusetts at Amherst, USA; Microsoft Research, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-9-p doi:

Synthesizing Data Structure Transformations from Input-Output Examples
John K. Feser, Swarat Chaudhuri, and Isil Dillig
(Rice University, USA; University of Texas at Austin, USA)
Article: pldi15main-mainpldi15-117-p doi:

Concurrency II
Tue, Jun 16, 09:15 - 10:55 (Chair: Suresh Jagannathan)

Composing Concurrency Control
Ofri Ziv, Alex Aiken, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv
(Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India)
Article: pldi15main-mainpldi15-102-p doi:

Dynamic Partial Order Reduction for Relaxed Memory Models
Naling Zhang, Markus Kusano, and Chao Wang
(Virginia Tech, USA)
Article: pldi15main-mainpldi15-51-p doi:

Monitoring Refinement via Symbolic Reasoning
Michael Emmi, Constantin Enea, and Jad Hamza
(IMDEA Software Institute, Spain; University of Paris Diderot, France)

aec-badge-pldi Article: pldi15main-mainpldi15-152-p doi:

Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications
Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate
(Cornell University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-79-p doi:

Analysis
Tue, Jun 16, 14:00 - 15:40 (Chair: Yannis Smaragdakis)

DAG Inlining: A Decision Procedure for Reachability-Modulo-Theories in Hierarchical Programs
Akash Lal and Shaz Qadeer
(Microsoft Research, India; Microsoft Research, USA)
Article: pldi15main-mainpldi15-182-p doi:

Exploring and Enforcing Security Guarantees via Program Dependence Graphs
Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong
(Harvard University, USA; MIT Lincoln Laboratory, USA)
Article: pldi15main-mainpldi15-58-p doi:

Making Numerical Program Analysis Fast
Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)

aec-badge-pldi Article: pldi15main-mainpldi15-236-p doi:

Tree Dependence Analysis
Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind Kulkarni
(Purdue University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-107-p doi:

Semantics I
Tue, Jun 16, 14:00 - 15:40 (Chair: Hans-J. Boehm)

A Formal C Memory Model Supporting Integer-Pointer Casts
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis
(Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany)

aec-badge-pldi Article: pldi15main-mainpldi15-267-p doi:

Defining the Undefinedness of C
Chris Hathhorn, Chucky Ellison, and Grigore Roşu
(University of Missouri, USA; University of Illinois at Urbana-Champaign, USA)
Article: pldi15main-mainpldi15-134-p doi:

KJS: A Complete Formal Semantics of JavaScript
Daejun Park, Andrei Stefănescu, and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-194-p doi:

Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson
(University of Washington, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-60-p doi:

Performance
Wed, Jun 17, 09:15 - 10:55 (Chair: Mary Hall)

Static Detection of Asymptotic Performance Bugs in Collection Traversals
Oswaldo Olivo, Isil Dillig, and Calvin Lin
(University of Texas at Austin, USA)
Article: pldi15main-mainpldi15-78-p doi:

Autotuning Algorithmic Choice for Input Sensitivity
Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng Shen, Una-May O’Reilly, and Saman Amarasinghe
(North Carolina State University, USA; Massachusetts Institute of Technology, USA)
Article: pldi15main-mainpldi15-100-p doi:

Helium: Lifting High-Performance Stencil Kernels from Stripped x86 Binaries to Halide DSL Code
Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA)
Article: pldi15main-mainpldi15-113-p doi:

Profile-Guided Meta-Programming
William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig
(Northeastern University, USA; Cisco Systems, USA)
Article: pldi15main-mainpldi15-193-p doi:

Semantics II
Wed, Jun 17, 09:15 - 10:55 (Chair: Robby Findler)

Declarative Programming over Eventually Consistent Data Stores
KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan
(University of Cambridge, UK; Purdue University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-143-p doi:

Blame and Coercion: Together Again for the First Time
Jeremy Siek, Peter Thiemann, and Philip Wadler
(Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK)
Article: pldi15main-mainpldi15-92-p doi:

Lightweight, Flexible Object-Oriented Generics
Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers
(Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-309-p doi:

Relatively Complete Counterexamples for Higher-Order Programs
Phúc C. Nguyễn and David Van Horn
(University of Maryland, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-103-p doi:

Logic
Wed, Jun 17, 14:00 - 15:40 (Chair: Madhusudan Parthasarathy)

Automatic Induction Proofs of Data-Structures in Imperative Programs
Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh
(National University of Singapore, Singapore)
Article: pldi15main-mainpldi15-155-p doi:

Compositional Certified Resource Bounds
Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao
(Yale University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-41-p doi:

Peer-to-Peer Affine Commitment using Bitcoin
Karl Crary and Michael J. Sullivan
(Carnegie Mellon University, USA)
Article: pldi15main-mainpldi15-227-p doi:

Termination and Non-termination Specification Inference
Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin
(National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China)

aec-badge-pldi Article: pldi15main-mainpldi15-196-p doi:

Parallelism
Wed, Jun 17, 14:00 - 15:40 (Chair: Sara Baghsorkhi)

Efficient Execution of Recursive Programs on Commodity Vector Hardware
Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind Kulkarni
(Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-252-p doi:

Loop and Data Transformations for Sparse Matrix Code
Anand Venkat, Mary Hall, and Michelle Strout
(University of Utah, USA; Colorado State University, USA)
Article: pldi15main-mainpldi15-249-p doi:

Synthesizing Parallel Graph Programs via Automated Planning
Dimitrios Prountzos, Roman Manevich, and Keshav Pingali
(University of Texas at Austin, USA; Ben-Gurion University of the Negev, Israel)
Article: pldi15main-mainpldi15-30-p doi:

Potpourri
Wed, Jun 17, 16:00 - 17:40 (Chair: Tiark Rompf)

Zero-Overhead Metaprogramming: Reflection and Metaobject Protocols Fast and without Compromises
Stefan Marr, Chris Seaton, and Stéphane Ducasse
(INRIA, France; Oracle Labs, USA; University of Manchester, UK)

aec-badge-pldi Article: pldi15main-mainpldi15-71-p doi:

Finding Counterexamples from Parsing Conflicts
Chinawat Isradisaikul and Andrew C. Myers
(Cornell University, USA)
Article: pldi15main-mainpldi15-66-p doi:

Interactive Parser Synthesis by Example
Alan Leung, John Sarracino, and Sorin Lerner
(University of California at San Diego, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-248-p doi:

A Simpler, Safer Programming and Execution Model for Intermittent Systems
Brandon Lucia and Benjamin Ransford
(Carnegie Mellon University, USA; University of Washington, USA)
Article: pldi15main-mainpldi15-130-p doi:

Synthesis II
Wed, Jun 17, 16:00 - 17:40 (Chair: Isil Dillig)

Concurrency Debugging with Differential Schedule Projections
Nuno Machado, Brandon Lucia, and Luís Rodrigues
(Universidade de Lisboa, Portugal; Carnegie Mellon University, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-109-p doi:

Synthesis of Machine Code from Semantics
Venkatesh Srinivasan and Thomas Reps
(University of Wisconsin-Madison, USA; GrammaTech, USA)
Article: pldi15main-mainpldi15-64-p doi:

Synthesis of Ranking Functions using Extremal Counterexamples
Laure Gonnord, David Monniaux, and Gabriel Radanne
(Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France)
Article: pldi15main-mainpldi15-115-p doi:

Type-and-Example-Directed Program Synthesis
Peter-Michael Osera and Steve Zdancewic
(University of Pennsylvania, USA)

aec-badge-pldi Article: pldi15main-mainpldi15-288-p doi:

PLDI 2015 – Proceedings

Frontmatter

Research Papers

Distinguished Papers Mon, Jun 15, 09:00 - 11:00 (Chair: Steve Blackburn)

Correctness Mon, Jun 15, 14:00 - 15:40 (Chair: Jens Palsberg)

Verification Mon, Jun 15, 14:00 - 15:40 (Chair: Nate Foster)

Optimization Mon, Jun 15, 16:00 - 17:15 (Chair: Michelle Mills Strout)

TOPLAS Mon, Jun 15, 17:15 - 17:40 (Chair: Michelle Mills Strout)

Concurrency I Mon, Jun 15, 16:00 - 17:40 (Chair: Santosh Nagarakatte)

Synthesis I Tue, Jun 16, 09:15 - 10:55 (Chair: Kathleen Fisher)

Concurrency II Tue, Jun 16, 09:15 - 10:55 (Chair: Suresh Jagannathan)

Analysis Tue, Jun 16, 14:00 - 15:40 (Chair: Yannis Smaragdakis)

Semantics I Tue, Jun 16, 14:00 - 15:40 (Chair: Hans-J. Boehm)

Performance Wed, Jun 17, 09:15 - 10:55 (Chair: Mary Hall)

Semantics II Wed, Jun 17, 09:15 - 10:55 (Chair: Robby Findler)

Logic Wed, Jun 17, 14:00 - 15:40 (Chair: Madhusudan Parthasarathy)

Parallelism Wed, Jun 17, 14:00 - 15:40 (Chair: Sara Baghsorkhi)

Potpourri Wed, Jun 17, 16:00 - 17:40 (Chair: Tiark Rompf)

Synthesis II Wed, Jun 17, 16:00 - 17:40 (Chair: Isil Dillig)