{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:21Z","timestamp":1767927981075,"version":"3.49.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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":[[2024,6,20]]},"abstract":"<jats:p>The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.<\/jats:p>","DOI":"10.1145\/3656425","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1189-1212","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verification under Intel-x86 with Persistency"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2060-3592","authenticated-orcid":false,"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Cit\u00e9, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0504-7302","authenticated-orcid":false,"given":"K. Narayan","family":"Kumar","sequence":"additional","affiliation":[{"name":"Chennai Mathematical Institute, Chennai, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5060-0117","authenticated-orcid":false,"given":"Prakash","family":"Saivasan","sequence":"additional","affiliation":[{"name":"Institute of Mathematical Sciences, Chennai, India"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1294171129"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_3_1_4_1","volume-title":"NETYS 2020 (Lecture Notes in Computer Science)","author":"Abdulla Parosh Aziz","year":"2020","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer. 2020b. Safety Verification under Power. In NETYS 2020 (Lecture Notes in Computer Science). Springer."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434337"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17436-0_19"},{"key":"e_1_3_1_7_1","first-page":"5:1","volume-title":"CONCUR (LIPIcs, Vol. 59)","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2016. The Benefits of Duality in Verifying Concurrent Programs under TSO. In CONCUR (LIPIcs, Vol. 59). Schloss Dagstuhl, 5:1\u20135:15."},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_30"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_1"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_3"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_13"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371094"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434328"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519270.3538445"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505273"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498683"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656425","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656425","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:14Z","timestamp":1751661794000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656425"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":30,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656425"],"URL":"https:\/\/doi.org\/10.1145\/3656425","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}