Skip to content
Free planNo credit card requiredStart writing
AI for Research home
AI for Research home
Dashboard
Sign inGet started

article · Proceedings of the ACM on Programming Languages · 2025

Efficient Linearizability Monitoring

Parosh Aziz Abdulla, Sofia Grahn, Bengt Jönsson, Shankara Narayanan Krishna, Om Swostik Mishra

Cited by 2Open access

Abstract

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 ( n 2 ), ( n log n ), and ( n ), respectively, where n 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) have unsound correctness proofs (we present counter-examples of the correctness proofs), or (iii) have unsound 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 LiMo (Linearizability Monitor). We evaluate LiMo and compare it with the state-of-the-art tool Violin – whose correctness proofs we have found errors in – which checks for linearizability violations. Our experimental evaluation confirms that LiMo outperforms Violin regarding both efficiency and scalability.

Cite this paper

APA 7

Abdulla, P. A., Grahn, S., Jönsson, B., Krishna, S. N., & Mishra, O. S. (2025). Efficient Linearizability Monitoring. Proceedings of the ACM on Programming Languages, 9(PLDI), 1937–1960. https://doi.org/10.1145/3729328

MLA 9

Abdulla, Parosh Aziz, et al. “Efficient Linearizability Monitoring.” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, 2025, pp. 1937–60, https://doi.org/10.1145/3729328.

Chicago

Abdulla, Parosh Aziz, Sofia Grahn, Bengt Jönsson, Shankara Narayanan Krishna, and Om Swostik Mishra. 2025. “Efficient Linearizability Monitoring.” Proceedings of the ACM on Programming Languages 9 (PLDI): 1937–60. https://doi.org/10.1145/3729328.

Harvard

Abdulla, P.A. et al. (2025) ‘Efficient Linearizability Monitoring’, Proceedings of the ACM on Programming Languages, 9(PLDI), pp. 1937–1960. Available at: https://doi.org/10.1145/3729328.

BibTeX
@article{abdulla2025efficient,
  title = {{Efficient Linearizability Monitoring}},
  author = {Abdulla, Parosh Aziz and Grahn, Sofia and Jönsson, Bengt and Krishna, Shankara Narayanan and Mishra, Om Swostik},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  pages = {1937--1960},
  year = {2025},
  doi = {10.1145/3729328}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.

Related papers