{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:22:20Z","timestamp":1779074540810,"version":"3.51.4"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-003"],"award-info":[{"award-number":["ICT15-003"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["863818"],"award-info":[{"award-number":["863818"]}],"id":[{"id":"10.13039\/501100000781","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":[[2021,10,20]]},"abstract":"<jats:p>\n            The verification of concurrent programs remains an open challenge due to the non-determinism in inter-process communication. One recurring algorithmic problem in this challenge is the consistency verification of concurrent executions. In particular, consistency verification under a reads-from map allows to compute the\n            <jats:italic>reads-from (RF) equivalence<\/jats:italic>\n            between concurrent traces, with direct applications to areas such as Stateless Model Checking (SMC). Importantly, the RF equivalence was recently shown to be coarser than the standard Mazurkiewicz equivalence, leading to impressive scalability improvements for SMC under SC (sequential consistency). However, for the\n            <jats:italic>relaxed memory<\/jats:italic>\n            models of TSO and PSO (total\/partial store order), the algorithmic problem of deciding the RF equivalence, as well as its impact on SMC, has been elusive.\n          <\/jats:p>\n          <jats:p>\n            In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of\n            <jats:italic>n<\/jats:italic>\n            events over\n            <jats:italic>k<\/jats:italic>\n            threads and\n            <jats:italic>d<\/jats:italic>\n            variables, we establish novel bounds that scale as\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n              +1\n            <\/jats:sup>\n            for TSO and as\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n              +1\n            <\/jats:sup>\n            \u00b7 min(\n            <jats:italic>n<\/jats:italic>\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n              <jats:sup>2<\/jats:sup>\n            <\/jats:sup>\n            , 2\n            <jats:sup>\n              <jats:italic>k<\/jats:italic>\n              \u00b7\n              <jats:italic>d<\/jats:italic>\n            <\/jats:sup>\n            ) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is\n            <jats:italic>exploration-optimal<\/jats:italic>\n            , in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when\n            <jats:italic>k<\/jats:italic>\n            is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO\/PSO, which yields a significant speedup in the model checking task.\n          <\/jats:p>","DOI":"10.1145\/3485541","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["The reads-from equivalence for the TSO and PSO memory models"],"prefix":"10.1145","volume":"5","author":[{"given":"Truc Lam","family":"Bui","sequence":"first","affiliation":[{"name":"Comenius University Bratislava, Slovakia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tushar","family":"Gautam","sequence":"additional","affiliation":[{"name":"IIT Bombay, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Toman","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535845"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_26"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_24"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.6.11.108"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_14"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360591"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"e_1_2_2_14_1","volume-title":"The Reads-From Equivalence for the TSO and PSO Memory Models. CoRR, abs\/2011.11763","author":"Bui Truc Lam","year":"2021","unstructured":"Truc Lam Bui , Krishnendu Chatterjee , Tushar Gautam , Andreas Pavlogiannis , and Viktor Toman . 2021. The Reads-From Equivalence for the TSO and PSO Memory Models. CoRR, abs\/2011.11763 ( 2021 ), arXiv:2011.11763. arxiv:2011.11763 Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. 2021. The Reads-From Equivalence for the TSO and PSO Memory Models. CoRR, abs\/2011.11763 (2021), arXiv:2011.11763. arxiv:2011.11763"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564897"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2009.4798276"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2020.42"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2753761"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2011.41"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984025"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.16"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360599"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_21"},{"key":"e_1_2_2_42_1","volume-title":"CHESS: A systematic testing tool for concurrent software.","author":"Madan Musuvathi Tom Ball","year":"2007","unstructured":"Tom Ball Madan Musuvathi , Shaz Qadeer . 2007 . CHESS: A systematic testing tool for concurrent software. Tom Ball Madan Musuvathi, Shaz Qadeer. 2007. CHESS: A systematic testing tool for concurrent software."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2006.1598123"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_34"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.456"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385993"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103702"},{"key":"e_1_2_2_56_1","unstructured":"CORPORATE SPARC International Inc.. 1994. The SPARC Architecture Manual (Version 9). Prentice-Hall Inc. Upper Saddle River NJ USA. isbn:0-13-099227-5  CORPORATE SPARC International Inc.. 1994. The SPARC Architecture Manual (Version 9). Prentice-Hall Inc. Upper Saddle River NJ USA. isbn:0-13-099227-5"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_16"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485541","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485541"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":57,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485541"],"URL":"https:\/\/doi.org\/10.1145\/3485541","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}