{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:04Z","timestamp":1767929644420,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n            Linearizability has become the de facto standard for specifying correctness of implementations of concurrent data structures. While formally verifying such implementations remains challenging,\n            <jats:italic toggle=\"yes\">linearizability monitoring<\/jats:italic>\n            has emerged as a promising first step to rule out early problems in the development of custom implementations, and serves as a key component in approaches that stress test such implementations. In this work, we undertake an algorithmic investigation of the linearizability monitoring problem, which asks to check if an execution history obtained from a concurrent data structure implementation is linearizable.\n          <\/jats:p>\n          <jats:p>\n            While this problem is largely understood to be intractable in general, a systematic understanding of when it becomes tractable has remained elusive. We revisit this problem and first present a unified \u2018decrease-and-conquer\u2019 algorithmic framework for designing linearizability monitoring. At its heart, this framework asks to identify special\n            <jats:italic toggle=\"yes\">linearizability-preserving<\/jats:italic>\n            values in a given history \u2014 values whose presence yields an equi-linearizable sub-history (obtained by removing operations of such values), and whose absence indicates non-linearizability. More importantly, we prove that a polynomial time algorithm for the problem of identifying linearizability-preserving values, immediately yields a polynomial time algorithm for the linearizability monitoring problem, while conversely, intractability of this problem implies intractability of monitoring.\n          <\/jats:p>\n          <jats:p>\n            We demonstrate the effectiveness of our decrease-and-conquer framework by instantiating it for several popular concurrent data types \u2014 registers, sets, stacks, queues and priority queues \u2014 deriving polynomial time algorithms for them, under the (\n            <jats:italic toggle=\"yes\">unambiguity<\/jats:italic>\n            ) restriction that each insertion to the underlying data structure adds a distinct value. We further optimize these algorithms to achieve log-linear running time through the use of efficient data structures for amortizing the cost of solving induced sub-problems. Our implementation and evaluation on publicly available implementations of concurrent data structures show that our approach scales to very large histories and significantly outperforms existing state-of-the-art tools.\n          <\/jats:p>","DOI":"10.1145\/3763123","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2030-2057","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Decrease-and-Conquer Linearizability Monitoring"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-7130-2493","authenticated-orcid":false,"given":"Zheng Han","family":"Lee","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729328"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_16"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561322"},{"key":"e_1_2_1_5_1","unstructured":"Zhendong Ang Azadeh Farzan and Umang Mathur. 2025. Enhanced Data Race Prediction Through Modular Reasoning. arxiv:2504.10813. arxiv:2504.10813"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632915"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Michael Emmi Constantin Enea and Jad Hamza. 2015. On Reducing Linearizability to State Reachability. In Automata Languages and Programming Magn\u00fas M. Halld\u00f3rsson Kazuo Iwama Naoki Kobayashi and Bettina Speckmann (Eds.). Springer Berlin Heidelberg 95\u2013107. https:\/\/doi.org\/10.1007\/978-3-662-47666-6_8 10.1007\/978-3-662-47666-6_8","DOI":"10.1007\/978-3-662-47666-6_8"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2017.16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2005.86"},{"key":"e_1_2_1_14_1","volume-title":"Watson IBM Research Center and R.K. Treiber","author":"Thomas","year":"1986","unstructured":"Thomas J. Watson IBM Research Center and R.K. Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center. https:\/\/books.google.se\/books?id=YQg3HAAACAAJ"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632908"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2020.42"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158113"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737983"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632873"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/305619.305625"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-002-1046-6"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993636.1993687"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704906"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626403001628"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00607-018-0596-7"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429109"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_4"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632924"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-35257-7_12"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062374"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_8"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.16"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Zheng Han Lee and Umang Mathur. 2025. Artifact for \"Efficient Decrease-and-Conquer Linearizability Monitoring\". https:\/\/doi.org\/10.5281\/zenodo.16928307 10.5281\/zenodo.16928307","DOI":"10.5281\/zenodo.16928307"},{"key":"e_1_2_1_41_1","unstructured":"Zheng Han Lee and Umang Mathur. 2025. Efficient Decrease-And-Conquer Linearizability Monitoring. arxiv:2410.04581. arxiv:2410.04581"},{"key":"e_1_2_1_42_1","volume-title":"https:\/\/github.com\/focs-lab\/LinP Last accessed","author":"Lee Zheng Han","year":"2025","unstructured":"Zheng Han Lee and Umang Mathur. 2025. LinP (GitHub). https:\/\/github.com\/focs-lab\/LinP Last accessed 25 March 2025"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3928"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3569450"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378475"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3742465"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295726"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3650212.3685301"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639099"},{"key":"e_1_2_1_54_1","unstructured":"Zheng Shi Lasse M\u00d8ldrup Umang Mathur and Andreas Pavlogiannis. 2025. Testing Message-Passing Concurrency. arxiv:2505.05162. arxiv:2505.05162"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591251"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591291"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1993.1015"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","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\/3763123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:49:54Z","timestamp":1760032194000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":59,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763123"],"URL":"https:\/\/doi.org\/10.1145\/3763123","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}