OOPSLA 2021
Proceedings of the ACM on Programming Languages, Volume 5, Number OOPSLA
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 5, Number OOPSLA, October 20–22, 2021, Chicago, USA

OOPSLA – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems
Wolf Honoré ORCID logo, Jieung KimORCID logo, Ji-Yong Shin ORCID logo, and Zhong Shao ORCID logo
(Yale University, USA; Northeastern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Making Weak Memory Models Fair
Ori LahavORCID logo, Egor Namakonov ORCID logo, Jonas Oberhauser, Anton Podkopaev ORCID logo, and Viktor VafeiadisORCID logo
(Tel Aviv University, Israel; St. Petersburg University, Russia; JetBrains Research, Russia; Huawei, Germany; HSE University, Russia; MPI-SWS, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
Pengbo Yan ORCID logo and Toby Murray ORCID logo
(University of Melbourne, Australia)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Semantic Programming by Example with Pre-trained Models
Gust Verbruggen ORCID logo, Vu LeORCID logo, and Sumit GulwaniORCID logo
(KU Leuven, Belgium; Microsoft, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Promises Are Made to Be Broken: Migrating R to Strict Semantics
Aviral Goel ORCID logo, Jan Ječmen ORCID logo, Sebastián Krynski ORCID logo, Olivier FlückigerORCID logo, and Jan VitekORCID logo
(Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Efficient Compilation of Algebraic Effect Handlers
Georgios Karachalias, Filip Koprivec, Matija Pretnar ORCID logo, and Tom SchrijversORCID logo
(Tweag, France; University of Ljubljana, Slovenia; Institute of Mathematics, Physics, and Mechanics, Slovenia; KU Leuven, Belgium)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust
Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, and Amit Levy
(Princeton University, USA; Google, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Synthesizing Contracts Correct Modulo a Test Generator
Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. MadhusudanORCID logo, and Tao Xie ORCID logo
(University of Illinois at Urbana-Champaign, USA; Tufts University, USA; Peking University, China)
Publisher's Version
Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches
Masaomi Yamaguchi ORCID logo, Kazutaka Matsuda ORCID logo, Cristina David ORCID logo, and Meng Wang ORCID logo
(Tohoku University, Japan; University of Bristol, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
SimTyper: Sound Type Inference for Ruby using Type Equality Prediction
Milod Kazerounian, Jeffrey S. Foster, and Bonan Min
(University of Maryland at College Park, USA; Tufts University, USA; Raytheon BBN Technologies, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
ECROs: Building Global Scale Systems from Sequential Code
Kevin De PorreORCID logo, Carla Ferreira ORCID logo, Nuno Preguiça ORCID logo, and Elisa Gonzalez Boix ORCID logo
(Vrije Universiteit Brussel, Belgium; NOVA School of Science and Technology, Portugal)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Label Dependent Lambda Calculus and Gradual Typing
Weili Fu, Fabian Krause, and Peter ThiemannORCID logo
(University of Freiburg, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Efficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU
Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, and Jonathan Ragan-KelleyORCID logo
(Massachusetts Institute of Technology, USA; Adobe, USA; University of California at San Diego, USA)
Publisher's Version
Relational Nullable Types with Boolean Unification
Magnus Madsen ORCID logo and Jaco van de Pol
(Aarhus University, Denmark)
Publisher's Version
Solver-Based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane AndersonORCID logo, Michael Greenberg ORCID logo, and Arjun Guha ORCID logo
(University of Massachusetts at Amherst, USA; Wellesley College, USA; Stevens Institute of Technology, USA; Northeastern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
UDF to SQL Translation through Compositional Lazy Inductive Synthesis
Guoqiang Zhang, Yuanchao Xu ORCID logo, Xipeng ShenORCID logo, and Işıl Dillig ORCID logo
(North Carolina State University, USA; University of Texas at Austin, USA)
Publisher's Version
Verifying Concurrent Multicopy Search Structures
Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies ORCID logo
(New York University, USA; Microsoft Research, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Compiling with Continuations, Correctly
Zoe Paraskevopoulou and Anvay Grover
(Northeastern University, USA; University of Wisconsin-Madison, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Statically Bounded-Memory Delayed Sampling for Probabilistic Streams
Eric Atkinson ORCID logo, Guillaume BaudartORCID logo, Louis Mandel ORCID logo, Charles Yuan ORCID logo, and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA; Inria, France; ENS, France; PSL University, France; IBM Research, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Data-Driven Abductive Inference of Library Specifications
Zhe Zhou ORCID logo, Robert Dickerson, Benjamin DelawareORCID logo, and Suresh Jagannathan ORCID logo
(Purdue University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Formal Verification of High-Level Synthesis
Yann HerklotzORCID logo, James D. Pollard ORCID logo, Nadesh Ramanathan ORCID logo, and John Wickerson ORCID logo
(Imperial College London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Program Analysis via Efficient Symbolic Abstraction
Peisen YaoORCID logo, Qingkai Shi, Heqing Huang, and Charles ZhangORCID logo
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version
Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi ORCID logo, Max WillseyORCID logo, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock ORCID logo
(University of Washington, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
The Semantics of Shared Memory in Intel CPU/FPGA Systems
Dan IorgaORCID logo, Alastair F. DonaldsonORCID logo, Tyler Sorensen ORCID logo, and John Wickerson ORCID logo
(Imperial College London, UK; University of California at Santa Cruz, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Translating C to Safer Rust
Mehmet Emre ORCID logo, Ryan Schroeder, Kyle Dewey ORCID logo, and Ben Hardekopf
(University of California at Santa Barbara, USA; California State University at Northridge, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
One Down, 699 to Go: or, Synthesising Compositional Desugarings
Sándor Bartha, James Cheney ORCID logo, and Vaishak Belle ORCID logo
(University of Edinburgh, UK; Alan Turing Institute, UK)
Publisher's Version Published Artifact Artifacts Available
Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
Stefanos Chaliasos, Thodoris Sotiropoulos ORCID logo, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis ORCID logo
(Athens University of Economics and Business, Greece; Technical University of Crete, Greece; University of Athens, Greece; Delft University of Technology, Netherlands)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming
Malte Viering, Raymond Hu, Patrick EugsterORCID logo, and Lukasz Ziarek
(TU Darmstadt, Germany; Queen Mary University of London, UK; USI Lugano, Switzerland; Purdue University, USA; University at Buffalo, USA)
Publisher's Version Artifacts Reusable Artifacts Functional
What We Eval in the Shadows: A Large-Scale Study of Eval in R Programs
Aviral Goel ORCID logo, Pierre Donat-BouilludORCID logo, Filip Křikava, Christoph M. Kirsch, and Jan Vitek ORCID logo
(Northeastern University, USA; Czech Technical University, Czechia; University of Salzburg, Austria)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Gradually Structured Data
Stefan Malewski, Michael Greenberg ORCID logo, and Éric TanterORCID logo
(University of Chile, Chile; Stevens Institute of Technology, USA; IMFD, Chile)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional
Transitioning from Structural to Nominal Code with Efficient Gradual Typing
Fabian MuehlboeckORCID logo and Ross TateORCID logo
(IST Austria, Austria; Cornell University, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional
Compilation of Sparse Array Programming Models
Rawn Henry, Olivia Hsu ORCID logo, Rohan Yadav, Stephen ChouORCID logo, Kunle Olukotun ORCID logo, Saman AmarasingheORCID logo, and Fredrik KjolstadORCID logo
(Massachusetts Institute of Technology, USA; Stanford University, USA)
Publisher's Version Info
SpecSafe: Detecting Cache Side Channels in a Speculative World
Robert Brotzman, Danfeng Zhang, Mahmut Taylan Kandemir, and Gang Tan
(Pennsylvania State University, USA)
Publisher's Version
Coarsening Optimization for Differentiable Programming
Xipeng ShenORCID logo, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, and Shannon Yang
(North Carolina State University, USA; Facebook, USA)
Publisher's Version
Specifying and Testing GPU Workgroup Progress Models
Tyler Sorensen ORCID logo, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson ORCID logo, Margaret Martonosi, and Alastair F. DonaldsonORCID logo
(University of California at Santa Cruz, USA; Princeton University, USA; Google, USA; Imperial College London, UK)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, and Akash Lal
(Informal Systems, France; Microsoft, India; IIT Hyderabad, India; IRIF, France; University of Paris, France; CNRS, France; Microsoft Research, India)
Publisher's Version Published Artifact Artifacts Available
Durable Functions: Semantics for Stateful Serverless
Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos KallasORCID logo, Connor McMahon, and Christopher S. Meiklejohn
(Microsoft Research, USA; Microsoft Azure, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)
Publisher's Version
Gauss: Program Synthesis by Reasoning over Graphs
Rohan Bavishi ORCID logo, Caroline Lemieux, Koushik Sen, and Ion Stoica
(University of California at Berkeley, USA)
Publisher's Version
A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
Paul HeORCID logo, Eddy Westbrook, Brent Carmer, Chris Phifer ORCID logo, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve ZdancewicORCID logo
(University of Pennsylvania, USA; Galois, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode
Haoran Xu and Fredrik KjolstadORCID logo
(Stanford University, USA)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional
Study of the Subtyping Machine of Nominal Subtyping with Variance
Ori Roth
(Technion, Israel)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
Didier Ishimwe ORCID logo, KimHao NguyenORCID logo, and ThanhVu NguyenORCID logo
(University of Nebraska-Lincoln, USA; George Mason University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf
(University of Waterloo, Canada; Purdue University, USA)
Publisher's Version
Static Detection of Silent Misconfigurations with Deep Interaction Analysis
Jialu Zhang, Ruzica Piskac ORCID logo, Ennan Zhai, and Tianyin Xu ORCID logo
(Yale University, USA; Alibaba Group, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version Artifacts Functional
Interpretable Noninterference Measurement and Its Application to Processor Designs
Ziqiao Zhou and Michael K. Reiter
(Microsoft Research, USA; Duke University, USA)
Publisher's Version Info
Reconciling Optimization with Secure Compilation
Son Tuan Vu, Albert Cohen ORCID logo, Arnaud De Grandmaison, Christophe Guillon, and Karine Heydemann
(Sorbonne University, France; CNRS, France; LIP6, France; Google, France; ARM, France; STMicroelectronics, France)
Publisher's Version
Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
Florian Lanzinger ORCID logo, Alexander Weigl ORCID logo, Mattias Ulbrich ORCID logo, and Werner DietlORCID logo
(KIT, Germany; University of Waterloo, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
VESPA: Static Profiling for Binary Optimization
Angélica Aparecida Moreira ORCID logo, Guilherme Ottoni, and Fernando Magno Quintão Pereira ORCID logo
(Federal University of Minas Gerais, Brazil; Facebook, USA)
Publisher's Version Published Artifact Artifacts Available
Modular Specification and Verification of Closures in Rust
Fabian Wolff, Aurel Bílý ORCID logo, Christoph MathejaORCID logo, Peter Müller ORCID logo, and Alexander J. Summers ORCID logo
(ETH Zurich, Switzerland; University of British Columbia, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Rich Specifications for Ethereum Smart Contract Verification
Christian Bräm, Marco Eilers ORCID logo, Peter Müller ORCID logo, Robin Sierra, and Alexander J. Summers ORCID logo
(ETH Zurich, Switzerland; University of British Columbia, Canada)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity
Tian Tan, Yue Li, Xiaoxing Ma, Chang XuORCID logo, and Yannis Smaragdakis ORCID logo
(Nanjing University, China; University of Athens, Greece)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)
Guy L. Steele Jr. ORCID logo and Sebastiano Vigna ORCID logo
(Oracle Labs, USA; University of Milan, Italy)
Publisher's Version
Permchecker: A Toolchain for Debugging Memory Managers with Typestate
Karl CronburgORCID logo and Samuel Z. Guyer
(Tufts University, USA)
Publisher's Version
Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation
Artem PelenitsynORCID logo, Julia BelyakovaORCID logo, Benjamin Chung ORCID logo, Ross TateORCID logo, and Jan VitekORCID logo
(Northeastern University, USA; Cornell University, USA; Czech Technical University, Czechia)
Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Artifacts Functional
A Derivative-Based Parser Generator for Visibly Pushdown Grammars
Xiaodong Jia ORCID logo, Ashish Kumar ORCID logo, and Gang TanORCID logo
(Pennsylvania State University, USA)
Publisher's Version
Generative Type-Aware Mutation for Testing SMT Solvers
Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su ORCID logo
(École Polytechnique, France; ETH Zurich, Switzerland; East China Normal University, China)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
LooPy: Interactive Program Synthesis with Control Structures
Kasra Ferdowsifard ORCID logo, Shraddha BarkeORCID logo, Hila PelegORCID logo, Sorin LernerORCID logo, and Nadia PolikarpovaORCID logo
(University of California at San Diego, USA; Technion, Israel)
Publisher's Version Published Artifact Artifacts Available
Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget Sets
Michael D. BrownORCID logo, Matthew Pruett, Robert Bigelow, Girish Mururu, and Santosh Pande ORCID logo
(Georgia Institute of Technology, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
How Statically-Typed Functional Programmers Write Code
Justin LubinORCID logo and Sarah E. ChasinsORCID logo
(University of California at Berkeley, USA)
Publisher's Version
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs
Ting Su ORCID logo, Yichen Yan, Jue WangORCID logo, Jingling Sun ORCID logo, Yiheng Xiong, Geguang Pu, Ke Wang, and Zhendong Su ORCID logo
(East China Normal University, China; Nanjing University, China; Visa Research, USA; ETH Zurich, Switzerland)
Publisher's Version
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind KulkarniORCID logo, and Roopsha Samanta
(Purdue University, USA; CISPA, Germany)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based Synthesis
Kia Rahmani, Mohammad Raza ORCID logo, Sumit GulwaniORCID logo, Vu LeORCID logo, Daniel Morris, Arjun Radhakrishna ORCID logo, Gustavo Soares, and Ashish Tiwari ORCID logo
(Purdue University, USA; Microsoft, USA)
Publisher's Version
Compacting Points-To Sets through Object Clustering
Mohamad Barbar and Yulei SuiORCID logo
(University of Technology Sydney, Australia; CSIRO’s Data61, Australia)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Automatic Migration from Synchronous to Asynchronous JavaScript APIs
Satyajit Gokhale, Alexi Turcotte ORCID logo, and Frank Tip
(Northeastern University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries
Xiang Gao, Arjun Radhakrishna ORCID logo, Gustavo Soares, Ridwan ShariffdeenORCID logo, Sumit GulwaniORCID logo, and Abhik RoychoudhuryORCID logo
(National University of Singapore, Singapore; Microsoft, USA)
Publisher's Version
FPL: Fast Presburger Arithmetic through Transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser ORCID logo
(IIIT Hyderabad, India; ETH Zurich, Switzerland; University of Edinburgh, UK)
Publisher's Version Published Artifact Artifacts Available
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos ORCID logo, Konstantinos Triantafyllou, and Ilias Tsatiris ORCID logo
(University of Athens, Greece; University of Malta, Malta)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
The Reads-From Equivalence for the TSO and PSO Memory Models
Truc Lam Bui, Krishnendu Chatterjee ORCID logo, Tushar Gautam, Andreas PavlogiannisORCID logo, and Viktor Toman
(Comenius University Bratislava, Slovakia; IST Austria, Austria; IIT Bombay, India; Aarhus University, Denmark)
Publisher's Version
JavaDL: Automatically Incrementalizing Java Bug Pattern Detection
Alexandru Dura ORCID logo, Christoph ReichenbachORCID logo, and Emma Söderberg ORCID logo
(Lund University, Sweden)
Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Artifacts Functional
Programming and Execution Models for Parallel Bounded Exhaustive Testing
Nader Al Awar, Kush Jain, Christopher J. Rossbach ORCID logo, and Milos Gligoric
(University of Texas at Austin, USA; Katana Graph, USA)
Publisher's Version
Generalizable Synthesis through Unification
Ruyi Ji, Jingtao Xia, Yingfei Xiong ORCID logo, and Zhenjiang Hu
(Peking University, China)
Publisher's Version Published Artifact Artifacts Available

proc time: 21.46