Thu 24 Oct 2024 17:20 - 17:40 at IBR East - Concurrency Chair(s): Alex Potanin

Concurrent objects form the foundation of many applications that exploit multicore architectures and their importance has lead to informal correctness arguments, as well as formal proof systems. Correctness arguments (as found in the distributed computing literature) give intuitive descriptions of a few canonical executions or “scenarios” often each with only a few threads, yet it remains unknown as to whether these intuitive arguments have a formal grounding and extend to arbitrary interleavings over unboundedly many threads.

We present a novel proof technique for concurrent objects, based around identifying a small set of scenarios (representative, canonical interleavings), formalized as the commutativity quotient of a concurrent object. We next give an expression language for defining abstractions of the quotient in the form of regular or context-free languages that enable simple proofs of linearizability. These quotient expressions organize unbounded interleavings into a form more amenable to reasoning and make explicit the relationship between implementation-level contention/interference and ADT-level transitions.

We evaluate our work on numerous non-trivial concurrent objects from the literature (including the Michael-Scott queue, Elimination stack, SLS reservation queue, RDCSS and Herlihy-Wing queue). We show that quotients capture the diverse features/complexities of these algorithms, can be used even when linearization points are not straight-forward, correspond to original authors’ correctness arguments, and provide some new scenario-based arguments. Finally, we show that discovery of some object’s quotients reduces to two-thread reasoning and give an implementation that can derive candidate quotients expressions from source code.

Thu 24 Oct

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

16:00 - 17:40
ConcurrencyOOPSLA 2024 at IBR East
Chair(s): Alex Potanin Australian National University
16:00
20m
Talk
Concurrent Data Structures Made Easy
OOPSLA 2024
Callista Le Yale-NUS College, Kiran Gopinathan National University of Singapore, Lee Koon Wen Ahrefs, Seth Gilbert National University of Singapore, Ilya Sergey National University of Singapore
DOI
16:20
20m
Talk
Automated Verification of Parametric Channel-Based Process Communication
OOPSLA 2024
Georgian-Vlad Saioc Aarhus University, Julien Lange Royal Holloway, University of London, Anders Møller Aarhus University
DOI
16:40
20m
Talk
Automated Robustness Verification of Concurrent Data Structure Libraries Against Relaxed Memory Models
OOPSLA 2024
Kartik Nagar IIT Madras, Anmol Sahoo Purdue University, Romit Roy Chowdhury Chennai Mathematical Institute, Suresh Jagannathan Purdue University
DOI
17:00
20m
Talk
Verified Lock-Free Session Channels with Linking
OOPSLA 2024
Thomas Somers Radboud University Nijmegen, Robbert Krebbers Radboud University Nijmegen
DOI
17:20
20m
Talk
Scenario-based Proofs for Concurrent ObjectsRemote
OOPSLA 2024
Constantin Enea LIX, CNRS, Ecole Polytechnique, Eric Koskinen Stevens Institute of Technology
DOI