Fixed Parameter Tractable Linearizability Monitoring

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 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 𝑂 (𝑐 𝑘 • poly(𝑛)), where 𝑛 is the history size, 𝑘 is the number of processes, and 𝑐 is a constant, yielding efficient performance when 𝑘 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 𝐿. 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.

CCS Concepts: • Theory of computation → Theory and algorithms for application domains; • Computing methodologies → Concurrent computing methodologies; • Software and its engineering → Software verification and validation.