PLDI 2019
40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019)
Powered by
Conference Publishing Consulting

40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019), June 22–26, 2019, Phoenix, AZ, USA

PLDI 2019 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Message from the Chairs
PLDI 2019 Organization
Sponsors

Concurrency I

Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur
(Cambridge University, UK; KAIST, South Korea; Seoul National University, South Korea)
Publisher's Version Article Search Artifacts Functional
Accelerating Sequential Consistency for Java with Speculative Compilation
Lun Liu, Todd Millstein, and Madanlal Musuvathi
(University of California at Los Angeles, USA; Microsoft Research, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Renaissance: Benchmarking Suite for Parallel Applications on the JVM
Aleksandar Prokopec, Andrea Rosà, David Leopoldseder, Gilles Duboscq, Petr Tůma, Martin Studener, Lubomír Bulej, Yudi Zheng, Alex Villazón, Doug Simon, Thomas Würthinger, and Walter Binder
(Oracle Labs, Switzerland; USI Lugano, Switzerland; JKU Linz, Austria; Charles University in Prague, Czechia; Universidad Privada Boliviana, Bolivia)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Language Design I

LoCal: A Language for Programs Operating on Serialized Data
Michael Vollmer, Chaitanya Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, and Ryan R. Newton
(Indiana University, USA; Purdue University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Scenic: A Language for Scenario Specification and Scene Generation
Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia
(University of California at Berkeley, USA)
Publisher's Version Article Search Info
Compiling KB-Sized Machine Learning Models to Tiny IoT Devices
Sridhar Gopinath, Nikhil Ghanathe, Vivek Seshadri, and Rahul Sharma
(Microsoft Research, India)
Publisher's Version Article Search

Concurrency II

Model Checking for Weakly Consistent Libraries
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Towards Certified Separate Compilation for Concurrent Programs
Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng
(University of Science and Technology of China, China; Nanjing University, China)
Publisher's Version Article Search Artifacts Functional
Robustness against Release/Acquire Semantics
Ori Lahav and Roy Margalit
(Tel Aviv University, Israel)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Language Design II

CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madanlal Musuvathi, and Todd Mytkowicz
(University of Texas at Austin, USA; Microsoft Research, USA)
Publisher's Version Article Search
Usuba: High-Throughput and Constant-Time Ciphers, by Construction
Darius Mercadier and Pierre-Évariste Dagand
(Sorbonne University, France; CNRS, France; Inria, France; LIP6, France)
Publisher's Version Article Search Artifacts Available Artifacts Functional
FaCT: A DSL for Timing-Sensitive Computation
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; Stanford University, USA; Inria, France; MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional

Probabilistic Programming

Scalable Verification of Probabilistic Networks
Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva
(Cornell University, USA; Carnegie Mellon University, USA; University of Wisconsin-Madison, USA; University College London, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Cost Analysis of Nondeterministic Probabilistic Programs
Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi
(Shanghai Jiao Tong University, China; East China Normal University, China; IST Austria, Austria)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Gen: A General-Purpose Probabilistic Programming System with Programmable Inference
Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search
Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs
Jieyuan Zhang and Jingling Xue
(UNSW, Australia)
Publisher's Version Article Search Artifacts Functional

Synthesis

Resource-Guided Program Synthesis
Tristan Knoth, Di Wang, Nadia Polikarpova, and Jan Hoffmann
(University of California at San Diego, USA; Carnegie Mellon University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Using Active Learning to Synthesize Models of Applications That Access Databases
Jiasi Shen and Martin C. Rinard
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search
Synthesizing Database Programs for Schema Refactoring
Yuepeng Wang, James Dong, Rushi Shah, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version Article Search
Synthesis and Machine Learning for Heterogeneous Extraction
Arun Iyer, Manohar Jonnalagedda, Suresh Parthasarathy, Arjun Radhakrishna, and Sriram K. Rajamani
(Microsoft Research, India; Inpher, Switzerland; Microsoft, USA)
Publisher's Version Article Search

Memory Management

AutoPersist: An Easy-To-Use Java NVM Framework Based on Reachability
Thomas Shull, Jian Huang, and Josep Torrellas
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search
Mesh: Compacting Memory Management for C/C++ Applications
Bobby Powers, David Tench, Emery D. Berger, and Andrew McGregor
(University of Massachusetts at Amherst, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Panthera: Holistic Memory Management for Big Data Processing over Hybrid Memories
Chenxi Wang, Huimin Cui, Ting Cao, John Zigman, Haris Volos, Onur Mutlu, Fang Lv, Xiaobing Feng, and Guoqing Harry Xu
(University of California at Los Angeles, USA; Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Microsoft Research, USA; University of Sydney, Australia; Google, USA; ETH Zurich, Switzerland)
Publisher's Version Article Search

Parsing

Lightweight Multi-Language Syntax Transformation with Parser Parser Combinators
Rijnard van Tonder and Claire Le Goues
(Carnegie Mellon University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
A Typed, Algebraic Approach to Parsing
Neelakantan R. Krishnaswami and Jeremy Yallop
(University of Cambridge, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Genie: A Generator of Natural Language Semantic Parsers for Virtual Assistant Commands
Giovanni Campagna, Silei Xu, Mehrad Moradshahi, Richard Socher, and Monica S. Lam
(Stanford University, USA; Salesforce, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Bug Finding and Testing I

Lazy Counterfactual Symbolic Execution
William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac
(Yale University, USA; University of California at San Diego, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript
Blake Loring, Duncan Mitchell, and Johannes Kinder
(Royal Holloway University of London, UK; Bundeswehr University Munich, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Effective Floating-Point Analysis via Weak-Distance Minimization
Zhoulai Fu and Zhendong Su
(IT University of Copenhagen, Denmark; ETH Zurich, Switzerland)
Publisher's Version Article Search

Parallelism and Super Computing I

Huron: Hybrid False Sharing Detection and Repair
Tanvir Ahmed Khan, Yifan Zhao, Gilles Pokam, Barzan Mozafari, and Baris Kasikci
(University of Michigan, USA; Intel, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Model-Driven Transformations for Multi- and Many-Core CPUs
Martin Kong and Louis-Noël Pouchet
(Brookhaven National Laboratory, USA; Colorado State University, USA)
Publisher's Version Article Search
Parallelism-Centric What-If and Differential Analyses
Adarsh Yoga and Santosh Nagarakatte
(Rutgers University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Type Systems I

Verifying Message-Passing Programs with Dependent Behavioural Types
Alceste Scalas, Nobuko Yoshida, and Elias Benussi
(Imperial College London, UK; Aston University, UK; Faculty Science, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Toward Efficient Gradual Typing for Structural Types via Coercions
Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek
(Indiana University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg
(Facebook, USA; SUNY Buffalo, USA; MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; MPI-SWS, Germany)
Publisher's Version Article Search

Bug Finding and Testing II

Parser-Directed Fuzzing
Björn Mathis, Rahul Gopinath, Michaël Mera, Alexander Kampmann, Matthias Höschele, and Andreas Zeller
(CISPA, Germany)
Publisher's Version Article Search
Continuously Reasoning about Programs using Differential Bayesian Inference
Kihong Heo, Mukund Raghothaman, Xujie Si, and Mayur Naik
(University of Pennsylvania, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Sparse Record and Replay with Controlled Scheduling
Christopher Lidbury and Alastair F. Donaldson
(Imperial College London, UK)
Publisher's Version Article Search

Parallelism and Super Computing II

Sparse Computation Data Dependence Simplification for Efficient Compiler-Generated Inspectors
Mahdi Soltan Mohammadi, Tomofumi Yuki, Kazem Cheshmi, Eddie C. Davis, Mary Hall, Maryam Mehri Dehnavi, Payal Nandy, Catherine Olschanowsky, Anand Venkat, and Michelle Mills Strout
(University of Arizona, USA; Inria, France; University of Rennes, France; CNRS, France; IRISA, France; University of Toronto, Canada; Boise State University, USA; University of Utah, USA; Intel, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Modular Divide-and-Conquer Parallelization of Nested Loops
Azadeh Farzan and Victor Nicolet
(University of Toronto, Canada)
Publisher's Version Article Search
Generating Piecewise-Regular Code from Irregular Structures
Travis Augustine, Janarthanan Sarma, Louis-Noël Pouchet, and Gabriel Rodríguez
(Colorado State University, USA; Universidade da Coruña, Spain)
Publisher's Version Article Search Artifacts Functional

Type Systems II

ILC: A Calculus for Composable, Computational Cryptography
Kevin Liao, Matthew A. Hammer, and Andrew Miller
(University of Illinois at Urbana-Champaign, USA; DFINITY, USA)
Publisher's Version Article Search
Proving Differential Privacy with Shadow Execution
Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang
(Pennsylvania State University, USA)
Publisher's Version Article Search
Data-Trace Types for Distributed Stream Processing Systems
Konstantinos Mamouras, Caleb Stanford, Rajeev Alur, Zachary G. Ives, and Val Tannen
(Rice University, USA; University of Pennsylvania, USA)
Publisher's Version Article Search

ML

An Inductive Synthesis Framework for Verifiable Reinforcement Learning
He Zhu, Zikang Xiong, Stephen Magill, and Suresh Jagannathan
(Galois, USA; Purdue University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Programming Support for Autonomizing Software
Wen-Chuan Lee, Peng Liu, Yingqi Liu, Shiqing Ma, and Xiangyu Zhang
(Purdue University, USA; IBM, USA)
Publisher's Version Article Search
Wootz: A Compiler-Based Framework for Fast CNN Pruning via Composability
Hui Guan, Xipeng Shen, and Seung-Hwan Lim
(North Carolina State University, USA; Oak Ridge National Laboratory, USA)
Publisher's Version Article Search
Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri
(University of Texas at Austin, USA; Rice University, USA)
Publisher's Version Article Search

Specification

Unsupervised Learning of API Aliasing Specifications
Jan Eberhardt, Samuel Steffen, Veselin Raychev, and Martin Vechev
(DeepCode, Switzerland; ETH Zurich, Switzerland)
Publisher's Version Article Search
Scalable Taint Specification Inference with Big Code
Victor Chibotaru, Benjamin Bichsel, Veselin Raychev, and Martin Vechev
(DeepCode, Switzerland; ETH Zurich, Switzerland)
Publisher's Version Article Search
Learning Stateful Preconditions Modulo a Test Generator
Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen
(Stevens Institute of Technology, USA; University of Nebraska-Lincoln, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Static Analysis

Abstract Interpretation under Speculative Execution
Meng Wu and Chao Wang
(Virginia Tech, USA; University of Southern California, USA)
Publisher's Version Article Search
A Fast Analytical Model of Fully Associative Caches
Tobias Gysi, Tobias Grosser, Laurin Brandner, and Torsten Hoefler
(ETH Zurich, Switzerland)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees
Laith Sakka, Kirshanthan Sundararajah, Ryan R. Newton, and Milind Kulkarni
(Purdue University, USA; Indiana University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Size-Change Termination as a Contract: Dynamically and Statically Enforcing Termination for Higher-Order Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland at College Park, USA; University of Alabama at Birmingham, USA; Indiana University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Dynamics: Analysis and Compilation

SemCluster: Clustering of Imperative Programming Assignments Based on Quantitative Semantic Features
David M. Perry, Dohyeong Kim, Roopsha Samanta, and Xiangyu Zhang
(Purdue University, USA)
Publisher's Version Article Search
Computing Summaries of String Loops in C for Better Testing and Refactoring
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Cristian Cadar
(Imperial College London, UK; Tel Aviv University, Israel; Technion, Israel)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Reusable Inline Caching for JavaScript Performance
Jiho Choi, Thomas Shull, and Josep Torrellas
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search

Performance

Composable, Sound Transformations of Nested Recursion and Loops
Kirshanthan Sundararajah and Milind Kulkarni
(Purdue University, USA)
Publisher's Version Article Search
Low-Latency Graph Streaming using Compressed Purely-Functional Trees
Laxman Dhulipala, Guy E. Blelloch, and Julian Shun
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Co-optimizing Memory-Level Parallelism and Cache-Level Parallelism
Xulong Tang, Mahmut Taylan Kandemir, Mustafa Karakoy, and Meenakshi Arunachalam
(Pennsylvania State University, USA; TOBB University of Economics and Technology, Turkey; Intel, USA)
Publisher's Version Article Search

Type Systems III

Characterising Renaming within OCaml’s Module System: Theory and Implementation
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson, and Scott Owens
(University of Kent, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, and David Van Horn
(University of Maryland at College Park, USA; IMDEA Software Institute, Spain; Tufts University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Systems I

Replication-Aware Linearizability
Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri
(IRIF, France; University Paris Diderot, France; CNRS, France; ARM, UK)
Publisher's Version Article Search
DFix: Automatically Fixing Timing Bugs in Distributed Systems
Guangpu Li, Haopeng Liu, Xianglan Chen, Haryadi S. Gunawi, and Shan Lu
(University of Chicago, USA; University of Science and Technology of China, China)
Publisher's Version Article Search
Ignis: Scaling Distribution-Oblivious Systems with Light-Touch Distribution
Nikos Vasilakis, Ben Karel, Yash Palkhiwala, John Sonchack, André DeHon, and Jonathan M. Smith
(University of Pennsylvania, USA)
Publisher's Version Article Search

Verification I

Semantic Program Alignment for Equivalence Checking
Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Verified Compilation on a Verified Processor
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox
(Chalmers University of Technology, Sweden; DeepMind, UK; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; Australian National University, Australia; ARM, UK)
Publisher's Version Article Search Artifacts Functional
Argosy: Verifying Layered Storage Systems with Recovery Refinement
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Systems II

Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv
(VMware, USA; Tel Aviv University, Israel; University of Waterloo, Canada; SRI International, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Transactional Concurrency Control for Intermittent, Energy-Harvesting Computing Systems
Emily Ruppel and Brandon Lucia
(Carnegie Mellon University, USA)
Publisher's Version Article Search
Supporting Peripherals in Intermittent Systems with Just-In-Time Checkpoints
Kiwan Maeng and Brandon Lucia
(Carnegie Mellon University, USA)
Publisher's Version Article Search

Verification II

Verification of Programs under the Release-Acquire Semantics
Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna
(Uppsala University, Sweden; IIT Bombay, India)
Publisher's Version Article Search Artifacts Available Artifacts Functional
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
An Applied Quantum Hoare Logic
Li Zhou, Nengkun Yu, and Mingsheng Ying
(Tsinghua University, China; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China)
Publisher's Version Article Search

proc time: 5.58