Fixed Parameter Tractable Linearizability Monitoring

Abstract

We study the linearizability monitoring problem, which asks whether a given history of a concurrent implementation of a data structure is linearizable, i.e., whether it is equivalent to a history generated by a sequential implementation of the same data structure. In general, this problem is known to be NP-hard, even for simple data structures such as registers. Recently, tractability results have been shown for subclasses of histories, most notably the class of unambiguous (also known as differentiated) histories. In this work, we revisit the tractability boundary from a fine-grained perspective. We show that, for a large class of data structures—including stacks, queues, priority queues, and maps—this problem is fixed-parameter tractable when treating the number of processes in the history as a parameter. More precisely, we show that linearizability monitoring for such data structures can be performed in time O(c^k · poly(n)), where n is the size of the history, k is the number of processes, and c is a constant. Thus, the problem can be solved efficiently when the number of processes is small. At a technical level, our algorithms proceed by reducing the linearizability monitoring problem for concurrent histories to language reachability over graphs. Given a fixed formal language L, this problem asks whether a graph G contains a path whose sequence of labels belongs to L. To this end, we identify classes of languages that capture the sequential specifications of a large class of data structures and for which language reachability is efficiently solvable on the class of graphs arising from linearizability monitoring. Our results complement prior hardness results and tractable subclass results for linearizability monitoring. We implement our algorithms and demonstrate runtime improvements over the current state-of-the-art general linearizability monitor, which exhibits worst-case exponential behavior.