{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T12:00:01Z","timestamp":1790424001717,"version":"4.1.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,4,10]]},"abstract":"<jats:p>We present a model checking approach for axiomatic memory consistency models written in the language CAT. It can prove properties of single memory models like the monotonicity of barriers, and also compare models like TSO and ARM8. To achieve this expressiveness, our approach supports the full rational fragment of CAT. We not only support the Kleene star operation, composition, and union to define relations in a memory model, but also, for the first time, intersection, converse, and the construction of relations from sets. Our model checking approach for memory consistency models is logical in nature: we formulate the problem as satisfiability in a logical theory of relations. Our technical contribution is then a new theory solver that is sound, complete, and optimal from a complexity point of view. At the heart of our solver is a cyclic proof system that can detect invariants on-the-fly. This allows us to terminate early not only in the case that a model has been found, but also in the case of unsatisfiability. Our solver is easy to implement and easy to combine with heuristics. We have implemented a combination with counterexample-guided abstraction refinement, and exercised the prototype on a number of benchmarks \u2014 with promising results.<\/jats:p>","DOI":"10.1145\/3798208","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T14:33:43Z","timestamp":1775831623000},"page":"231-259","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["RAT-CAT-SAT: Model Checking Memory Consistency Models"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-2418-8689","authenticated-orcid":false,"given":"Jan","family":"Gr\u00fcnke","sequence":"first","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3176-8552","authenticated-orcid":false,"given":"Thomas","family":"Haas","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8495-671X","authenticated-orcid":false,"given":"Roland","family":"Meyer","sequence":"additional","affiliation":[{"name":"TU Braunschweig, Braunschweig, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330023"},{"key":"e_1_3_2_4_2","volume-title":"Ph. D. Dissertation","author":"Alglave Jade","year":"2010","unstructured":"JadeAlglave. 2010. A shared memory poetics. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_7_2","unstructured":"JadeAlglave and LucMaranget. 2010. herdtools7: A Tool Suite to Test Weak Memory Models. https:\/\/github.com\/herd\/herdtools7."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3296957.3177156"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01225472"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.09.024"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706303"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3465402"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837637"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/1207696"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_3_2_19_2","first-page":"49","volume-title":"Proceedings of the 2013 USENIX Conference on Annual Technical Conference (San Jose, CA) (USENIX ATC\u201913)","author":"Bronson Nathan","year":"2013","unstructured":"NathanBronson, ZachAmsden, GeorgeCabrera, PrasadChakka, PeterDimov, HuiDing, JackFerris, AnthonyGiardullo, SachinKulkarni, HarryLi, MarkMarchukov, DmitriPetrov, LovroPuzar, Yee JiunSong, and VenkatVenkataramani. 2013. TAO: Facebook\u2019s distributed data store for the social graph. In Proceedings of the 2013 USENIX Conference on Annual Technical Conference (San Jose, CA) (USENIX ATC\u201913). USENIX Association, USA, 49\u201360."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328453"},{"key":"e_1_3_2_21_2","unstructured":"PaulBrunet and DamienPous. 2014. Decidability of Identity-free Relational Kleene Lattices. Ph. D. Dissertation. ENS de Lyon."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06251-8_7"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.17"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049844"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_31"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66902-1_16"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.19"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.5555\/359243.359271"},{"issue":"121","key":"e_1_3_2_30_2","first-page":"123","article-title":"GRAMMAR LOGICS","volume":"31","author":"del Cerro Luis Fari\u00f1as","year":"1988","unstructured":"Luis Fari\u00f1asdel Cerro and MarttiPenttonen. 1988. GRAMMAR LOGICS. Logique et Analyse 31, 121\/122 (1988), 123\u2013134. http:\/\/www.jstor.org\/stable\/44084228","journal-title":"Logique et Analyse"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.6.933"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2021.41"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.3166\/JANCL.21.61-91"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"SebastianEnqvist. 2020. A circular proof system for the hybrid mu-calculus. arXiv:2001.04971 [cs.LO] doi:10.48550\/arXiv.2001.04971","DOI":"10.48550\/arXiv.2001.04971"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"DiegoFigueira SantiagoFigueira and EdwinPin. 2023. PDL on Steroids: on Expressive Extensions of PDL with Intersection and Converse. In 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201313. doi:10.1109\/LICS56636.2023.10175813","DOI":"10.1109\/LICS56636.2023.10175813"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab017"},{"key":"e_1_3_2_37_2","unstructured":"StefanG\u00f6ller and MarkusLohrey. 2010. ICPDL with Fixed Points and Nominals. https:\/\/staff.fnwi.uva.nl\/y.venema\/mfl\/contributed\/goeller.pdf."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_15"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.2178\/JSL\/1231082313"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_20"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"JanGr\u00fcnke ThomasHaas and RolandMeyer. 2026. RAT-SAT-CAT: Model Checking Memory Consistency Models (Artifact). doi:10.5281\/zenodo.18498209","DOI":"10.5281\/zenodo.18498209"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563292"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_27"},{"key":"e_1_3_2_45_2","volume-title":"Programming language C++","author":"International Organization for Standardization","year":"2011","unstructured":"International Organization for Standardization 2011. ISO\/IEC 14882:2011. Programming language C++. International Organization for Standardization."},{"key":"e_1_3_2_46_2","volume-title":"Programming language C","author":"International Organization for Standardization","year":"2011","unstructured":"International Organization for Standardization 2011. ISO\/IEC 9899:2011. Programming language C. International Organization for Standardization."},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2935764.2935810"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2011.10.009"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2024.33"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63172-0_43"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837643"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062352"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1129642115"},{"key":"e_1_3_2_59_2","unstructured":"LKMM 2024. LKML Patch v04 Discussion. https:\/\/lkml.org\/lkml\/2024\/6\/4\/1071. [Accessed 2026-02-26]."},{"key":"e_1_3_2_60_2","unstructured":"LKMM 2025. Linux-kernel Memory Model. https:\/\/github.com\/torvalds\/linux\/blob\/master\/tools\/memory-model\/linux-kernel.cat. [Accessed 2026-02-26]."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3533045"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304043"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024842"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Yatin A.Manerkar CarolineTrippel DanielLustig MichaelPellauer and MargaretMartonosi. 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. arXiv:1611.01507 [cs.PL] doi:10.48550\/arXiv.1611.01507","DOI":"10.48550\/arXiv.1611.01507"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040336"},{"key":"e_1_3_2_68_2","unstructured":"LucMaranget and JadeAlglave. 2015. Towards a Formalization of the HSA Memory Model in the cat Language. 57 pages. https:\/\/inria.hal.science\/hal-01413251 HSA Foundation technical and normative document available at http:\/\/www.hsafoundation.com\/standards\/."},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005132"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","unstructured":"YoshikiNakamura. 2024. Derivatives on Graphs for the Positive Calculus of Relations with Transitive Closure. arXiv preprint arXiv:2408.08236 (2024). doi:10.48550\/arXiv.2408.08236","DOI":"10.48550\/arXiv.2408.08236"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","unstructured":"Linh AnhNguyen. 2011. A Cut-Free ExpTime Tableau Decision Procedure for the Logic Extending Converse-PDL with Regular Inclusion Axioms. arXiv e-prints Article arXiv:1104.0405 (April 2011) arXiv:1104.0405 pages. arXiv:1104.0405 [cs.LO] doi:10.48550\/arXiv.1104.0405","DOI":"10.48550\/arXiv.1104.0405"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-09506-8"},{"key":"e_1_3_2_73_2","unstructured":"JonasOberhauser. 2023. Linux-kernel Memory Model Patch v02. https:\/\/github.com\/torvalds\/linux\/commit\/9ba7d3b3b826ef47c1b7b8dbc2d57da868168128. [Accessed 2026-02-26]."},{"key":"e_1_3_2_74_2","unstructured":"JonasOberhauser. 2023. Linux-kernel Memory Model Patch v03. https:\/\/github.com\/torvalds\/linux\/commit\/762e9357e713a2025db05bc36a36a7afc248f9d3. [Accessed 2026-02-26]."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_77_2","unstructured":"AntonioPaolillo Hern\u00e1n Poncede Le\u00f3n ThomasHaas DiogoBehrens Rafael Lourenco de LimaChehab MingFu and RolandMeyer. 2021. Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models. CoRR abs\/2111.15240 (2021). arXiv:2111.15240 https:\/\/arxiv.org\/abs\/2111.15240"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","unstructured":"Hern\u00e1n Ponce-deLe\u00f3n FlorianFurbach KeijoHeljanko and RolandMeyer. 2018. BMC with Memory Models as Modules. In 2018 Formal Methods in Computer Aided Design (FMCAD). 1\u20139. doi:10.23919\/FMCAD.2018.8603021","DOI":"10.23919\/FMCAD.2018.8603021"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.STACS.2018.3"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-016-"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/1017460.1017464"},{"key":"e_1_3_2_84_2","unstructured":"AlanStern. 2023. Linux-kernel Memory Model Patch v01. https:\/\/github.com\/torvalds\/linux\/commit\/ebd50e2947de9d2675b800a6a29748d0ed7d7fd4. [Accessed 2026-02-26]."},{"key":"e_1_3_2_85_2","doi-asserted-by":"crossref","unstructured":"ATarski and SGivant. 1987. A formalization of set theory without variables AMS Coll.","DOI":"10.1090\/coll\/041"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676995"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902305"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/2926965"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385973"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3798208","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T11:17:20Z","timestamp":1790421440000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3798208"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,10]]},"references-count":91,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2026,4,10]]}},"alternative-id":["10.1145\/3798208"],"URL":"https:\/\/doi.org\/10.1145\/3798208","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,10]]},"assertion":[{"value":"2025-10-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}