PLDI 2016 – Proceedings

37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016), June 13–17, 2016, Santa Barbara, CA, USA

Frontmatter

Research Papers

Down to the Metal I

Into the Depths of C: Elaborating the De Facto Standards
Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N. M. Watson, and Peter Sewell
(University of Cambridge, UK)
Article: pldi16main-main2-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Living on the Edge: Rapid-Toggling Probes with Cross-Modification on x86
Buddhika Chamith, Bo Joel Svensson, Luke Dalessandro, and Ryan R. Newton
(Indiana University, USA)
Article: pldi16main-main21-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Polymorphic Type Inference for Machine Code
Matt Noonan, Alexey Loginov, and David Cok
(GrammaTech, USA)
Article: pldi16main-main241-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verification I

Data-Driven Precondition Inference with Learned Features
Saswat Padhi, Rahul Sharma, and Todd Millstein
(University of California at Los Angeles, USA; Stanford University, USA)
Article: pldi16main-main83-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Cartesian Hoare Logic for Verifying k-Safety Properties
Marcelo Sousa and Isil Dillig
(University of Oxford, UK; University of Texas at Austin, USA)
Article: pldi16main-main62-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verifying Bit-Manipulations of Floating-Point
Wonyeol Lee, Rahul Sharma, and Alex Aiken
(Stanford University, USA)
Article: pldi16main-main123-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Testing and Debugging

Coverage-Directed Differential Testing of JVM Implementations
Yuting Chen, Ting Su, Chengnian Sun, Zhendong Su, and Jianjun Zhao
(Shanghai Jiao Tong University, China; East China Normal University, China; University of California at Davis, USA; Kyushu University, Japan)
Article: pldi16main-main76-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Exposing Errors Related to Weak Memory in GPU Applications
Tyler Sorensen and Alastair F. Donaldson
(Imperial College London, UK)
Article: pldi16main-main196-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Lightweight Computation Tree Tracing for Lazy Functional Languages
Maarten Faddegon and Olaf Chitil
(University of Kent, UK)

aec-badge-pldi Article: pldi16main-main103-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Energy and Performance

Effective Padding of Multidimensional Arrays to Avoid Cache Conflict Misses
Changwan Hong, Wenlei Bao, Albert Cohen, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, J. Ramanujam, and P. Sadayappan
(Ohio State University, USA; Inria, France; ENS, France; Pacific Northwest National Laboratory, USA; Louisiana State University, USA)
Article: pldi16main-main269-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

GreenWeb: Language Extensions for Energy-Efficient Mobile Web Computing
Yuhao Zhu and Vijay Janapa Reddi
(University of Texas at Austin, USA)
Article: pldi16main-main5-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Input Responsiveness: Using Canary Inputs to Dynamically Steer Approximation
Michael A. Laurenzano, Parker Hill, Mehrzad Samadi, Scott Mahlke, Jason Mars, and Lingjia Tang
(University of Michigan, USA)
Article: pldi16main-main39-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

New Languages

Configuration Synthesis for Programmable Analog Devices with Arco
Sara Achour, Rahul Sarpeshkar, and Martin C. Rinard
(Massachusetts Institute of Technology, USA; Dartmouth College, USA)

aec-badge-pldi Article: pldi16main-main221-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

From Datalog to Flix: A Declarative Language for Fixed Points on Lattices
Magnus Madsen, Ming-Ho Yee, and Ondřej Lhoták
(University of Waterloo, Canada)
Article: pldi16main-main79-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Latte: A Language, Compiler, and Runtime for Elegant and Efficient Deep Neural Networks
Leonard Truong, Rajkishore Barik, Ehsan Totoni, Hai Liu, Chick Markley, Armando Fox, and Tatiana Shpeisman
(Intel Labs, USA; University of California at Berkeley, USA)
Article: pldi16main-main111-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Parsing and Compilation

On the Complexity and Performance of Parsing with Derivatives
Michael D. Adams, Celeste Hollenbeck, and Matthew Might
(University of Utah, USA)
Article: pldi16main-main317-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Down to the Metal II

Stratified Synthesis: Automatically Learning the x86-64 Instruction Set
Stefan Heule, Eric Schkufza, Rahul Sharma, and Alex Aiken
(Stanford University, USA; VMware, USA)
Article: pldi16main-main260-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Remix: Online Detection and Repair of Cache Contention for the JVM
Ariel Eizenberg, Shiliang Hu, Gilles Pokam, and Joseph Devietti
(University of Pennsylvania, USA; Intel, USA)

aec-badge-pldi Article: pldi16main-main47-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Statistical Similarity of Binaries
Yaniv David, Nimrod Partush, and Eran Yahav
(Technion, Israel)
Article: pldi16main-main297-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Types I

Accepting Blame for Safe Tunneled Exceptions
Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers
(Cornell University, USA; TU Darmstadt, Germany; Massachusetts Institute of Technology, USA)
Article: pldi16main-main33-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Occurrence Typing Modulo Theories
Andrew M. Kent, David Kempe, and Sam Tobin-Hochstadt
(Indiana University, USA)

aec-badge-pldi Article: pldi16main-main56-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala
(University of California at San Diego, USA)

aec-badge-pldi Article: pldi16main-main161-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Synthesis I

MapReduce Program Synthesis
Calvin Smith and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Article: pldi16main-main91-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Programmatic and Direct Manipulation, Together at Last
Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers
(University of Chicago, USA)

aec-badge-pldi Article: pldi16main-main95-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Fast Synthesis of Fast Collections
Calvin Loncaric, Emina Torlak, and Michael D. Ernst
(University of Washington, USA)

