{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:32:49Z","timestamp":1790937169442,"version":"4.1.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"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":[[2023,1,9]]},"abstract":"<jats:p>The metatheory of axiomatic weak memory models covers questions like the \ncorrectness of compilation mappings from one model to another and the \ncorrectness of local program transformations according to a given model---topics \nusually requiring lengthy human investigation. \nWe show that these questions can be solved by answering a \nmore basic question: \"Given two memory models, is one weaker than the other?\" \nMoreover, for a wide class of axiomatic memory models, we show that this \nbasic question can be reduced to a language inclusion problem between regular \nlanguages, which is decidable.<\/jats:p>\n          <jats:p>Similarly, implementing an efficient check for whether an execution graph is \nconsistent according to a given memory model has required non-trivial manual \neffort. Again, we show that such efficient checks can be derived automatically \nfor a wide class of axiomatic memory models, and that incremental consistency checks \ncan be incorporated in GenMC, a state-of-the-art model checker for concurrent \nprograms. As a result, we get the first time- and space-efficient bounded \nverifier taking the axiomatic memory model as an input parameter.<\/jats:p>","DOI":"10.1145\/3571212","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"544-572","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Kater: Automating Weak Memory Model Metatheory and Consistency Checking"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"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, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"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\/3173162.3177156"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/T-C"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63172-0"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024842"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_1_30_1","unstructured":"Yuval Filmus (https:\/\/cs.stackexchange.com\/users\/683\/yuval-filmus) ( 2022 ). Is the power of a regular language regular? Is the root of a regular language regular? Computer Science Stack Exchange. URL:https:\/\/cs.stackexchange.com\/q\/99371 (version: 2018-10-31). eprint: https:\/\/cs.stackexchange.com\/q\/99371. url: https:\/\/cs.stackexchange.com\/q\/99371 (visited on Oct. 20 2022 ).  \t\t\t\t  Yuval Filmus (https:\/\/cs.stackexchange.com\/users\/683\/yuval-filmus) ( 2022 ). Is the power of a regular language regular? Is the root of a regular language regular? Computer Science Stack Exchange. URL:https:\/\/cs.stackexchange.com\/q\/99371 (version: 2018-10-31). eprint: https:\/\/cs.stackexchange.com\/q\/99371. url: https:\/\/cs.stackexchange.com\/q\/99371 (visited on Oct. 20 2022 )."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_35_1","volume-title":"The SPARC Architecture Manual: Version 8","author":"SPARC International Inc. ( 1992 ).","unstructured":"SPARC International Inc. ( 1992 ). The SPARC Architecture Manual: Version 8 . Prentice-Hall, Inc. SPARC International Inc. ( 1992 ). The SPARC Architecture Manual: Version 8. Prentice-Hall, Inc."},{"key":"e_1_2_1_36_1","volume-title":"The SPARC architecture manual (version 9)","author":"SPARC International Inc. ( 1994 ).","unstructured":"SPARC International Inc. ( 1994 ). The SPARC architecture manual (version 9) . Prentice-Hall . SPARC International Inc. ( 1994 ). The SPARC architecture manual (version 9). Prentice-Hall."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_1_39_1","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\/10.1145\/3571212","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571212"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571212"],"URL":"https:\/\/doi.org\/10.1145\/3571212","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}