paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Fixed Parameter Tractable Linearizability Monitoring

固定参数可处理的线性一致性监测
PLDI 10(PLDI)2026匹配度 2/10 · 该论文是并发程序验证中线性一致性监测的固定参数可处理性理论工作,与用户画像核心关注的 LLM/Agent 与静态分析/形式化验证的交叉、浮点程序分析、贝叶斯程序分析均无直接关联;仅在“形式化验证”大领域上有边缘重叠,且不涉及 LLM/Agent 作为工具或对象。引用 0 inbox
Zheng Han Lee, Umang Mathur
crossref: 2026-09-10

AI 速览

一句话:证明以进程数为参数时,栈、队列、优先队列和映射的线性一致性监测是固定参数可处理的。

线性一致性监测判断给定并发历史是否等价于数据结构的某次顺序执行,一般 NP 难,即使对寄存器等简单对象;已有工作仅处理受限历史。本文从参数化视角重新审视可处理边界,证明对栈、队列、优先队列和映射等广泛数据结构,以进程数 k 为参数时线性一致性监测是固定参数可处理的,时间为 O(c^k·poly(n))(n 为历史长度)。方法将问题归约为图上的语言可达性:判断带标签图是否存在标签序列属于固定语言 L 的路径,并识别刻画上述数据结构顺序规约的语言类。作者实现原型并显著加速;结果补充既有难解性与可处理子类,提供统一框架。

问题
研究并发历史线性一致性监测的可处理边界:给定数据结构并发历史,判定其是否等价于某顺序执行;该问题一般 NP 难,需寻找受限或参数化高效算法。
方法
将线性一致性监测归约为带标签图上的语言可达性,识别刻画栈、队列、优先队列、映射等顺序规约的语言类,并设计按进程数 k 参数化的 FPT 算法。
评估
实现原型并在基准上与现有最坏情况指数级算法比较,显示运行时间显著降低;同时给出 O(c^k·poly(n)) 的理论保证。
原文摘要(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 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2509-05586,
  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}
}