{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:00:54Z","timestamp":1779087654557,"version":"3.51.4"},"reference-count":94,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>We propose a family of logical theories for capturing an abstract notion of consistency and show how to build a generic and efficient theory solver that works for all members in the family.  \nThe theories can be used to model the influence of memory consistency models on the semantics of concurrent programs.  \nThey are general enough to precisely capture important examples like TSO, POWER, ARMv8, RISC-V, RC11, IMM, and the Linux kernel memory model.  \nTo evaluate the expressiveness of our theories and the performance of our solver, we integrate them into a lazy SMT scheme that we use as a backend for a bounded model checking tool.  \nAn evaluation against related verification tools shows, besides flexibility, promising performance on challenging programs under complex memory models.<\/jats:p>","DOI":"10.1145\/3563292","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"114-144","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["CAAT: consistency as a theory"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-8552","authenticated-orcid":false,"given":"Thomas","family":"Haas","sequence":"first","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8830","authenticated-orcid":false,"given":"Hern\u00e1n","family":"Ponce de Le\u00f3n","sequence":"additional","affiliation":[{"name":"Huawei, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_2_1_5_1","volume-title":"Foundations of Databases: The Logical Level","author":"Abiteboul Serge","unstructured":"Serge Abiteboul , Richard Hull , and Victor Vianu . 1995. Foundations of Databases: The Logical Level . Addison-Wesley Longman Publishing Co., Inc. . https:\/\/doi.org\/10.5555\/551350 10.5555\/551350 Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases: The Logical Level. Addison-Wesley Longman Publishing Co., Inc.. https:\/\/doi.org\/10.5555\/551350"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_1_8_1","unstructured":"Jade Alglave. 2010. A Shared Memory Poetics. L\u2019universit\u00e9 Paris Denis Diderot. \t\t\t\t  Jade Alglave. 2010. A Shared Memory Poetics. L\u2019universit\u00e9 Paris Denis Diderot."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786763.2694391"},{"key":"e_1_2_1_10_1","volume-title":"Syntax and analytic semantics of LISA. CoRR, abs\/1608.06583","author":"Alglave Jade","year":"2016","unstructured":"Jade Alglave and Patrick Cousot . 2016. Syntax and analytic semantics of LISA. CoRR, abs\/1608.06583 ( 2016 ), arxiv:1608.06583 Jade Alglave and Patrick Cousot. 2016. Syntax and analytic semantics of LISA. CoRR, abs\/1608.06583 (2016), arxiv:1608.06583"},{"key":"e_1_2_1_11_1","volume-title":"Syntax and semantics of the weak consistency model specification language CAT. CoRR, abs\/1608.07531","author":"Alglave Jade","year":"2016","unstructured":"Jade Alglave , Patrick Cousot , and Luc Maranget . 2016. Syntax and semantics of the weak consistency model specification language CAT. CoRR, abs\/1608.07531 ( 2016 ), arxiv:1608.07531 Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. Syntax and semantics of the weak consistency model specification language CAT. CoRR, abs\/1608.07531 (2016), arxiv:1608.07531"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_16"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_9"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4980-1_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103717"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375591"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062353"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_1_32_1","volume-title":"Reasoning about parallel architectures","author":"Collier William W.","unstructured":"William W. Collier . 1992. Reasoning about parallel architectures . Prentice Hall . isbn:978-0-13-766098-8 William W. Collier. 1992. Reasoning about parallel architectures. Prentice Hall. isbn:978-0-13-766098-8"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_31"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_25"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303984"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486607.3486751"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-0-22107-6"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508424"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7079674"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_2_1_49_1","volume-title":"Ioannidis and Raghu Ramakrishnan","author":"Yannis","year":"1988","unstructured":"Yannis E. Ioannidis and Raghu Ramakrishnan . 1988 . Efficient Transitive Closure Algorithms. In VLDB. Morgan Kaufmann , 382\u2013394. https:\/\/doi.org\/10.5555\/645915.671829 10.5555\/645915.671829 Yannis E. Ioannidis and Raghu Ramakrishnan. 1988. Efficient Transitive Closure Algorithms. In VLDB. Morgan Kaufmann, 382\u2013394. https:\/\/doi.org\/10.5555\/645915.671829"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/357474.355063"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44880-2_1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48869-1_11"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_25"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_2_1_58_1","volume-title":"A Formally-Verified Framework for Fair Synchronization in Kotlin Coroutines. CoRR, abs\/2111.12682","author":"Koval Nikita","year":"2021","unstructured":"Nikita Koval , Dmitry Khalanskiy , and Dan Alistarh . 2021. A Formally-Verified Framework for Fair Synchronization in Kotlin Coroutines. CoRR, abs\/2111.12682 ( 2021 ), arxiv:2111.12682 Nikita Koval, Dmitry Khalanskiy, and Dan Alistarh. 2021. A Formally-Verified Framework for Fair Synchronization in Kotlin Coroutines. CoRR, abs\/2111.12682 (2021), arxiv:2111.12682"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_22"},{"key":"e_1_2_1_63_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/ \t\t\t\t  K. Rustan M. Leino. 2008. This is Boogie 2. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_1_65_1","volume-title":"Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR, abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar , Caroline Trippel , Daniel Lustig , Michael Pellauer , and Margaret Martonosi . 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR, abs\/1611.01507 ( 2016 ), arxiv:1611.01507 Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR, abs\/1611.01507 (2016), arxiv:1611.01507"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290371"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371136"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446748"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"e_1_2_1_72_1","volume-title":"Diogo Behrens Thomas Haas, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer.","author":"Paolillo Antonio","year":"2022","unstructured":"Antonio Paolillo , Hern\u00e1n Ponce de Le\u00f3n , Diogo Behrens Thomas Haas, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer. 2022 . Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. CoRR , abs\/2111.15240 (2022), arxiv:2111.15240 Antonio Paolillo, Hern\u00e1n Ponce de Le\u00f3n, Diogo Behrens Thomas Haas, Rafael Lourenco de Lima Chehab, Ming Fu, and Roland Meyer. 2022. Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. CoRR, abs\/2111.15240 (2022), arxiv:2111.15240"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_15"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_24"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_11"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328911.1328917"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993520"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190034"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3604-8_2"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/SWAT.1971.10"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806635"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509532"},{"key":"e_1_2_1_92_1","volume-title":"Introduction to Graph Theory","author":"West Douglas B.","unstructured":"Douglas B. West . 2000. Introduction to Graph Theory . Prentice Hall . Douglas B. West. 2000. Introduction to Graph Theory. Prentice Hall."},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009838"},{"key":"e_1_2_1_94_1","volume-title":"Provenance for Large-scale Datalog. CoRR, abs\/1907.05045","author":"Zhao David","year":"2019","unstructured":"David Zhao , Pavle Subotic , and Bernhard Scholz . 2019. Provenance for Large-scale Datalog. CoRR, abs\/1907.05045 ( 2019 ), arxiv:1907.05045 David Zhao, Pavle Subotic, and Bernhard Scholz. 2019. Provenance for Large-scale Datalog. CoRR, abs\/1907.05045 (2019), arxiv:1907.05045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563292","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563292","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563292"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":94,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563292"],"URL":"https:\/\/doi.org\/10.1145\/3563292","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}