{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:22Z","timestamp":1790927542219,"version":"4.1.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>\n            Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C\/C++. One of the most fundamental problems associated with a memory model\n            <jats:italic>M<\/jats:italic>\n            is consistency checking: given an execution\n            <jats:italic>X<\/jats:italic>\n            , is\n            <jats:italic>X<\/jats:italic>\n            consistent with\n            <jats:italic>M<\/jats:italic>\n            ? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic analyses. As such, it has been explored extensively and its complexity is well-understood for traditional models like SC and TSO. However, less is known for the numerous model variants of C\/C++, for which the problem becomes challenging due to the intricacies of their concurrency primitives. In this work we study the problem of consistency checking for popular variants of the C11 memory model, in particular, the\n            <jats:italic>RC<\/jats:italic>\n            20 model, its release-acquire (\n            <jats:italic>RA<\/jats:italic>\n            ) fragment, the strong and weak variants of\n            <jats:italic>RA<\/jats:italic>\n            (\n            <jats:italic>SRA<\/jats:italic>\n            and\n            <jats:italic>WRA<\/jats:italic>\n            ), as well as the\n            <jats:italic>Relaxed<\/jats:italic>\n            fragment of\n            <jats:italic>RC<\/jats:italic>\n            20.\n          <\/jats:p>\n          <jats:p>\n            Motivated by applications in testing and model checking, we focus on reads-from consistency checking. The input is an execution\n            <jats:italic>X<\/jats:italic>\n            specifying a set of events, their program order and their reads-from relation, and the task is to decide the existence of a modification order on the writes of\n            <jats:italic>X<\/jats:italic>\n            that makes\n            <jats:italic>X<\/jats:italic>\n            consistent in a memory model. We draw a rich complexity landscape for this problem; our results include (i) nearly-linear-time algorithms for certain variants, which improve over prior results, (ii) fine-grained optimality results, as well as (iii) matching upper and lower bounds (NP-hardness) for other variants. To our knowledge, this is the first work to characterize the complexity of consistency checking for C11 memory models. We have implemented our algorithms inside the TruSt model checker and the C11Tester testing tool. Experiments on standard benchmarks show that our new algorithms improve consistency checking, often by a significant margin.\n          <\/jats:p>","DOI":"10.1145\/3591251","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"761-785","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Optimal Reads-From Consistency Checking for C11-Style Memory Models"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9125-8506","authenticated-orcid":false,"given":"H\u00fcnkar Can","family":"Tun\u00e7","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4454-2050","authenticated-orcid":false,"given":"Soham","family":"Chakraborty","sequence":"additional","affiliation":[{"name":"TU Delft, Netherlands"}],"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, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360576"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"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","unstructured":"Jade Alglave. 2010. A Shared Memory Poetics. Ph. D. Dissertation. l\u2019Universit\u00e9 Paris 7 - Denis Diderot. \t\t\t\t  Jade Alglave. 2010. A Shared Memory Poetics. Ph. D. Dissertation. l\u2019Universit\u00e9 Paris 7 - Denis Diderot."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360568"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009888"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485541"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360550"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007391"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2009.4798276"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2020.42"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2753761"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594315"},{"key":"e_1_2_1_26_1","unstructured":"ISO\/IEC 14882. 2011. Programming Language C++. \t\t\t\t  ISO\/IEC 14882. 2011. Programming Language C++."},{"key":"e_1_2_1_27_1","unstructured":"ISO\/IEC 9899. 2011. Programming Language C. \t\t\t\t  ISO\/IEC 9899. 2011. Programming Language C."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276516"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062374"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505273"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_1_40_1","unstructured":"Carl Lerche. 2020. Loom. Available at https:\/\/github.com\/tokio-rs\/loom \t\t\t\t  Carl Lerche. 2020. Loom. Available at https:\/\/github.com\/tokio-rs\/loom"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043593"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446711"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2006.1598123"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276515"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394783"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371085"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1225053"},{"key":"e_1_2_1_52_1","volume-title":"Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis.","author":"Tun\u00e7 H\u00fcnkar Can","year":"2023","unstructured":"H\u00fcnkar Can Tun\u00e7 , Parosh Aziz Abdulla , Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis. 2023 . Optimal Reads-From Consistency Checking for C11-Style Memory Models . arxiv:2304.03714. H\u00fcnkar Can Tun\u00e7, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis. 2023. Optimal Reads-From Consistency Checking for C11-Style Memory Models. arxiv:2304.03714."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7816526"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1142\/9789813272880_0188"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3186893"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1812"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_16"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591251","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591251","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591251"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":59,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591251"],"URL":"https:\/\/doi.org\/10.1145\/3591251","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}