{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:32Z","timestamp":1780994492327,"version":"3.54.1"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["678177"],"award-info":[{"award-number":["678177"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>While many program properties like the validity of assertions and in-bounds array accesses admit nearly-trivial monitoring algorithms, the standard correctness criterion for concurrent data structures does not. Given an implementation of an arbitrary abstract data type, checking whether the operations invoked in one single concurrent execution are linearizable, i.e., indistinguishable from an execution where the same operations are invoked atomically, requires exponential time in the number of operations.<\/jats:p>\n          <jats:p>In this work we identify a class of collection abstract data types which admit polynomial-time linearizability monitors. Collections capture the majority of concurrent data structures available in practice, including stacks, queues, sets, and maps. Although monitoring executions of arbitrary abstract data types requires enumerating exponentially-many possible linearizations, collections enjoy combinatorial properties which avoid the enumeration. We leverage these properties to reduce linearizability to Horn satisfiability. As far as we know, ours is the first sound, complete, and tractable algorithm for monitoring linearizability for types beyond single-value registers.<\/jats:p>","DOI":"10.1145\/3158113","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Sound, complete, and tractable linearizability monitoring for concurrent collections"],"prefix":"10.1145","volume":"2","author":[{"given":"Michael","family":"Emmi","sequence":"first","affiliation":[{"name":"SRI International, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"University of Paris Diderot, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2847"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_8"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677002"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/343477.343502"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950377"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699681"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676963"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958085"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837645"},{"key":"e_1_2_2_15_1","volume-title":"Exposing Non-Atomic Methods of Concurrent Objects. CoRR abs\/1706.09305","author":"Emmi Michael","year":"2017","unstructured":"Michael Emmi and Constantin Enea . 2017. Exposing Non-Atomic Methods of Concurrent Objects. CoRR abs\/1706.09305 ( 2017 ). arXiv: 1706.09305 http:\/\/arxiv.org\/abs\/1706.09305 Michael Emmi and Constantin Enea. 2017. Exposing Non-Atomic Methods of Concurrent Objects. CoRR abs\/1706.09305 (2017). arXiv: 1706.09305 http:\/\/arxiv.org\/abs\/1706.09305"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737983"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_21"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-003-0117-6"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_2_21_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming. Morgan Kaufmann.  Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming. Morgan Kaufmann."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19195-9_4"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_26"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/942572.807045"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3928"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1201\/9781420035179.ch47"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048073"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1993.1015"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2467371"},{"key":"e_1_2_2_40_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\/10.1145\/3158113","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158113","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158113"],"URL":"https:\/\/doi.org\/10.1145\/3158113","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}