{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:41Z","timestamp":1784199941838,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100001862","name":"The Swedish Research Council","doi-asserted-by":"crossref","award":["2020-04430"],"award-info":[{"award-number":["2020-04430"]}],"id":[{"id":"10.13039\/501100001862","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    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 \ud835\udcde(\ud835\udc5b\n                    <jats:sup>2<\/jats:sup>\n                    ), \ud835\udcde(\ud835\udc5b \ud835\udc59\ud835\udc5c\ud835\udc54 \ud835\udc5b), and \ud835\udcde(\ud835\udc5b), respectively, where \ud835\udc5b 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 \ud835\udc3f\ud835\udc56\ud835\udc40\ud835\udc5c (Linearizability Monitor). We evaluate \ud835\udc3f\ud835\udc56\ud835\udc40\ud835\udc5c and compare it with the state-of-the-art tool \ud835\udc49\ud835\udc56\ud835\udc5c\ud835\udc59\ud835\udc56\ud835\udc5b \u2013 whose correctness proofs we have found errors in \u2013 which checks for linearizability violations. Our experimental evaluation confirms that \ud835\udc3f\ud835\udc56\ud835\udc40\ud835\udc5c outperforms \ud835\udc49\ud835\udc56\ud835\udc5c\ud835\udc59\ud835\udc56\ud835\udc5b regarding both efficiency and scalability.\n                  <\/jats:p>","DOI":"10.1145\/3729328","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1937-1960","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Linearizability Monitoring"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"},{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1762-8061","authenticated-orcid":false,"given":"Samuel","family":"Grahn","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7897-601X","authenticated-orcid":false,"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0925-398X","authenticated-orcid":false,"given":"Shankaranarayanan","family":"Krishna","sequence":"additional","affiliation":[{"name":"IIT Bombay, Mumbai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-6858-6605","authenticated-orcid":false,"given":"Om Swostik","family":"Mishra","sequence":"additional","affiliation":[{"name":"IIT Bombay, Mumbai, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"324","article-title":"An Integrated Specification and Verification Technique for Highly Concurrent Data Structures","author":"Abdulla P.A.","year":"2013","unstructured":"P.A. Abdulla, F. Haziza, L. Hol\u00edk, B. Jonsson, and A. Rezine. 2013. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In TACAS. 324\u2013338.","journal-title":"TACAS"},{"key":"e_1_3_2_3_2","article-title":"Fragment Abstraction for Concurrent Shape Analysis","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla, Bengt Jonsson, and Cong Quy Trinh. 2018. Fragment Abstraction for Concurrent Shape Analysis. In ESOP (LNCS).","journal-title":"ESOP (LNCS)"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Daphna Amit Noam Rinetzky Thomas W. Reps Mooly Sagiv and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In Computer Aided Verification 19th International Conference CAV 2007 Berlin Germany \ud835\udd0duly 3\u20137 2007 (Lecture Notes in Computer Science Vol. 4590) Werner Damm and Holger Hermanns (Eds.). Springer 477\u2013490. doi:10.1007\/978-3-540-73368-3_49","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)00176-Y"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Michael Emmi Constantin Enea and Jad Hamza. 2015. Tractable Refinement Checking for Concurrent Objects. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015 Mumbai India \ud835\udd0danuary 15\u201317 2015 Sriram K. Rajamani and David Walker (Eds.). ACM 651\u2013662. doi:10.1145\/2676726.2677000","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Sebastian Burckhardt Chris Dern Madanlal Musuvathi and Roy Tan. 2010. Line-up: a complete and automatic linearizability checker. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2010 Toronto Ontario Canada \ud835\udd0dune 5\u201310 2010 Benjamin G. Zorn and Alexander Aiken (Eds.). ACM 330\u2013340. doi:10.1145\/1806596.1806634","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_3_2_9_2","unstructured":"R.K. Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated Thomas J. Watson Research Center. https:\/\/books.google.se\/books?id=YQg3AAAACAAJ."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Mike Dodds Andreas Haas and Christoph M. Kirsch. 2015. A Scalable Correct Time-Stamped Stack. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015 Mumbai India \ud835\udd0danuary 15\u201317 2015 Sriram K. Rajamani and David Walker (Eds.). ACM 233\u2013246. doi:10.1145\/2676726.2676963","DOI":"10.1145\/2676726.2676963"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Cezara Drago\u015f Ashutosh Gupta and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification - 25th International Conference (CAV 2013) Saint Petersburg Russia \ud835\udd0duly 13\u201319 2013 (Lecture Notes in Computer Science Vol. 8044) Natasha Sharygina and Helmut Veith (Eds.). Springer 174\u2013190. doi:10.1007\/978-3-642-39799-8_11","DOI":"10.1007\/978-3-642-39799-8_11"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158113"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Michael Emmi Constantin Enea and Jad Hamza. 2015. Monitoring refinement via symbolic reasoning. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015) Portland OR USA \ud835\udd0dune 15\u201317 2015 David Grove and Stephen M. Blackburn (Eds.). ACM 260\u2013269. doi:10.1145\/2737924.2737983","DOI":"10.1145\/2737924.2737983"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Samuel Grahn. 2025. Limo Artifact. doi:10.5281\/zenodo.15258056","DOI":"10.5281\/zenodo.15258056"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2410.04581"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-003-0117-6"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Thomas A. Henzinger Ali Sezgin and Viktor Vafeiadis. 2013. Aspect-Oriented Linearizability Proofs. In CONCUR 2013 - Concurrency Theory - 24th International Conference Buenos Aires Argentina August 27\u201330 2013 (Lecture Notes in Computer Science Vol. 8052) Pedro R. D\u2019Argenio and Hern\u00e1n C. Melgratti (Eds.). Springer 242\u2013256. doi:10.1007\/978-3-642-40184-8_18","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger Ali Sezgin and Viktor Vafeiadis. 2013. Aspect-Oriented Linearizability Proofs. In CONCUR 2013 \u2013 Concurrency Theory Pedro R. D\u2019Argenio and Hern\u00e1n Melgratti (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 242\u2013256.","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_21_2","article-title":"Faster linearizability checking via $P$-compositionality","author":"Horn Alex","year":"2015","unstructured":"Alex Horn and Daniel Kroening. 2015. Faster linearizability checking via $P$-compositionality. CoRR abs\/1504.00204 (2015). arXiv:1504.00204. http:\/\/arxiv.org\/abs\/1504.00204","journal-title":"CoRR"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"Qiaowen Jia Yi Lv Peng Wu Bohua Zhan Jifeng Hao Hong Ye and Chao Wang. 2023. VeriLin: A Linearizability Checker for Large-Scale Concurrent Objects. In International Symposium on Theoretical Aspects of Software Engineering. Springer 202\u2013220.","DOI":"10.1007\/978-3-031-35257-7_12"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1609.01171"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201913) Seattle WA USA \ud835\udd0dune 16\u201319 2013 Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM 459\u2013470. doi:10.1145\/2491956.2462189","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3928"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Maged M. Michael and Michael L. Scott. 1996. Simple Fast and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing PODC 1996 Philadelphia Pennsylvania USA May 23\u201326 1996 James E. Burns and Yoram Moses (Eds.). ACM 267\u2013275. doi:10.1145\/248052.248106","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn Noam Rinetzky Martin T. Vechev Eran Yahav and Greta Yorsh. 2010. Verifying linearizability with hindsight. In Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing PODC 2010 Zurich Switzerland \ud835\udd0duly 25\u201328 2010 Andr\u00e9 W. Richa and Rachid Guerraoui (Eds.). ACM 85\u201394. doi:10.1145\/1835698.1835722","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Christina L. Peterson Victor Cook and Damian Dechev. 2021. Concurrent Correctness in Vector Space. In Verification Model Checking and Abstract Interpretation - 22nd International Conference VMCAI 2021 Copenhagen Denmark \ud835\udd0danuary 17\u201319 2021 Proceedings (Lecture Notes in Computer Science Vol. 12597) Fritz Henglein Sharon Shoham and Yakir Vizel (Eds.). Springer 151\u2013173. doi:10.1007\/978-3-030-67067-2_8","DOI":"10.1007\/978-3-030-67067-2_8"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Ilya Sergey Aleksandar Nanevski and Aminyad Banerjee. 2015. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation Portland OR USA \ud835\udd0dune 15\u201317 2015 David Grove and Stephen M. Blackburn (Eds.). ACM 77\u201387. doi:10.1145\/2737924.2737964","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ohad Shacham Nathan Grasso Bronson Alex Aiken Mooly Sagiv Martin T. Vechev and Eran Yahav. 2011. Testing atomicity of composed concurrent operations. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications OOPSLA 2011 part of SPLASH 2011 Portland OR USA October 22 \u2013 27 2011 Cristina Videira Lopes and Kathleen Fisher (Eds.). ACM 51\u201364. doi:10.1145\/2048066.2048073","DOI":"10.1145\/2048066.2048073"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In Computer Aided Verification 22nd International Conference CAV 2010 Edinburgh UK \ud835\udd0duly 15\u201319 2010. Proceedings (Lecture Notes in Computer Science Vol. 6174) Tayssir Touili Byron Cook and Paul B. Jackson (Eds.). Springer 450\u2013464. doi:10.1007\/978-3-642-14295-6_40","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1993.1015"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Pierre Wolper. 1986. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In POPL. ACM Press 184\u2013193. doi:10.1145\/152644.512661","DOI":"10.1145\/152644.512661"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Shao Jie Zhang. 2011. Scalable automatic linearizability checking. In Proceedings of the 33rd International Conference on Software Engineering ICSE 2011 Waikiki Honolulu HI USA May 21\u201328 2011 Richard N. Taylor Harald C. Gall and Nenad Medvidovic (Eds.). ACM 1185\u20131187. doi:10.1145\/1985793.1986037","DOI":"10.1145\/1985793.1986037"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729328","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:38Z","timestamp":1784196398000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729328"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":33,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729328"],"URL":"https:\/\/doi.org\/10.1145\/3729328","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}