PLDI 2022
43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022)
Powered by
Conference Publishing Consulting

43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022), June 13–17, 2022, San Diego, CA, USA

PLDI 2022 – Proceedings

Contents - Abstracts - Authors

Frontmatter

Title Page
Welcome from the Chairs
PLDI 2022 Committees
PLDI 2022 Sponsors and Supporters

Security

Modular Information Flow through Ownership
Will CrichtonORCID logo, Marco Patrignani ORCID logo, Maneesh Agrawala ORCID logo, and Pat Hanrahan ORCID logo
(Stanford University, USA; University of Trento, Italy)
Publisher's Version Article Search Archive submitted (3.6 MB) Artifacts Available Artifacts Reusable
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
Sankha Narayan GuriaORCID logo, Niki VazouORCID logo, Marco Guarnieri, and James Parker
(University of Maryland at College Park, USA; IMDEA Software Institute, Spain; Galois, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy ORCID logo, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta
(Microsoft Research, USA; Microsoft Research, India; Cornell University, USA; Microsoft, USA)
Publisher's Version Article Search
P4BID: Information Flow Control in P4
Karuna Grewal, Loris D'AntoniORCID logo, and Justin Hsu ORCID logo
(Cornell University, USA; University of Wisconsin-Madison, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Memory

Turning Manual Concurrent Memory Reclamation into Automatic Reference Counting
Daniel Anderson ORCID logo, Guy E. Blelloch ORCID logo, and Yuanhao Wei ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Low-Latency, High-Throughput Garbage Collection
Wenyu ZhaoORCID logo, Stephen M. BlackburnORCID logo, and Kathryn S. McKinleyORCID logo
(Australian National University, Australia; Google, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Mako: A Low-Pause, High-Throughput Evacuating Collector for Memory-Disaggregated Datacenters
Haoran Ma, Shi Liu, Chenxi Wang ORCID logo, Yifan Qiao, Michael D. Bond, Stephen M. BlackburnORCID logo, Miryung Kim, and Guoqing Harry Xu
(University of California at Los Angeles, USA; Ohio State University, USA; Australian National University, Australia)
Publisher's Version Article Search Artifacts Available
PaC-Trees: Supporting Parallel and Compressed Purely-Functional Collections
Laxman DhulipalaORCID logo, Guy E. Blelloch ORCID logo, Yan Gu ORCID logo, and Yihan Sun ORCID logo
(University of Maryland, USA; Carnegie Mellon University, USA; University of California at Riverside, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Synthesis I

Type-Directed Program Synthesis for RESTful APIs
Zheng Guo ORCID logo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, and Nadia PolikarpovaORCID logo
(University of California at San Diego, USA; Akita Software, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Visualization Question Answering using Introspective Program Synthesis
Yanju Chen ORCID logo, Xifeng Yan ORCID logo, and Yu FengORCID logo
(University of California at Santa Barbara, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
WebRobot: Web Robotic Process Automation using Interactive Programming-by-Demonstration
Rui Dong ORCID logo, Zhicheng Huang ORCID logo, Ian Iong Lam ORCID logo, Yan ChenORCID logo, and Xinyu Wang ORCID logo
(University of Michigan, USA; University of Toronto, Canada)
Publisher's Version Article Search
Synthesizing Analytical SQL Queries from Computation Demonstration
Xiangyu Zhou, Rastislav Bodik, Alvin Cheung ORCID logo, and Chenglong Wang
(University of Washington, USA; University of California at Berkeley, USA; Microsoft Research, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Compilation

Finding Typing Compiler Bugs
Stefanos Chaliasos ORCID logo, Thodoris Sotiropoulos ORCID logo, Diomidis Spinellis ORCID logo, Arthur Gervais ORCID logo, Benjamin Livshits ORCID logo, and Dimitris Mitropoulos ORCID logo
(Imperial College London, UK; Athens University of Economics and Business, Greece; Delft University of Technology, Netherlands; University of Athens, Greece)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
IRDL: An IR Definition Language for SSA Compilers
Mathieu Fehr ORCID logo, Jeff Niu, River Riddle, Mehdi Amini ORCID logo, Zhendong Su ORCID logo, and Tobias Grosser ORCID logo
(University of Edinburgh, UK; University of Waterloo, Canada; Modular AI, USA; Google, USA; ETH Zurich, Switzerland)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Sequential Reasoning for Optimizing Compilers under Weak Memory Concurrency
Minki Cho ORCID logo, Sung-Hwan LeeORCID logo, Dongjae Lee ORCID logo, Chung-Kil Hur ORCID logo, and Ori LahavORCID logo
(Seoul National University, South Korea; Tel Aviv University, Israel)
Publisher's Version Article Search Info Artifacts Available Artifacts Functional

Synthesis II

Can Reactive Synthesis and Syntax-Guided Synthesis Be Friends?
Wonhyuk ChoiORCID logo, Bernd Finkbeiner ORCID logo, Ruzica Piskac ORCID logo, and Mark Santolucito ORCID logo
(Columbia University, USA; CISPA, Germany; Yale University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Recursion Synthesis with Unrealizability Witnesses
Azadeh FarzanORCID logo, Danya Lette ORCID logo, and Victor NicoletORCID logo
(University of Toronto, Canada)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
“Synthesizing Input Grammars”: A Replication Study
Bachir Bendrissou ORCID logo, Rahul GopinathORCID logo, and Andreas Zeller ORCID logo
(CISPA, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Tensors

Autoscheduling for Sparse Tensor Algebra with an Asymptotic Cost Model
Peter AhrensORCID logo, Fredrik KjolstadORCID logo, and Saman AmarasingheORCID logo
(Massachusetts Institute of Technology, USA; Stanford University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
DISTAL: The Distributed Tensor Algebra Compiler
Rohan Yadav, Alex AikenORCID logo, and Fredrik KjolstadORCID logo
(Stanford University, USA)
Publisher's Version Article Search
All You Need Is Superword-Level Parallelism: Systematic Control-Flow Vectorization with SLP
Yishen Chen, Charith Mendis, and Saman AmarasingheORCID logo
(Massachusetts Institute of Technology, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Warping Cache Simulation of Polyhedral Programs
Canberk Morelli ORCID logo and Jan ReinekeORCID logo
(Saarland University, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Distribution

Certified Mergeable Replicated Data Types
Vimala SoundarapandianORCID logo, Adharsh Kamath ORCID logo, Kartik Nagar ORCID logo, and KC SivaramakrishnanORCID logo
(IIT Madras, India; NITK Surathkal, India)
Publisher's Version Article Search
Hamband: RDMA Replicated Data Types
Farzin Houshmand ORCID logo, Javad Saberlatibari, and Mohsen Lesani ORCID logo
(University of California at Riverside, USA)
Publisher's Version Article Search
RunTime-Assisted Convergence in Replicated Data Types
Gowtham KakiORCID logo, Prasanth Prahladan, and Nicholas V. Lewchenko
(University of Colorado Boulder, USA)
Publisher's Version Article Search Archive submitted (210 kB)
Adore: Atomic Distributed Objects with Certified Reconfiguration
Wolf Honoré ORCID logo, Ji-Yong Shin ORCID logo, Jieung KimORCID logo, and Zhong Shao ORCID logo
(Yale University, USA; Northeastern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Analysis

CycleQ: An Efficient Basis for Cyclic Equational Reasoning
Eddie Jones ORCID logo, C.-H. Luke Ong ORCID logo, and Steven Ramsay ORCID logo
(University of Bristol, UK; University of Oxford, UK)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Finding the Dwarf: Recovering Precise Types from WebAssembly Binaries
Daniel LehmannORCID logo and Michael Pradel ORCID logo
(University of Stuttgart, Germany)
Publisher's Version Article Search Info
Abstract Interpretation Repair
Roberto BruniORCID logo, Roberto GiacobazziORCID logo, Roberta GoriORCID logo, and Francesco RanzatoORCID logo
(University of Pisa, Italy; University of Verona, Italy; University of Padua, Italy)
Publisher's Version Article Search
Differential Cost Analysis with Simultaneous Potentials and Anti-potentials
Đorđe Žikelić, Bor-Yuh Evan ChangORCID logo, Pauline Bolignano, and Franco Raimondi
(IST Austria, Austria; University of Colorado Boulder, USA; Amazon, USA; Amazon, UK; Middlesex University, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Concurrency

A Flexible Type System for Fearless Concurrency
Mae MilanoORCID logo, Joshua Turcotti ORCID logo, and Andrew C. Myers ORCID logo
(University of California at Berkeley, USA; Cornell University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
A Study of Real-World Data Races in Golang
Milind Chabbi ORCID logo and Murali Krishna Ramanathan ORCID logo
(Uber Technologies, USA)
Publisher's Version Article Search Artifacts Available
Checking Robustness to Weak Persistency Models
Hamed GorjiaraORCID logo, Weiyu Luo, Alex Lee, Guoqing Harry Xu, and Brian Demsky
(University of California at Irvine, USA; University of California at Los Angeles, USA)
Publisher's Version Article Search Archive submitted (260 kB) Artifacts Available Artifacts Reusable
Sound Sequentialization for Concurrent Program Verification
Azadeh FarzanORCID logo, Dominik Klumpp ORCID logo, and Andreas Podelski ORCID logo
(University of Toronto, Canada; University of Freiburg, Germany)
Publisher's Version Article Search Archive submitted (3.1 MB) Artifacts Available Artifacts Reusable

Numbers

Choosing Mathematical Function Implementations for Speed and Accuracy
Ian Briggs ORCID logo and Pavel PanchekhaORCID logo
(University of Utah, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming
Raven Beutner ORCID logo, C.-H. Luke Ong ORCID logo, and Fabian Zaiser ORCID logo
(CISPA, Germany; University of Oxford, UK)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Progressive Polynomial Approximations for Fast Correctly Rounded Math Libraries
Mridul AanjaneyaORCID logo, Jay P. Lim ORCID logo, and Santosh Nagarakatte ORCID logo
(Rutgers University, USA; Yale University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Semantics

A Typed Continuation-Passing Translation for Lexical Effect Handlers
Philipp Schuster ORCID logo, Jonathan Immanuel BrachthäuserORCID logo, Marius Müller ORCID logo, and Klaus Ostermann ORCID logo
(University of Tübingen, Germany)
Publisher's Version Article Search
Deep and Shallow Types for Gradual Languages
Ben GreenmanORCID logo
(Brown University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Kleene Algebra Modulo Theories: A Framework for Concrete KATs
Michael GreenbergORCID logo, Ryan Beckett, and Eric Campbell ORCID logo
(Stevens Institute of Technology, USA; Microsoft Research, USA; Cornell University, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Semantic Soundness for Language Interoperability
Daniel Patterson, Noble Mushtak, Andrew Wagner, and Amal Ahmed
(Northeastern University, USA)
Publisher's Version Article Search

Quantum

Quartz: Superoptimization of Quantum Circuits
Mingkuan Xu ORCID logo, Zikun Li ORCID logo, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth ORCID logo, Henry Ma ORCID logo, Jens PalsbergORCID logo, Alex Aiken ORCID logo, Umut A. Acar ORCID logo, and Zhihao Jia ORCID logo
(Carnegie Mellon University, USA; University of California at Los Angeles, USA; VMware Research, USA; Microsoft, USA; University of Oxford, UK; Stanford University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Giallar: Push-Button Verification for the Qiskit Quantum Compiler
Runzhou Tao ORCID logo, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. ChongORCID logo, and Ronghui GuORCID logo
(Columbia University, USA; Amazon, USA; IBM Research, USA; University of Chicago, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra
Yuxiang Peng ORCID logo, Mingsheng Ying ORCID logo, and Xiaodi Wu ORCID logo
(University of Maryland, USA; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)
Publisher's Version Article Search
PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics
Michael ChristensenORCID logo, Georgios Tzimpragos ORCID logo, Harlan Kringen ORCID logo, Jennifer Volk, Timothy SherwoodORCID logo, and Ben Hardekopf
(University of California at Santa Barbara, USA)
Publisher's Version Article Search Archive submitted (810 kB) Artifacts Available Artifacts Reusable

Hardware

Bind the Gap: Compiling Real Software to Hardware FFT Accelerators
Jackson Woodruff ORCID logo, Jordi Armengol-Estapé ORCID logo, Sam AinsworthORCID logo, and Michael F. P. O'Boyle ORCID logo
(University of Edinburgh, UK)
Publisher's Version Article Search Artifacts Available
Exocompilation for Productive Programming of Hardware Accelerators
Yuka IkarashiORCID logo, Gilbert Louis BernsteinORCID logo, Alex ReinkingORCID logo, Hasan Genc ORCID logo, and Jonathan Ragan-KelleyORCID logo
(Massachusetts Institute of Technology, USA; University of California at Berkeley, USA)
Publisher's Version Article Search Archive submitted (570 kB) Artifacts Available Artifacts Reusable
PDL: A High-Level Hardware Design Language for Pipelined Processors
Drew ZagieboyloORCID logo, Charles Sherk, Gookwon Edward Suh ORCID logo, and Andrew C. Myers ORCID logo
(Cornell University, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Software-Hardware Codesign for Efficient In-Memory Regular Pattern Matching
Lingkun Kong, Qixuan Yu, Agnishom Chattopadhyay, Alexis Le Glaunec, Yi Huang, Konstantinos Mamouras, and Kaiyuan Yang
(Rice University, USA)
Publisher's Version Article Search

DSLs

Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations
Olivier FlückigerORCID logo, Jan Ječmen ORCID logo, Sebastián Krynski ORCID logo, and Jan VitekORCID logo
(Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Karp: A Language for NP Reductions
Chenhao Zhang, Jason D. Hartline, and Christos Dimoulas
(Northwestern University, USA)
Publisher's Version Article Search Artifacts Reusable
WARio: Efficient Code Generation for Intermittent Computing
Vito Kortbeek ORCID logo, Souradip Ghosh ORCID logo, Josiah Hester ORCID logo, Simone Campanoni ORCID logo, and Przemysław Pawełczak ORCID logo
(Delft University of Technology, Netherlands; Carnegie Mellon University, USA; Northwestern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Verification I

Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic
Hoang-Hai Dang ORCID logo, Jaehwang Jung ORCID logo, Jaemin Choi ORCID logo, Duc-Than Nguyen ORCID logo, William Mansky ORCID logo, Jeehoon KangORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; KAIST, South Korea; University of Illinois at Chicago, USA)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris
Ike MulderORCID logo, Robbert KrebbersORCID logo, and Herman Geuvers ORCID logo
(Radboud University Nijmegen, Netherlands; Eindhoven University of Technology, Netherlands)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
Michael Sammler ORCID logo, Angus Hammond ORCID logo, Rodolphe Lepigre ORCID logo, Brian Campbell ORCID logo, Jean Pichon-Pharabod ORCID logo, Derek DreyerORCID logo, Deepak GargORCID logo, and Peter Sewell ORCID logo
(MPI-SWS, Germany; University of Cambridge, UK; University of Edinburgh, UK; Aarhus University, Denmark)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
Yusuke MatsushitaORCID logo, Xavier DenisORCID logo, Jacques-Henri JourdanORCID logo, and Derek DreyerORCID logo
(University of Tokyo, Japan; Université Paris-Saclay, France; CNRS, France; ENS Paris-Saclay, France; Inria, France; Laboratoire Méthodes Formelles, France; MPI-SWS, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Verification and Optimization

Efficient Approximations for Cache-Conscious Data Placement
Ali Ahmadi, Majid Daliri, Amir Kafshdar Goharshady ORCID logo, and Andreas PavlogiannisORCID logo
(Sharif University of Technology, Iran; University of Tehran, Iran; Hong Kong University of Science and Technology, China; Aarhus University, Denmark)
Publisher's Version Article Search
FreeTensor: A Free-Form DSL with Holistic Optimizations for Irregular Tensor Programs
Shizhi Tang ORCID logo, Jidong Zhai, Haojie Wang ORCID logo, Lin Jiang, Liyan Zheng ORCID logo, Zhenhao Yuan, and Chen Zhang ORCID logo
(Tsinghua University, China)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Lasagne: A Static Binary Translator for Weak Memory Model Architectures
Rodrigo C. O. Rocha ORCID logo, Dennis Sprokholt, Martin Fink, Redha Gouicem ORCID logo, Tom Spink ORCID logo, Soham Chakraborty, and Pramod Bhatotia
(University of Edinburgh, UK; Delft University of Technology, Netherlands; TU Munich, Germany; University of St. Andrews, UK)
Publisher's Version Article Search Archive submitted (930 kB) Artifacts Available Artifacts Reusable
Verifying Optimizations of Concurrent Programs in the Promising Semantics
Junpeng Zha, Hongjin Liang, and Xinyu Feng
(Nanjing University, China)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Verification II

Relational Compilation for Performance-Critical Applications: Extensible Proof-Producing Translation of Functional Models into Low-Level Code
Clément Pit-ClaudelORCID logo, Jade Philipoom ORCID logo, Dustin Jamner ORCID logo, Andres ErbsenORCID logo, and Adam ChlipalaORCID logo
(EPFL, Switzerland; Amazon AWS, Switzerland; Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Formally Verified Lifting of C-Compiled x86-64 Binaries
Freek Verbeek ORCID logo, Joshua Bockenek ORCID logo, Zhoulai Fu ORCID logo, and Binoy Ravindran ORCID logo
(Open University of the Netherlands, Netherlands; Virginia Tech, USA; SUNY Korea, South Korea)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable
Leapfrog: Certified Equivalence for Protocol Parsers
Ryan Doenges ORCID logo, Tobias Kappé ORCID logo, John Sarracino ORCID logo, Nate FosterORCID logo, and Greg Morrisett ORCID logo
(Cornell University, USA; University of Amsterdam, Netherlands)
Publisher's Version Article Search Artifacts Available Artifacts Reusable
Computing Correctly with Inductive Relations
Zoe Paraskevopoulou, Aaron Eline, and Leonidas LampropoulosORCID logo
(Northeastern University, USA; University of Maryland, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable

Testing and Synthesis

Interpreter-Guided Differential JIT Compiler Unit Testing
Guillermo PolitoORCID logo, Stéphane Ducasse, and Pablo Tesone
(University of Lille, France; CNRS, France; Inria, France; Centrale Lille, France; UMR 9189 CRIStAL, France; Pharo Consortium, Argentina)
Publisher's Version Article Search
Landmarks and Regions: A Robust Approach to Data Extraction
Suresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry, Arun IyerORCID logo, Arjun Radhakrishna ORCID logo, Sriram K. Rajamani, and Mohammad Raza ORCID logo
(Microsoft, UK; Microsoft Research, India; Microsoft, USA)
Publisher's Version Article Search
Odin: On-Demand Instrumentation with On-the-Fly Recompilation
Mingzhe Wang ORCID logo, Jie Liang ORCID logo, Chijin Zhou, Zhiyong Wu ORCID logo, Xinyi Xu, and Yu JiangORCID logo
(Tsinghua University, China)
Publisher's Version Article Search
Quickstrom: Property-Based Acceptance Testing with LTL Specifications
Liam O'ConnorORCID logo and Oskar WickströmORCID logo
(University of Edinburgh, UK; Monoid Consulting, Sweden)
Publisher's Version Article Search Info Artifacts Available Artifacts Reusable

proc time: 11.84