This program is tentative and subject to change.

Wed 17 Jun 2026 14:00 - 14:20 at Flatirons 3 - Concurrent Monitoring and Verification

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 Jun

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

13:40 - 15:20
Concurrent Monitoring and VerificationPLDI Research Papers at Flatirons 3
13:40
20m
Talk
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
20m
Talk
Fixed Parameter Tractable Linearizability Monitoring
PLDI Research Papers
Zheng Han Lee National University of Singapore, Umang Mathur National University of Singapore
DOI
14:20
20m
Talk
SuperCollider: Scalable and Effective Data Race Detection for CUDA
PLDI Research Papers
DOI
14:40
20m
Talk
Fast Atomicity Monitoring
PLDI Research Papers
Hünkar Can Tunç Uber, Yifan Dong Aarhus University, Andreas Pavlogiannis Aarhus University
DOI