
arXiv: 2509.17795
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.
FOS: Computer and information sciences, Datatypes, Computer and Information Sciences, Abstract data types, Formella metoder, Testing, Linearization, Multi-sets, Data- och informationsvetenskap, Formal Methods, Computational complexity, Queueing theory, Data independence, Time complexity, Monitoring algorithms, Linearizability, Standard assumptions, Programming Languages, Concurrent Data Structures, Correctness proofs, Abstract data, Programming Languages (cs.PL)
FOS: Computer and information sciences, Datatypes, Computer and Information Sciences, Abstract data types, Formella metoder, Testing, Linearization, Multi-sets, Data- och informationsvetenskap, Formal Methods, Computational complexity, Queueing theory, Data independence, Time complexity, Monitoring algorithms, Linearizability, Standard assumptions, Programming Languages, Concurrent Data Structures, Correctness proofs, Abstract data, Programming Languages (cs.PL)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 4 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