aec-badge-pldi Article: pldi16main-main261-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Software-Defined Networking

Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Černý
(University of Colorado at Boulder, USA; Cornell University, USA)

aec-badge-pldi Article: pldi16main-main80-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Temporal NetKAT
Ryan Beckett, Michael Greenberg, and David Walker
(Princeton University, USA; Pomona College, USA)

aec-badge-pldi Article: pldi16main-main132-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

SDNRacer: Concurrency Analysis for Software-Defined Networks
Ahmed El-Hassany, Jeremie Miserez, Pavol Bielik, Laurent Vanbever, and Martin Vechev
(ETH Zurich, Switzerland)

aec-badge-pldi Article: pldi16main-main274-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verifying Systems

Rehearsal: A Configuration Verification Tool for Puppet
Rian Shambaugh, Aaron Weiss, and Arjun Guha
(University of Massachusetts at Amherst, USA)

aec-badge-pldi Article: pldi16main-main19-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu
(Yale University, USA)
Article: pldi16main-main86-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verified Peephole Optimizations for CompCert
Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman
(University of Washington, USA)
Article: pldi16main-main150-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Types II

Just-in-Time Static Type Checking for Dynamic Languages
Brianna M. Ren and Jeffrey S. Foster
(University of Maryland at College Park, USA)

aec-badge-pldi Article: pldi16main-main306-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Types from Data: Making Structured Data First-Class Citizens in F#
Tomas Petricek, Gustavo Guerra, and Don Syme
(University of Cambridge, UK; Microsoft, UK; Microsoft Research, UK)
Article: pldi16main-main213-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Automatically Learning Shape Specifications
He Zhu, Gustavo Petri, and Suresh Jagannathan
(Purdue University, USA; University of Paris Diderot, France)

aec-badge-pldi Article: pldi16main-main291-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Synthesis II

Synthesizing Transformations on Hierarchically Structured Data
Navid Yaghmazadeh, Christian Klinger, Isil Dillig, and Swarat Chaudhuri
(University of Texas at Austin, USA; University of Freiburg, Germany; Rice University, USA)
Article: pldi16main-main40-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Program Synthesis from Polymorphic Refinement Types
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)

aec-badge-pldi Article: pldi16main-main64-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Parallelism I

Higher-Order and Tuple-Based Massively-Parallel Prefix Sums
Sepideh Maleki, Annie Yang, and Martin Burtscher
(Texas State University, USA)

aec-badge-pldi Article: pldi16main-main42-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

A Distributed OpenCL Framework using Redundant Computation and Data Replication
Junghyun Kim, Gangwon Jo, Jaehoon Jung, Jungwon Kim, and Jaejin Lee
(Seoul National University, South Korea)
Article: pldi16main-main72-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Memory Management

Idle Time Garbage Collection Scheduling
Ulan Degenbaev, Jochen Eisinger, Manfred Ernst, Ross McIlroy, and Hannes Payer
(Google, Germany; Google, USA; Google, UK)

aec-badge-pldi Article: pldi16main-main114-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Assessing the Limits of Program-Specific Garbage Collection Performance
Nicholas Jacek, Meng-Chieh Chiu, Benjamin Marlin, and Eliot Moss
(University of Massachusetts at Amherst, USA)
Article: pldi16main-main246-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verification II

Cardinalities and Universal Quantifiers for Verifying Parameterized Systems
Klaus v. Gleissenthall, Nikolaj Bjørner, and Andrey Rybalchenko
(TU Munich, Germany; University of California at San Diego, USA; Microsoft Research, USA; Microsoft Research, UK)
Article: pldi16main-main319-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Ivy: Safety Verification by Interactive Generalization
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; Microsoft Research, USA; University of California at Berkeley, USA)

aec-badge-pldi Article: pldi16main-main228-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Security

Precise, Dynamic Information Flow for Database-Backed Applications
Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, and Stephen Chong
(Carnegie Mellon University, USA; Harvard Medical School, USA; Dropbox, USA; San Jose State University, USA; Massachusetts Institute of Technology, USA; University of California at Santa Cruz, USA; Harvard University, USA)

aec-badge-pldi Article: pldi16main-main82-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

End-to-End Verification of Information-Flow Security for C and Assembly Programs
David Costanzo, Zhong Shao, and Ronghui Gu
(Yale University, USA)

aec-badge-pldi Article: pldi16main-main84-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

A Design and Verification Methodology for Secure Isolated Regions
Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram Rajamani, Sanjit A. Seshia, and Kapil Vaswani
(University of California at Berkeley, USA; Microsoft Research, UK; Microsoft Research, India)

aec-badge-pldi Article: pldi16main-main168-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Parallelism II

Transactional Data Structure Libraries
Alexander Spiegelman, Guy Golan-Gueta, and Idit Keidar
(Technion, Israel; Yahoo Research, Israel)
Article: pldi16main-main167-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

FlexVec: Auto-Vectorization for Irregular Loops
Sara S. Baghsorkhi, Nalini Vasudevan, and Youfeng Wu
(Intel, USA; Google, USA)
Article: pldi16main-main162-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi:

Verified Lifting of Stencil Computations
Shoaib Kamil, Alvin Cheung, Shachar Itzhaky, and Armando Solar-Lezama
(Adobe, USA; University of Washington, USA; Massachusetts Institute of Technology, USA)
Article: pldi16main-main227-p (type: Full Paper (15 pages all inclusive, plus up to 2 pages to buy)) doi: