This program is tentative and subject to change.
We study the linearizability monitoring problem, which asks whether a given concurrent history of a data structure is equivalent to some sequential execution of the same data structure. In general, this problem is $\mathsf{NP}$-hard, even for simple objects such as registers. Recent work has identified tractable cases for restricted classes of histories, notably unambiguous and differentiated histories.
We revisit the tractability boundary from a fine-grained, parameterized perspective. We show that for a broad class of data structures — including stacks, queues, priority queues, and maps—linearizability monitoring is fixed-parameter tractable when parameterized by the number of processes. Concretely, we give an algorithm running in time $O(c^{k} \cdot \mathsf{poly}(n))$, where $n$ is the history size, $k$ is the number of processes, and $c$ is a constant, yielding efficient performance when $k$ is small.
%
Our approach reduces linearizability monitoring to a language reachability problem on graphs, which asks whether a labeled graph admits a path whose label sequence belongs to a fixed language $L$. We identify classes of languages that capture the sequential specifications of the above data structures and show that language reachability is efficiently solvable on the graph structures induced by concurrent histories.
Our results complement prior hardness results and existing tractable subclasses, and provide a unified algorithmic framework. We implement our approach and demonstrate significant runtime improvements over existing algorithms, which exhibit exponential worst-case behavior.
This program is tentative and subject to change.
Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change
13:40 - 15:20 | |||
13:40 20mTalk | State Space Estimation for DPOR-Based Model Checkers PLDI Research Papers A. R. Balasubramanian MPI-SWS, Mohammad Hossein Khoshechin Jorshari MPI-SWS, Rupak Majumdar MPI-SWS, Umang Mathur National University of Singapore, Minjian Zhang University of Illinois Urbana-Champaign DOI | ||
14:00 20mTalk | Fixed Parameter Tractable Linearizability Monitoring PLDI Research Papers DOI | ||
14:20 20mTalk | SuperCollider: Scalable and Effective Data Race Detection for CUDA PLDI Research Papers Mark Stephenson NVIDIA, Sana Damani NVIDIA, Mohamed Tarek Ibn Ziad NVIDIA, Anis Ladram NVIDIA, Michael Garland NVIDIA DOI | ||
14:40 20mTalk | Fast Atomicity Monitoring PLDI Research Papers DOI | ||