Mon 19 Jun 2023 16:40 - 17:00 at Cypress 2 - PLDI: Concurrency & Parallelism Chair(s): Calin Cascaval

Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. Accesses to the database are typically enclosed in transactions that allow computations on shared data to be isolated from other concurrent computations and resilient to failures. Modern databases trade isolation for performance. The weaker the isolation level is, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors.

In this work, we propose stateless model checking algorithms for studying correctness of such applications that rely on dynamic partial order reduction. These algorithms work for a number of widely-used weak isolation levels, including Read Committed, Causal Consistency, Snapshot Isolation, and Serializability. We show that they are complete, sound and optimal, and run with polynomial memory consumption in all cases. We report on an implementation of these algorithms in the context of Java Pathfinder applied to a number of challenging applications drawn from the literature of distributed systems and databases.

Mon 19 Jun

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
PLDI: Concurrency & ParallelismPLDI Research Papers at Cypress 2
Chair(s): Calin Cascaval Google Research

#pldi-mon-1600-concurrency-cypress Discord icon small YouTube icon small

16:00
20m
Talk
Type-Checking CRDT Convergence
PLDI Research Papers
George Zakhour University of St.Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen
DOI Pre-print
16:20
20m
Talk
Reliable Actors with Retry Orchestration
PLDI Research Papers
Olivier Tardieu IBM Research, David Grove IBM Research, Gheorghe-Teodor Bercea IBM Research, Paul Castro IBM Research, Jaroslaw Cwiklik IBM Research, Edward Epstein IBM Research
DOI
16:40
20m
Talk
Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels
PLDI Research Papers
Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIX, CNRS, Ecole Polytechnique, Enrique Román-Calvo Université Paris Cité - CNRS - IRIF
DOI
17:00
20m
Talk
Responsive Parallelism with Synchronization
PLDI Research Papers
Stefan K. Muller Illinois Institute of Technology, Kyle Singer Washington University in St. Louis, USA, Devyn Terra Keeney Illinois Institute of Technology, Andrew Neth Illinois Institute of Technology, Kunal Agrawal Washington University in St. Louis, USA, I-Ting Angelina Lee Washington University in St. Louis, USA, Umut A. Acar Carnegie Mellon University
DOI
17:20
20m
Talk
Parallelism in a Region Inference Context
PLDI Research Papers
Martin Elsman University of Copenhagen, Denmark, Troels Henriksen University of Copenhagen, Denmark
DOI
17:40
20m
Talk
Performal: Formal Verification of Latency Properties for Distributed Systems
PLDI Research Papers
Nuda Zhang University of Michigan, Upamanyu Sharma Massachusetts Institute of Technology, Manos Kapritsos University of Michigan, USA
DOI