paperbot · PL 论文追踪

RSS

Fixed Parameter Tractable Linearizability Monitoring

PLDI 10(PLDI)2026
Zheng Han Lee, Umang Mathur

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

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 O ( c k · 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.

链接与引用

DOI 原文 ·

BibTeX
@article{paperbot3691,
  title = {Fixed Parameter Tractable Linearizability Monitoring},
  author = {Zheng Han Lee and Umang Mathur},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808315}
}