一句话：为并发栈、队列、集合与多重集给出更快的线性一致性监控算法，纠正既有错误证明，并实现工具 LiMo。
本文重新审视并发栈、队列、集合与多重集的线性一致性监控问题：给定这些抽象数据类型实现的一段历史，判断其是否可线性化。作者分别给出栈、队列与（多）集合的监控算法，复杂度依次为 O(n²)、O(n log n) 与 O(n)，其中 n 为历史中操作数；栈与队列的结果在标准的数据无关假设下成立。相比已有工作，这些算法不仅将立方级复杂度降低，还解决了此前正确性证明缺失、证明有误或算法错误的问题——论文给出了反例，并为新算法提供详细正确性证明。作者在工具 LiMo 中实现了栈与队列算法，并与最先进工具 Violin（其正确性证明被本文指出有误）进行对比，实验表明 LiMo 在效率与可扩展性上均优于 Violin。
This paper revisits the fundamental problem of monitoring the linearizability of concurrent stacks, queues, sets, and multisets. Given a history of a library implementing one of these abstract data types, the monitoring problem is to answer whether the given history is linearizable. For stacks, queues, and (multi)sets, we present monitoring algorithms with complexities 𝓞(𝑛 2 ), 𝓞(𝑛 𝑙𝑜𝑔 𝑛), and 𝓞(𝑛), respectively, where 𝑛 is the number of operations in the input history. For stacks and queues, our results hold under the standard assumption of data-independence, i.e., the behavior of the library is not sensitive to the actual values stored in the data structure. Past works to solve the same problems have cubic time complexity and (more seriously) have correctness issues: they either (i) lack correctness proofs or (ii) the suggested correctness proofs are erroneous (we present counter-examples), or (iii) have incorrect algorithms. Our improved complexity results rely on substantially different algorithms for which we provide detailed proofs of correctness. We have implemented our stack and queue algorithms in 𝐿𝑖𝑀𝑜 (Linearizability Monitor). We evaluate 𝐿𝑖𝑀𝑜 and compare it with the state-of-the-art tool 𝑉𝑖𝑜𝑙𝑖𝑛 – whose correctness proofs we have found errors in – which checks for linearizability violations. Our experimental evaluation confirms that 𝐿𝑖𝑀𝑜 outperforms 𝑉𝑖𝑜𝑙𝑖𝑛 regarding both efficiency and scalability.
@article{paperbot3138,
title = {Efficient Linearizability Monitoring},
author = {Parosh Aziz Abdulla and Samuel Grahn and Bengt Jonsson and Shankaranarayanan Krishna and Om Swostik Mishra},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729328}
}