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 Preprint 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 Article Search 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 Article Search Artifacts Available Artifacts Functional
Semantic Programming by Example with Pre-trained Models
Gust Verbruggen ORCID logo, Vu Le, and Sumit Gulwani
(KU Leuven, Belgium; Microsoft, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Promises Are Made to Be Broken: Migrating R to Strict Semantics
Aviral Goel ORCID logo, Jan Ječmen, Sebastián Krynski, Olivier Flückiger ORCID logo, and Jan VitekORCID logo
(Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version Article Search 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 Article Search 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 Article Search 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 Article Search
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 Article Search 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 Article Search 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 Article Search 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 Article Search 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-Kelley
(Massachusetts Institute of Technology, USA; Adobe, USA; University of California at San Diego, USA)
Publisher's Version Article Search
Relational Nullable Types with Boolean Unification
Magnus Madsen and Jaco van de Pol
(Aarhus University, Denmark)
Publisher's Version Article Search
Solver-Based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane AndersonORCID logo, Michael Greenberg ORCID logo, and Arjun Guha
(University of Massachusetts at Amherst, USA; Wellesley College, USA; Stevens Institute of Technology, USA; Northeastern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
UDF to SQL Translation through Compositional Lazy Inductive Synthesis
Guoqiang Zhang, Yuanchao Xu, Xipeng ShenORCID logo, and Işıl Dillig
(North Carolina State University, USA; University of Texas at Austin, USA)
Publisher's Version Article Search
Verifying Concurrent Multicopy Search Structures
Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA; Microsoft Research, UK)
Publisher's Version Article Search 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 Article Search Artifacts Available Artifacts Functional
Statically Bounded-Memory Delayed Sampling for Probabilistic Streams
Eric Atkinson ORCID logo, Guillaume Baudart, Louis Mandel, 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 Article Search Archive submitted (470 kB) Artifacts Available Artifacts Reusable Artifacts Functional
Data-Driven Abductive Inference of Library Specifications
Zhe Zhou ORCID logo, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA)
Publisher's Version Article Search 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 Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Program Analysis via Efficient Symbolic Abstraction
Peisen Yao ORCID logo, Qingkai Shi, Heqing Huang, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)
Publisher's Version Article Search
Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi, Max WillseyORCID logo, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock
(University of Washington, USA)
Publisher's Version Article Search 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 Preprint 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 Article Search Archive submitted (1.4 MB) 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 Preprint Artifacts Available
Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis
(Athens University of Economics and Business, Greece; Technical University of Crete, Greece; University of Athens, Greece; Delft University of Technology, Netherlands)
Publisher's Version Article Search 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 Article Search 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
(Northeastern University, USA; Czech Technical University, Czechia; University of Salzburg, Austria)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Gradually Structured Data
Stefan Malewski, Michael Greenberg ORCID logo, and Éric Tanter
(University of Chile, Chile; Stevens Institute of Technology, USA; IMFD, Chile)
Publisher's Version Article Search 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 Preprint Info Artifacts Available Artifacts Functional
Compilation of Sparse Array Programming Models
Rawn Henry, Olivia Hsu ORCID logo, Rohan Yadav, Stephen Chou, Kunle Olukotun, Saman Amarasinghe, and Fredrik Kjolstad
(Massachusetts Institute of Technology, USA; Stanford University, USA)
Publisher's Version Article Search Archive submitted (1 MB) 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 Article Search
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 Article Search
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 Article Search 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 Article Search Artifacts Available
Durable Functions: Semantics for Stateful Serverless
Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, and Christopher S. Meiklejohn
(Microsoft Research, USA; Microsoft Azure, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)
Publisher's Version Article Search
Gauss: Program Synthesis by Reasoning over Graphs
Rohan Bavishi, Caroline Lemieux, Koushik Sen, and Ion Stoica
(University of California at Berkeley, USA)
Publisher's Version Article Search
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 Article Search Artifacts Available Artifacts Functional
Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode
Haoran Xu and Fredrik Kjolstad
(Stanford University, USA)
Publisher's Version Preprint Archive submitted (200 kB) Info Artifacts Available Artifacts Reusable Artifacts Functional
Study of the Subtyping Machine of Nominal Subtyping with Variance
Ori Roth
(Technion, Israel)
Publisher's Version Preprint 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 Article Search Archive submitted (8.9 MB) 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 Article Search
Static Detection of Silent Misconfigurations with Deep Interaction Analysis
Jialu Zhang, Ruzica Piskac, Ennan Zhai, and Tianyin Xu ORCID logo
(Yale University, USA; Alibaba Group, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article Search 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 Article Search 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 Article Search
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 Article Search Archive submitted (350 kB) 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 PereiraORCID logo
(Federal University of Minas Gerais, Brazil; Facebook, USA)
Publisher's Version Article Search 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 Article Search 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 Article Search 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 Xu, and Yannis Smaragdakis
(Nanjing University, China; University of Athens, Greece)
Publisher's Version Article Search 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 Article Search
Permchecker: A Toolchain for Debugging Memory Managers with Typestate
Karl CronburgORCID logo and Samuel Z. Guyer
(Tufts University, USA)
Publisher's Version Preprint
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 Preprint 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 Article Search
Generative Type-Aware Mutation for Testing SMT Solvers
Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su
(École Polytechnique, France; ETH Zurich, Switzerland; East China Normal University, China)
Publisher's Version Article Search 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 Article Search 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
(Georgia Institute of Technology, USA)
Publisher's Version Preprint 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 Article Search
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs
Ting Su ORCID logo, Yichen Yan, Jue Wang, Jingling Sun ORCID logo, Yiheng Xiong, Geguang Pu, Ke Wang, and Zhendong Su
(East China Normal University, China; Nanjing University, China; Visa Research, USA; ETH Zurich, Switzerland)
Publisher's Version Article Search
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 Article Search 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, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, and Ashish Tiwari
(Purdue University, USA; Microsoft, USA)
Publisher's Version Preprint
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 Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Automatic Migration from Synchronous to Asynchronous JavaScript APIs
Satyajit Gokhale, Alexi Turcotte, and Frank Tip
(Northeastern University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Reusable Artifacts Functional
APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries
Xiang Gao, Arjun Radhakrishna, Gustavo Soares, Ridwan ShariffdeenORCID logo, Sumit Gulwani, and Abhik RoychoudhuryORCID logo
(National University of Singapore, Singapore; Microsoft, USA)
Publisher's Version Article Search
FPL: Fast Presburger Arithmetic through Transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser
(IIIT Hyderabad, India; ETH Zurich, Switzerland; University of Edinburgh, UK)
Publisher's Version Article Search Artifacts Available
Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, and Ilias Tsatiris
(University of Athens, Greece; University of Malta, Malta)
Publisher's Version Article Search 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 Article Search
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 Article Search Artifacts Available Artifacts Reusable Artifacts Functional
Programming and Execution Models for Parallel Bounded Exhaustive Testing
Nader Al Awar, Kush Jain, Christopher J. Rossbach, and Milos Gligoric
(University of Texas at Austin, USA; Katana Graph, USA)
Publisher's Version Article Search
Generalizable Synthesis through Unification
Ruyi Ji, Jingtao Xia, Yingfei Xiong, and Zhenjiang Hu
(Peking University, China)
Publisher's Version Article Search Artifacts Available

proc time: 14.93