{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:11Z","timestamp":1780994651662,"version":"3.54.1"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010661","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/100010661","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":[[2025,1,7]]},"abstract":"<jats:p>Concurrent libraries implement standard data structures, such as stacks and queues, in a thread-safe manner, typically providing an atomic interface to the data structure. They serve as building blocks for concurrent programs, and incorporate advanced synchronization mechanisms to achieve good performance.<\/jats:p>\n                  <jats:p>\n                    In this paper, we are concerned with the problem of verifying correctness of such libraries under weak memory consistency in a fully automated fashion. To this end, we develop R\n                    <jats:sc>elinche<\/jats:sc>\n                    , a model checker that verifies atomicity and functional correctness of a concurrent library implementation in any client program that invokes the library methods up to some bounded number of times. Our tool establishes refinement between the concurrent library implementation and its atomic specification in a fully parallel client, which it then strengthens to capture all possible other (more constrained) clients of the library.\n                  <\/jats:p>\n                  <jats:p>\n                    R\n                    <jats:sc>elinche<\/jats:sc>\n                    scales sufficiently to verify correctness of standard concurrent library benchmarks for all client programs with up to 7\u20139 library method invocations, and finds minimal counterexamples with 4-7 method calls of non-trivial linearizability bugs due to weak memory consistency.\n                  <\/jats:p>","DOI":"10.1145\/3704906","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2090-2117","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3990-1651","authenticated-orcid":false,"given":"Pavel","family":"Golovin","sequence":"first","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_3_1","first-page":"324","article-title":"An integrated specification and verification technique for highly concurrent data structures.","volume":"7795","author":"Abdulla Parosh Aziz","year":"2013","unstructured":"Parosh Aziz Abdulla, Fr\u00e9d\u00e9ric Haziza, Luk\u00e1\u0161 Hol\u00edk, Bengt Jonsson, and Ahmed Rezine. 2013. An integrated specification and verification technique for highly concurrent data structures. In: TACAS 2013 (LNCS). Ed. by Nir Piterman and Scott A. Smolka. Vol. 7795. Springer, 324\u2013338.","journal-title":"TACAS 2013"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"e_1_3_2_5_1","unstructured":"Samy Al Bahra N.d..Concurrency Kit. (). https:\/\/github.com\/concurrencykit\/ck."},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485541"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_45"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00625969"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676963"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-73721-8_9"},{"key":"e_1_3_2_21_1","first-page":"174","article-title":"Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates.","volume":"8044","author":"Dragoi Cezara","year":"2013","unstructured":"Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In: CAV 2013 (LNCS). Ed. by Natasha Sharygina and Helmut Veith. Vol. 8044. Springer, 174\u2013190.","journal-title":"CAV 2013"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_30"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290373"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428196"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Pavel Golovin Michalis Kokologiannakis and Viktor Vafeiadis. Oct.2024. RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency (Replication Package). (Oct. 2024). https:\/\/doi.org\/10.5281\/zenodo.13992580 10.5281\/zenodo.13992580","DOI":"10.5281\/zenodo.13992580"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_3_2_30_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77096-1_29"},{"key":"e_1_3_2_33_1","unstructured":"Max Khizhinsky N.d..CDS C++ library. (). https:\/\/github.com\/khizmax\/libcds."},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_26"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656449"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_12"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_8"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.03.007"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/CPE.3928"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018743.3018749"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_3_2_55_1","unstructured":"James Reinders. 2007. Intel Threading Building Blocks."},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571246"},{"key":"e_1_3_2_57_1","first-page":"450","article-title":"Automatically Proving Linearizability.","volume":"6174","author":"Vafeiadis Viktor","year":"2010","unstructured":"Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In: CAV 2010 (LNCS). Ed. by Tayssir Touili, Byron Cook, and Paul Jackson. Vol. 6174. Springer, 450\u2013464.","journal-title":"CAV 2010"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_27"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704906","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704906","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:08Z","timestamp":1770200228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704906"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":57,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704906"],"URL":"https:\/\/doi.org\/10.1145\/3704906","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}