PLDI 2020
41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2020)
Powered by
Conference Publishing Consulting

41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2020), June 15–20, 2020, London, UK

PLDI 2020 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Message from the Chairs
PLDI 2020 Organization
Sponsors

Synthesis I

Data-Driven Inference of Representation Invariants
Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker
(Princeton University, USA; University of California at Los Angeles, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Type Error Feedback via Analytic Program Repair
Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, and Ranjit Jhala
(University of California at San Diego, USA; University of Michigan, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Synthesizing Structured CAD Models with Equality Saturation and Inverse Transformations
Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock
(University of Washington, USA; Certora, USA; MPI-SWS, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Language Implementation

Compiler and Runtime Support for Continuation Marks
Matthew Flatt and R. Kent Dybvig
(University of Utah, USA; Cisco Systems, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Crafty: Efficient, HTM-Compatible Persistent Transactions
Kaan Genç, Michael D. Bond, and Guoqing Harry Xu
(Ohio State University, USA; University of California at Los Angeles, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
From Folklore to Fact: Comparing Implementations of Stacks and Continuations
Kavon Farvardin and John Reppy
(University of Chicago, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Machine Learning I

Typilus: Neural Type Hints
Miltiadis Allamanis, Earl T. Barr, Soline Ducousso, and Zheng Gao
(Microsoft Research, UK; University College London, UK; ENSTA Paris, France)
Publisher's Version Article Search
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks
Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu
(Columbia University, USA)
Publisher's Version Article Search Artifacts Functional
Blended, Precise Semantic Program Embeddings
Ke Wang and Zhendong Su
(Visa Research, USA; ETH Zurich, Switzerland)
Publisher's Version Article Search

Security

Towards a Verified Range Analysis for JavaScript JITs
Fraser Brown, John Renner, Andres Nötzli, Sorin Lerner, Hovav Shacham, and Deian Stefan
(Stanford University, USA; University of California at San Diego, USA; University of Texas at Austin, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Binary Rewriting without Control Flow Recovery
Gregory J. Duck, Xiang Gao, and Abhik Roychoudhury
(National University of Singapore, Singapore)
Publisher's Version Article Search
BlankIt Library Debloating: Getting What You Want Instead of Cutting What You Don’t
Chris Porter, Girish Mururu, Prithayan Barua, and Santosh Pande
(Georgia Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Verification I

Verifying Concurrent Search Structure Templates
Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies
(Microsoft Research, UK; New York University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Armada: Low-Effort Verification of High-Performance Concurrent Programs
Jacob R. Lorch, Yixuan Chen, Manos Kapritsos, Bryan Parno, Shaz Qadeer, Upamanyu Sharma, James R. Wilcox, and Xueyuan Zhao
(Microsoft Research, USA; University of Michigan, USA; Yale University, USA; Carnegie Mellon University, USA; Calibra, USA; Certora, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Decidable Verification under a Causally Consistent Shared Memory
Ori Lahav and Udi Boker
(Tel Aviv University, Israel; IDC Herzliya, Israel)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Inductive Sequentialization of Asynchronous Programs
Bernhard Kragl, Constantin Enea, Thomas A. Henzinger, Suha Orhun Mutluergil, and Shaz Qadeer
(IST Austria, Austria; IRIF, France; University of Paris, France; CNRS, France; Calibra, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Language Design I

The Essence of Bluespec: A Core Language for Rule-Based Hardware Design
Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, and Arvind
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional
LLHD: A Multi-level Intermediate Representation for Hardware Description Languages
Fabian Schuiki, Andreas Kurth, Tobias Grosser, and Luca Benini
(ETH Zurich, Switzerland)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable Artifacts Functional
On the Principles of Differentiable Quantum Programming Languages
Shaopeng Zhu, Shih-Han Hung, Shouvanik Chakrabarti, and Xiaodi Wu
(University of Maryland, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics
Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Memory Management

Improving Program Locality in the GC using Hotness
Albert Mingkun Yang, Erik Österlund, and Tobias Wrigstad
(Uppsala University, Sweden; Oracle, Sweden)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
A Marriage of Pointer- and Epoch-Based Reclamation
Jeehoon Kang and Jaehwang Jung
(KAIST, South Korea)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable Artifacts Functional
CARAT: A Case for Virtual Memory through Compiler- and Runtime-Based Address Translation
Brian Suchy, Simone Campanoni, Nikos Hardavellas, and Peter Dinda
(Northwestern University, USA)
Publisher's Version Article Search

Concurrency

Repairing and Mechanising the JavaScript Relaxed Memory Model
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, and Shu-yu Guo
(University of Cambridge, UK; National Research University Higher School of Economics, Russia; MPI-SWS, Germany; ENS Rennes, France; Bloomberg, USA)
Publisher's Version Article Search
Promising 2.0: Global Optimizations in Relaxed Memory Concurrency
Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, and Viktor Vafeiadis
(Seoul National University, South Korea; National Research University Higher School of Economics, Russia; MPI-SWS, Germany; IIT Delhi, India; Tel Aviv University, Israel)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
NVTraverse: In NVRAM Data Structures, the Destination Is More Important Than the Journey
Michal Friedman, Naama Ben-David, Yuanhao Wei, Guy E. Blelloch, and Erez Petrank
(Technion, Israel; Carnegie Mellon University, USA)
Publisher's Version Article Search Info

Type Systems

Predictable Accelerator Design with Time-Sensitive Affine Types
Rachit Nigam, Sachille Atapattu, Samuel Thomas, Zhijing Li, Theodore Bauer, Yuwei Ye, Apurva Koti, Adrian Sampson, and Zhiru Zhang
(Cornell University, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable Artifacts Functional
Type-Directed Scheduling of Streaming Accelerators
David Durst, Matthew Feldman, Dillon Huff, David Akeley, Ross Daly, Gilbert Louis Bernstein, Marco Patrignani, Kayvon Fatahalian, and Pat Hanrahan
(Stanford University, USA; University of California at Los Angeles, USA; University of California at Berkeley, USA; CISPA, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Functional
FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates
(University of Edinburgh, UK; Imperial College London, UK; Lodz University of Technology, Poland; Alan Turing Institute, UK)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional

Smart Contracts

Securing Smart Contract with Runtime Validation
Ao Li, Jemin Andrew Choi, and Fan Long
(University of Toronto, Canada)
Publisher's Version Article Search Artifacts Functional
Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities
Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis
(International Computer Science Institute, USA; University of Sydney, Australia; University of Athens, Greece)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Behavioral Simulation for Smart Contracts
Sidi Mohamed Beillahi, Gabriela Ciocarlie, Michael Emmi, and Constantin Enea
(University of Paris Diderot, France; IRIF, France; CNRS, France; SRI International, USA; IUF, France)
Publisher's Version Article Search Artifacts Functional

Synthesis II

Multi-modal Synthesis of Regular Expressions
Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, and Isil Dillig
(University of Texas at Austin, USA; University of Michigan at Ann Arbor, USA)
Publisher's Version Article Search
Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting
DongKwon Lee, Woosuk Lee, Hakjoo Oh, and Kwangkeun Yi
(Seoul National University, South Korea; Hanyang University, South Korea; Korea University, South Korea)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
CacheQuery: Learning Replacement Policies from Hardware Caches
Pepe Vila, Pierre Ganty, Marco Guarnieri, and Boris Köpf
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain; Microsoft Research, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Language Design II

HipHop.js: (A)Synchronous Reactive Web Programming
Gérard Berry and Manuel Serrano
(Collège de France, France; Inria, France)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable Artifacts Functional
EVA: An Encrypted Vector Arithmetic Language and Compiler for Efficient Homomorphic Computation
Roshan Dathathri, Blagovesta Kostova, Olli Saarikivi, Wei Dai, Kim Laine, and Madan Musuvathi
(University of Texas at Austin, USA; EPFL, Switzerland; Microsoft Research, USA)
Publisher's Version Article Search
Towards an API for the Real Numbers
Hans-J. Boehm
(Google, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Responsive Parallelism with Futures and State
Stefan K. Muller, Kyle Singer, Noah Goldstein, Umut A. Acar, Kunal Agrawal, and I-Ting Angelina Lee
(Carnegie Mellon University, USA; Washington University in St. Louis, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Performance

SympleGraph: Distributed Graph Processing with Precise Loop-Carried Dependency Guarantee
Youwei Zhuo, Jingji Chen, Qinyi Luo, Yanzhi Wang, Hailong Yang, Depei Qian, and Xuehai Qian
(University of Southern California, USA; Northeastern University, USA; Beihang University, China)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional
PMEvo: Portable Inference of Port Mappings for Out-of-Order Processors by Evolutionary Optimization
Fabian Ritter and Sebastian Hack
(Saarland University, Germany)
Publisher's Version Article Search Artifacts Functional
PMThreads: Persistent Memory Threads Harnessing Versioned Shadow Copies
Zhenwei Wu, Kai Lu, Andrew Nisbet, Wenzhe Zhang, and Mikel Luján
(National University of Defense Technology, China; University of Manchester, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework
Sotiris Apostolakis, Ziyang Xu, Zujun Tan, Greg Chan, Simone Campanoni, and David I. August
(Princeton University, USA; Northwestern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Verification II

Scalable Validation of Binary Lifters
Sandeep Dasgupta, Sushant Dinesh, Deepan Venkatesh, Vikram S. Adve, and Christopher W. Fletcher
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Polynomial Invariant Generation for Non-deterministic Recursive Programs
Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady
(IST Austria, Austria; Shanghai Jiao Tong University, China; Ferdowsi University of Mashhad, Iran)
Publisher's Version Article Search
Templates and Recurrences: Better Together
Jason Breck, John Cyphert, Zachary Kincaid, and Thomas Reps
(University of Wisconsin-Madison, USA; Princeton University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
First-Order Quantified Separators
Jason R. Koenig, Oded Padon, Neil Immerman, and Alex Aiken
(Stanford University, USA; University of Massachusetts at Amherst, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Bug Finding

Validating SMT Solvers via Semantic Fusion
Dominik Winterer, Chengyu Zhang, and Zhendong Su
(ETH Zurich, Switzerland; East China Normal University, China)
Publisher's Version Article Search
Debugging and Detecting Numerical Errors in Computation with Posits
Sangeeta Chowdhary, Jay P. Lim, and Santosh Nagarakatte
(Rutgers University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
SmartTrack: Efficient Predictive Race Detection
Jake Roemer, Kaan Genç, and Michael D. Bond
(Ohio State University, USA)
Publisher's Version Article Search Artifacts Available
Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs
Boqin Qin, Yilun Chen, Zeming Yu, Linhai Song, and Yiying Zhang
(Pennsylvania State University, USA; Purdue University, USA; University of California at San Diego, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Static Analysis

Fast Graph Simplification for Interleaved Dyck-Reachability
Yuanbo Li, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Publisher's Version Article Search
Static Analysis of Java Enterprise Applications: Frameworks and Caches, the Elephants in the Room
Anastasios Antoniadis, Nikos Filippakis, Paddy Krishnan, Raghavendra Ramesh, Nicholas Allen, and Yannis Smaragdakis
(University of Athens, Greece; CERN, Switzerland; Oracle Labs, Australia; ConsenSys, Australia)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Automated Derivation of Parametric Data Movement Lower Bounds for Affine Programs
Auguste Olivry, Julien Langou, Louis-Noël Pouchet, P. Sadayappan, and Fabrice Rastello
(Grenoble Alps University, France; CNRS, France; Inria, France; Grenoble INP, France; LIG, France; University of Colorado at Denver, USA; Colorado State University, USA; University of Utah, USA)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional

Code Generation

Automatic Generation of Efficient Sparse Tensor Format Conversion Routines
Stephen Chou, Fredrik Kjolstad, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; Stanford University, USA)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional
OOElala: Order-of-Evaluation Based Alias Analysis for Compiler Optimization
Ankush Phulia, Vaibhav Bhagee, and Sorav Bansal
(IIT Delhi, India)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Effective Function Merging in the SSA Form
Rodrigo C. O. Rocha, Pavlos Petoumenos, Zheng Wang, Murray Cole, and Hugh Leather
(University of Edinburgh, UK; University of Manchester, UK; University of Leeds, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Probabilistic Programming

Proving Almost-Sure Termination by Omega-Regular Decomposition
Jianhui Chen and Fei He
(Tsinghua University, China)
Publisher's Version Article Search
λPSI: Exact Inference for Higher-Order Probabilistic Programs
Timon Gehr, Samuel Steffen, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Reactive Probabilistic Programming
Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin
(IBM Research, USA; Massachusetts Institute of Technology, USA; ENS, France; PSL University, France)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional

Symbolic Execution

Constant-Time Foundations for the New Spectre Era
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe
(University of California at San Diego, USA; Inria, France; MPI-SP, Germany; IMDEA Software Institute, Spain)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Gillian, Part I: A Multi-language Platform for Symbolic Execution
José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner
(INESC-ID, Portugal; Instituto Superior Técnico, University of Lisbon, Portugal; Imperial College London, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Efficient Handling of String-Number Conversion
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janků, Hsin-Hung Lin, Lukáš Holík, and Wei-Cheng Wu
(Uppsala University, Sweden; Academia Sinica, Taiwan; IBM Research, USA; Brno University of Technology, Czechia; University of Southern California, USA)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional

Networking and Hardware

NV: An Intermediate Language for Verification of Network Control Planes
Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker
(Princeton University, USA; Microsoft Research, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Detecting Network Load Violations for Distributed Control Planes
Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, and Aditya Akella
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search Artifacts Functional
Compiler-Directed Soft Error Resilience for Lightweight GPU Register File Protection
Hongjune Kim, Jianping Zeng, Qingrui Liu, Mohammad Abdel-Majeed, Jaejin Lee, and Changhee Jung
(Seoul National University, South Korea; Purdue University, USA; Annapurna Labs, USA; University of Jordan, Jordan)
Publisher's Version Article Search
Adaptive Low-Overhead Scheduling for Periodic and Reactive Intermittent Execution
Kiwan Maeng and Brandon Lucia
(Carnegie Mellon University, USA)
Publisher's Version Article Search

Parsing, Debugging, and Code Search

Faster General Parsing through Context-Free Memoization
Grzegorz Herman
(Jagiellonian University, Poland)
Publisher's Version Article Search
Zippy LL(1) Parsing with Derivatives
Romain Edelmann, Jad Hamza, and Viktor Kunčak
(EPFL, Switzerland)
Publisher's Version Article Search
Debug Information Validation for Optimized Code
Yuanbo Li, Shuo Ding, Qirun Zhang, and Davide Italiano
(Georgia Institute of Technology, USA; Apple, USA)
Publisher's Version Article Search
Semantic Code Search via Equational Reasoning
Varot Premtoon, James Koppel, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Video Artifacts Available Artifacts Functional

Machine Learning II

Proving Data-Poisoning Robustness in Decision Trees
Samuel Drews, Aws Albarghouthi, and Loris D'Antoni
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search Artifacts Reusable Artifacts Functional
A Study of the Learnability of Relational Properties: Model Counting Meets Machine Learning (MCML)
Muhammad Usman, Wenxi Wang, Marko Vasic, Kaiyuan Wang, Haris Vikalo, and Sarfraz Khurshid
(University of Texas at Austin, USA; Google, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Learning Fast and Precise Numerical Analysis
Jingxuan He, Gagandeep Singh, Markus Püschel, and Martin Vechev
(ETH Zurich, Switzerland)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional

Synthesis III

Exact and Approximate Methods for Proving Unrealizability of Syntax-Guided Synthesis Problems
Qinheping Hu, John Cyphert, Loris D'Antoni, and Thomas Reps
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Question Selection for Interactive Program Synthesis
Ruyi Ji, Jingjing Liang, Yingfei Xiong, Lu Zhang, and Zhenjiang Hu
(Peking University, China)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional
Reconciling Enumerative and Deductive Program Synthesis
Kangjing Huang, Xiaokang Qiu, Peiyuan Shen, and Yanjun Wang
(Purdue University, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable Artifacts Functional

proc time: 30.85