{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:58:14Z","timestamp":1767920294722,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100001843","name":"Science and Engineering Research Board (SERB), India","doi-asserted-by":"crossref","award":["MTR\/2022\/000312"],"award-info":[{"award-number":["MTR\/2022\/000312"]}],"id":[{"id":"10.13039\/501100001843","id-type":"DOI","asserted-by":"crossref"}]},{"name":"French National Research Agency (ANR) project CENTEANES","award":["ANR-24-CE25-5598-04"],"award-info":[{"award-number":["ANR-24-CE25-5598-04"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    We address the reachability problem for concurrent programs with an arbitrary number of threads running over the Intel x-86 architecture. We consider the formal model eTSO for Intel x-86 defined by Raad et al. in POPL 2022. This model takes into account multiple memory types and non-temporal writes, combining in a complex way features in the TSO and PSO weak memory models. In PLDI 2024, Abdulla et al. proved that this problem is undecidable for eTSO in general, but that it is decidable under\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -alternation bounding when computations have, for some fixed bound\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    , at most\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    alternations of TSO segments (with TSO writes only) and PSO segments (with PSO writes only) for each thread. The proof of this result assumes that the number of threads is fixed, and relies crucially on referring to thread identities. In this paper, we prove the decidability of the\n                    <jats:italic toggle=\"yes\">k<\/jats:italic>\n                    -alternation bounded reachability problem of eTSO in the parametrized setting when the number of threads is a parameter that can be arbitrarily high. The proof is nontrivial as it cannot refer to thread identities, their number being unbounded. We show that it is possible to overcome this difficulty using a novel and quite complex reduction to reachability in well-structured systems on domains that are BQOs (Better Quasi Orders). This is the first time that BQO-based well-structured systems are used to prove the decidability of verification of infinite state programs.\n                  <\/jats:p>","DOI":"10.1145\/3776680","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1094-1122","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Parametrised Verification of Intel-x86 Programs"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"},{"name":"Malardalen University, Vasteras, 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":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1294171129"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2178\/BSL\/1294171129"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_2_1_4_1","volume-title":"NETYS 2020 (Lecture Notes in Computer Science). Springer.","author":"Abdulla Parosh Aziz","year":"2020","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer. 2020. Safety Verification under Power. In NETYS 2020 (Lecture Notes in Computer Science). Springer."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434337"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17436-0_19"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656425"},{"key":"e_1_2_1_8_1","first-page":"1","article-title":"The Benefits of Duality in Verifying Concurrent Programs under TSO. In CONCUR (LIPIcs, Vol. 59)","volume":"5","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.","journal-title":"Schloss Dagstuhl"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_30"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26850-7_3"},{"key":"e_1_2_1_14_1","volume-title":"Mohamed Faouzi Atig, and Rojin Rezvan","author":"Abdulla Parosh Aziz","year":"2020","unstructured":"Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. 2020. Parameterized verification under TSO is PSPACE-complete. PACMPL, 4, POPL (2020)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855762"},{"key":"e_1_2_1_17_1","volume-title":"Better Quasi-Ordered Transition Systems. CoRR, cs.LO\/0409052","author":"Abdulla Parosh Aziz","year":"2004","unstructured":"Parosh Aziz Abdulla and Aletta Nyl\u00e9n. 2004. Better Quasi-Ordered Transition Systems. CoRR, cs.LO\/0409052 (2004), arxiv:cs.LO\/0409052"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632925"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434328"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519270.3538445"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505273"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013952225669"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5315-4_14"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5315-4_15"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498683"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776680","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:01:32Z","timestamp":1767898892000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776680"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776680"],"URL":"https:\/\/doi.org\/10.1145\/3776680","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}