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 $\textsf{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 \textsf{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.
翻译:我们研究线性一致性监测问题,即判断给定的数据结构并发历史是否等价于同一数据结构的某个顺序执行。一般而言,该问题是$\textsf{NP}$-困难的,即使对于寄存器等简单对象也是如此。近期工作已识别出受限历史类(特别是无歧义和区分历史)的可处理情形。我们从细粒度参数化视角重新审视可处理边界。结果表明,对于栈、队列、优先队列和映射等广泛数据结构类,当以进程数为参数时,线性一致性监测是固定参数可处理的。具体而言,我们给出的算法运行时间为$O(c^{k} \cdot \textsf{poly}(n))$,其中$n$为历史规模,$k$为进程数,$c$为常数,在$k$较小时可实现高效性能。我们的方法将线性一致性监测归约为图上的语言可达性问题,即判断带标记图是否存在路径,其标记序列属于固定语言$L$。我们识别出能够刻画上述数据结构顺序规约的语言类,并证明在并发历史诱导的图结构上,语言可达性是可高效求解的。本结果补充了先前的困难性结论与现有可处理子类,并提供了统一算法框架。我们实现了所提方法,并证明相较最坏情况呈指数复杂度的现有算法,该方法可显著提升运行性能。