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

Clients reason about the behavior of concurrent data structure libraries such as sets, queues, or stacks using specifications that capture well-understood correctness conditions, such as linearizability. The implementation of these libraries, however, focused as they are on performance, may additionally exploit relaxed memory behavior allowed by the language or underlying hardware that weaken the strong ordering and visibility constraints on shared-memory accesses that would otherwise be imposed by a sequentially consistent (SC) memory model. As an alternative to developing new specification and verification mechanisms for reasoning about libraries under relaxed memory model, we instead consider the orthogonal problem of \emph{library robustness}, a property that holds when all possible behaviors of a library implementation under relaxed memory model are also possible under SC. In this paper, we develop a new \emph{automated} technique for verifying robustness of library implementations in the context of a C11-style memory model. This task is challenging because a most-general client may invoke an unbounded number of concurrently executing library operations that can manipulate an unbounded number of shared locations. We establish a novel inductive technique for verifying library robustness that leverages prior work on the robustness problem for the C11 memory model based on the search for a non-robustness witness under SC executions. We crucially rely on the fact that this search is carried out over SC executions, and use high-level SC specifications (including linearizability) of the library to verify the absence of a non-robustness witness. Our technique is compositional - we show how we can safely preserve robustness of multiple interacting library implementations and clients using additional SC fences to guarantee robustness of entire executions. Experimental results on a number of complex realistic library implementations demonstrate the feasibility of our approach.

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