Powered by
Conference Publishing Consulting

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

PLDI 2015 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Welcome from the PLDI Chairs
Message from the Artifact Evaluation Committee Chairs
PLDI 2015 Organization
Sponsors and Supporters

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 ORCID logo
(University of Washington, USA)
Publisher's Version aec-badge-pldi
Diagnosing Type Errors with Class
Danfeng Zhang, Andrew C. Myers ORCID logo, Dimitrios Vytiniotis, and Simon Peyton-Jones
(Cornell University, USA; Microsoft Research, UK)
Publisher's Version
Provably Correct Peephole Optimizations with Alive
Nuno P. Lopes, David Menendez, Santosh Nagarakatte ORCID logo, and John Regehr ORCID logo
(Microsoft Research, UK; Rutgers University, USA; University of Utah, USA)
Publisher's Version Video

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

Algorithmic Debugging of Real-World Haskell Programs: Deriving Dependencies from the Cost Centre Stack
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)
Publisher's Version Video aec-badge-pldi
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)
Publisher's Version
Light: Replay via Tightly Bounded Recording
Peng Liu, Xiangyu ZhangORCID logo, Omer Tripp, and Yunhui Zheng
(Purdue University, USA; IBM Research, USA)
Publisher's Version
Many-Core Compiler Fuzzing
Christopher Lidbury, Andrei Lascu, Nathan Chong, and Alastair F. Donaldson
(Imperial College London, UK; University College London, UK)
Publisher's Version aec-badge-pldi

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

Mechanized Verification of Fine-Grained Concurrent Programs
Ilya Sergey, Aleksandar Nanevski ORCID logo, and Anindya Banerjee ORCID logo
(IMDEA Software Institute, Spain)
Publisher's Version Video Info aec-badge-pldi
Verification of Producer-Consumer Synchronization in GPU Programs
Rahul Sharma, Michael Bauer, and Alex AikenORCID logo
(Stanford University, USA; NVIDIA Research, USA)
Publisher's Version Video Info aec-badge-pldi
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)
Publisher's Version Video aec-badge-pldi
Verifying Read-Copy-Update in a Logic for Weak Memory
Joseph Tassarotti, Derek DreyerORCID logo, and Viktor VafeiadisORCID logo
(Carnegie Mellon University, USA; MPI-SWS, Germany)
Publisher's Version

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)
Publisher's Version Info
Optimizing Off-Chip Accesses in Multicores
Wei Ding, Xulong Tang, Mahmut Kandemir, Yuanrui Zhang, and Emre Kultursay
(Pennsylvania State University, USA; Intel, USA)
Publisher's Version
Improving Compiler Scalability: Optimizing Large Programs at Small Price
Sanyam Mehta and Pen-Chung Yew
(University of Minnesota, USA)
Publisher's Version

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)
Publisher's Version

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

Asynchronous Programming, Analysis and Testing with State Machines
Pantazis Deligiannis, Alastair F. DonaldsonORCID logo, Jeroen Ketema, Akash Lal, and Paul Thomson
(Imperial College London, UK; Microsoft Research, India)
Publisher's Version aec-badge-pldi
Stateless Model Checking Concurrent Programs with Maximal Causality Reduction
Jeff Huang
(Texas A&M University, USA)
Publisher's Version Video Info
Synthesizing Racy Tests
Malavika Samak, Murali Krishna Ramanathan, and Suresh Jagannathan ORCID logo
(Indian Institute of Science, India; Purdue University, USA)
Publisher's Version aec-badge-pldi
The Push/Pull Model of Transactions
Eric Koskinen and Matthew Parkinson ORCID logo
(IBM Research, USA; Microsoft Research, UK)
Publisher's Version

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 FosterORCID logo
(University of Colorado at Boulder, USA; Cornell University, USA)
Publisher's Version Video aec-badge-pldi
Efficient Synthesis of Probabilistic Programs
Aditya V. Nori, Sherjil Ozair, Sriram K. Rajamani, and Deepak Vijaykeerthy
(Microsoft Research, India; IIT Delhi, India)
Publisher's Version
FlashRelate: Extracting Relational Data from Semi-structured Spreadsheets Using Examples
Daniel W. Barowy, Sumit GulwaniORCID logo, Ted Hart, and Benjamin Zorn
(University of Massachusetts at Amherst, USA; Microsoft Research, USA)
Publisher's Version aec-badge-pldi
Synthesizing Data Structure Transformations from Input-Output Examples
John K. Feser, Swarat Chaudhuri, and Isil Dillig ORCID logo
(Rice University, USA; University of Texas at Austin, USA)
Publisher's Version

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

Composing Concurrency Control
Ofri Ziv, Alex AikenORCID logo, Guy Golan-Gueta, G. Ramalingam, and Mooly Sagiv
(Tel Aviv University, Israel; Stanford University, USA; Microsoft Research, India)
Publisher's Version Video
Dynamic Partial Order Reduction for Relaxed Memory Models
Naling Zhang, Markus Kusano, and Chao Wang
(Virginia Tech, USA)
Publisher's Version Video
Monitoring Refinement via Symbolic Reasoning
Michael Emmi, Constantin Enea, and Jad Hamza
(IMDEA Software Institute, Spain; University of Paris Diderot, France)
Publisher's Version aec-badge-pldi
Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications
Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross TateORCID logo
(Cornell University, USA)
Publisher's Version Info aec-badge-pldi

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)
Publisher's Version
Exploring and Enforcing Security Guarantees via Program Dependence Graphs
Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong ORCID logo
(Harvard University, USA; MIT Lincoln Laboratory, USA)
Publisher's Version
Making Numerical Program Analysis Fast
Gagandeep Singh, Markus Püschel, and Martin VechevORCID logo
(ETH Zurich, Switzerland)
Publisher's Version Video Info aec-badge-pldi
Tree Dependence Analysis
Yusheng Weijiang, Shruthi Balakrishna, Jianqiao Liu, and Milind KulkarniORCID logo
(Purdue University, USA)
Publisher's Version aec-badge-pldi

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 ORCID logo, William Mansky, Dmitri Garbuzov, Steve ZdancewicORCID logo, and Viktor VafeiadisORCID logo
(Seoul National University, South Korea; University of Pennsylvania, USA; MPI-SWS, Germany)
Publisher's Version Video Info aec-badge-pldi
Defining the Undefinedness of C
Chris Hathhorn, Chucky Ellison, and Grigore Roşu ORCID logo
(University of Missouri, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version
KJS: A Complete Formal Semantics of JavaScript
Daejun Park, Andrei Stefănescu, and Grigore Roşu ORCID logo
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version aec-badge-pldi
Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock ORCID logo, Xi Wang, Michael D. Ernst, and Thomas Anderson
(University of Washington, USA)
Publisher's Version aec-badge-pldi

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

Static Detection of Asymptotic Performance Bugs in Collection Traversals
Oswaldo Olivo, Isil Dillig ORCID logo, and Calvin Lin
(University of Texas at Austin, USA)
Publisher's Version
Autotuning Algorithmic Choice for Input Sensitivity
Yufei Ding, Jason Ansel, Kalyan Veeramachaneni, Xipeng ShenORCID logo, Una-May O’Reilly ORCID logo, and Saman Amarasinghe ORCID logo
(North Carolina State University, USA; Massachusetts Institute of Technology, USA)
Publisher's Version
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 ORCID logo
(Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe, USA; Google, USA)
Publisher's Version Info
Profile-Guided Meta-Programming
William J. Bowman, Swaha Miller, Vincent St-Amour, and R. Kent Dybvig
(Northeastern University, USA; Cisco Systems, USA)
Publisher's Version

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 ORCID logo
(University of Cambridge, UK; Purdue University, USA)
Publisher's Version Video Info aec-badge-pldi
Blame and Coercion: Together Again for the First Time
Jeremy Siek, Peter ThiemannORCID logo, and Philip Wadler ORCID logo
(Indiana University, USA; University of Freiburg, Germany; University of Edinburgh, UK)
Publisher's Version
Lightweight, Flexible Object-Oriented Generics
Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, and Andrew C. Myers ORCID logo
(Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA)
Publisher's Version aec-badge-pldi
Relatively Complete Counterexamples for Higher-Order Programs
Phúc C. Nguyễn and David Van HornORCID logo
(University of Maryland, USA)
Publisher's Version aec-badge-pldi

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

Automatic Induction Proofs of Data-Structures in Imperative Programs
Duc-Hiep Chu, Joxan JaffarORCID logo, and Minh-Thai Trinh
(National University of Singapore, Singapore)
Publisher's Version
Compositional Certified Resource Bounds
Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao ORCID logo
(Yale University, USA)
Publisher's Version Video Info aec-badge-pldi
Peer-to-Peer Affine Commitment using Bitcoin
Karl Crary and Michael J. Sullivan
(Carnegie Mellon University, USA)
Publisher's Version
Termination and Non-termination Specification Inference
Ton Chanh Le, Shengchao Qin, and Wei-Ngan ChinORCID logo
(National University of Singapore, Singapore; Teesside University, UK; Shenzhen University, China)
Publisher's Version Video Info aec-badge-pldi

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

Celebrating Diversity: A Mixture of Experts Approach for Runtime Mapping in Dynamic Environments
Murali Krishna Emani and Michael O'Boyle ORCID logo
(University of Edinburgh, UK)
Publisher's Version
Efficient Execution of Recursive Programs on Commodity Vector Hardware
Bin Ren, Youngjoon Jo, Sriram Krishnamoorthy, Kunal Agrawal, and Milind KulkarniORCID logo
(Pacific Northwest National Laboratory, USA; Purdue University, USA; Washington University at St. Louis, USA)
Publisher's Version aec-badge-pldi
Loop and Data Transformations for Sparse Matrix Code
Anand Venkat, Mary Hall ORCID logo, and Michelle Strout
(University of Utah, USA; Colorado State University, USA)
Publisher's Version
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)
Publisher's Version

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)
Publisher's Version Info aec-badge-pldi
Finding Counterexamples from Parsing Conflicts
Chinawat Isradisaikul and Andrew C. Myers ORCID logo
(Cornell University, USA)
Publisher's Version Video Info
Interactive Parser Synthesis by Example
Alan Leung, John Sarracino, and Sorin LernerORCID logo
(University of California at San Diego, USA)
Publisher's Version aec-badge-pldi
A Simpler, Safer Programming and Execution Model for Intermittent Systems
Brandon Lucia and Benjamin Ransford
(Carnegie Mellon University, USA; University of Washington, USA)
Publisher's Version

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)
Publisher's Version Video aec-badge-pldi
Synthesis of Machine Code from Semantics
Venkatesh Srinivasan and Thomas RepsORCID logo
(University of Wisconsin-Madison, USA; GrammaTech, USA)
Publisher's Version
Synthesis of Ranking Functions using Extremal Counterexamples
Laure Gonnord ORCID logo, David Monniaux, and Gabriel Radanne
(Claude Bernard University Lyon 1, France; LIP, France; University of Grenoble, France; VERIMAG, France; University of Paris Diderot, France)
Publisher's Version
Type-and-Example-Directed Program Synthesis
Peter-Michael Osera and Steve ZdancewicORCID logo
(University of Pennsylvania, USA)
Publisher's Version aec-badge-pldi

proc time: 13.6