{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:12:16Z","timestamp":1784211136946,"version":"3.55.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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\n                    <jats:monospace>eTSO<\/jats:monospace>\n                    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\n                    <jats:monospace>eTSO<\/jats:monospace>\n                    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\n                    <jats:monospace>eTSO<\/jats:monospace>\n                    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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla. 2010. Well- and Better-Quasi Ordered Transition Systems. Bulletin of Symbolic Logic 16 4 (2010) 457\u2013515.","DOI":"10.2178\/bsl\/1294171129"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla. 2010. Well (and better) quasi-ordered transition systems. Bull. Symb. Log. 16 4 (2010) 457\u2013515. doi:10.2178\/BSL\/1294171129","DOI":"10.2178\/BSL\/1294171129"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Jatin Arora Mohamed Faouzi Atig and Shankara Narayanan Krishna. 2019. Verification of programs under the release-acquire semantics. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2019 Phoenix AZ USA June 22-26 2019. Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM 1117\u20131132. doi:10.1145\/3314221.3314649","DOI":"10.1145\/3314221.3314649"},{"key":"e_1_3_2_5_2","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_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Ahmed Bouajjani K. Narayan Kumar and Prakash Saivasan. 2021. Deciding reachability under persistent x86-TSO. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201332. doi:10.1145\/3434337","DOI":"10.1145\/3434337"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Ahmed Bouajjani K. Narayan Kumar and Prakash Saivasan. 2022. Verifying Reachability for TSO Programs with Dynamic Thread Creation. In Networked Systems - 10th International Conference NETYS 2022 Virtual Event May 17-19 2022 Proceedings (Lecture Notes in Computer Science Vol. 13464) Mohammed-Amine Koulali and Mira Mezini (Eds.). Springer 283\u2013300. doi:10.1007\/978-3-031-17436-0_19","DOI":"10.1007\/978-3-031-17436-0_19"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Ahmed Bouajjani K. Narayan Kumar and Prakash Saivasan. 2024. Verification under Intel-x86 with Persistency. Proc. ACM Program. Lang. 8 PLDI (2024) 1189\u20131212. doi:10.1145\/3656425","DOI":"10.1145\/3656425"},{"key":"e_1_3_2_9_2","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_2_10_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Ahmed Bouajjani and Tuan Phong Ngo. 2018. A Load-Buffer Semantics for Total Store Ordering. Logical Methods in Computer Science 14 1 (2018). doi:10.23638\/LMCS-14(1:9)2018","DOI":"10.23638\/LMCS-14(1:9)2018"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Florian Furbach Adwait Amit Godbole Yacoub G. Hendi Shankara Narayanan Krishna and Stephan Spengler. 2023. Parameterized Verification under TSO with Data Types. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference TACAS 2023 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2022 Paris France April 22-27 2023 Proceedings Part I (Lecture Notes in Computer Science Vol. 13993) Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer 588\u2013606. doi:10.1007\/978-3-031-30823-9_30","DOI":"10.1007\/978-3-031-30823-9_30"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Adwait Godbole Shankaranarayanan Krishna and Mihir Vahanwala. 2023. Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models. In Computer Aided Verification - 35th International Conference CAV 2023 Paris France July 17-22 2023 Proceedings Part I (Lecture Notes in Computer Science Vol. 13964) Constantin Enea and Akash Lal (Eds.). Springer 184\u2013205. doi:10.1007\/978-3-031-37706-8_10","DOI":"10.1007\/978-3-031-37706-8_10"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Adwait Godbole Shankara Narayanan Krishna and Viktor Vafeiadis. 2021. The Decidability of Verification under PS 2.0. In Programming Languages and Systems - 30th European Symposium on Programming ESOP 2021 Held as Part of the European foint Conferences on Theory and Practice of Software ETAPS 2021 Luxembourg City Luxembourg March 27 - April 1 2021 Proceedings (Lecture Notes in Computer Science Vol. 12648) Nobuko Yoshida (Ed.). Springer 1\u201329. doi:10.1007\/978-3-030-72019-3_1","DOI":"10.1007\/978-3-030-72019-3_1"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig Magnus L\u00e5ng and Tuan Phong Ngo. 2015. Precise and Sound Automatic Fence Insertion Procedure under PSO. In Networked Systems - Third International Conference NETYS 2015 Agadir Morocco May 13-15 2015 Revised Selected Papers (Lecture Notes in Computer Science Vol. 9466) Ahmed Bouajjani and Hugues Fauconnier (Eds.). Springer 32\u201347. doi:10.1007\/978-3-319-26850-7_3","DOI":"10.1007\/978-3-319-26850-7_3"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","unstructured":"Parosh Aziz Abdulla Mohamed Faouzi Atig and Rojin Rezvan. 2020. Parameterized verification under TSO is PSPACE-complete. PACMPL 4 POPL (2020).","DOI":"10.1145\/3371094"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Karlis Cerans Bengt Jonsson and Yih-Kuen Tsay. 1996. General Decidability Theorems for Infinite-State Systems. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science New Brunswick New Fersey USA July 27-30 1996. IEEE Computer Society 313\u2013321. doi:10.1109\/LICS.1996.561359","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla and Aletta Nyl\u00e9n. 2000. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In 15th Annual IEEE Symposium on Logic in Computer Science Santa Barbara California USA June 26-29 2000. IEEE Computer Society 132\u2013140. doi:10.1109\/LICS.2000.855762","DOI":"10.1109\/LICS.2000.855762"},{"key":"e_1_3_2_18_2","unstructured":"Parosh Aziz Abdulla and Aletta Nyl\u00e9n. 2004. Better Quasi-Ordered Transition Systems. CoRR cs.LO\/0409052 (2004). http:\/\/arxiv.org\/abs\/cs.LO\/0409052"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Mohamed Faouzi Atig Ahmed Bouajjani Sebastian Burckhardt and Madanlal Musuvathi. 2010. On the verification problem for weak memory models. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2010 Madrid Spain January 17-23 2010 Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM 7\u201318. doi:10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Mohamed Faouzi Atig Ahmed Bouajjani Sebastian Burckhardt and Madanlal Musuvathi. 2012. What\u2019s Decidable about Weak Memory Models?. In Programming Languages and Systems - 21st European Symposium on Programming ESOP 2012 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2012 Tallinn Estonia March 24 - April 1 2012. Proceedings (Lecture Notes in Computer Science Vol. 7211) Helmut Seidl (Ed.). Springer 26\u201346. doi:10.1007\/978-3-642-28869-2_2","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Egor Derevenetc and Roland Meyer. 2013. Checking and Enforcing Robustness against TSO. In Programming Languages and Systems - 22nd European Symposium on Programming ESOP 2013 Held as Part of the European Joint Conferences on Theory and Practice of Software ETAPS 2013 Rome Italy March 16-24 2013. Proceedings (Lecture Notes in Computer Science Vol. 7792) Matthias Felleisen and Philippa Gardner (Eds.). Springer 533\u2013553. doi:10.1007\/978-3-642-37036-6_29","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Roland Meyer and Eike M\u00f6hlmann. 2011. Deciding Robustness against Total Store Ordering. In Automata Languages and Programming - 38th International Colloquium ICALP 2011 Zurich Switzerland July 4-8 2011 Proceedings Part II (Lecture Notes in Computer Science Vol. 6756) Luca Aceto Monika Henzinger and Jir\u00ed Sgall (Eds.). Springer 428\u2013440. doi:10.1007\/978-3-642-22012-8_34","DOI":"10.1007\/978-3-642-22012-8_34"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Egor Derevenetc and Roland Meyer. 2014. Robustness against Power is PSpace-complete. In Automata Languages and Programming - 41st International Colloquium ICALP 2014 Copenhagen Denmark July 8-11 2014 Proceedings Part II (Lecture Notes in Computer Science Vol. 8573) Javier Esparza Pierre Fraigniaud Thore Husfeldt and Elias Koutsoupias (Eds.). Springer 158\u2013170. doi:10.1007\/978-3-662-43951-7_14","DOI":"10.1007\/978-3-662-43951-7_14"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Zachary Kincaid and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science LICS \u201916 New York NY USA July 5-8 2016 Martin Grohe Eric Koskinen and Natarajan Shankar (Eds.). ACM 185\u2013196. doi:10.1145\/2933575.2935310","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2024. Commutativity Simplifies Proofs of Parameterized Programs. Proc. ACM Program. Lang. 8 POPL (2024) 2485\u20132513. doi:10.1145\/3632925","DOI":"10.1145\/3632925"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Alain Finkel and Philippe Schnoebelen. 2001. Well-structured transition systems everywhere! Theor. Comput. Sci. 256 1-2 (2001) 63\u201392. doi:10.1016\/S0304-3975(00)00102-X","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Artem Khyzha and Ori Lahav. 2021. Taming x86-TSO Persistency. Proc. ACM Program. Lang. 5 POPL Article 47 (Jan. 2021) 29 pages. doi:10.1145\/3434328","DOI":"10.1145\/3434328"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Shankaranarayanan Krishna Adwait Godbole Roland Meyer and Soham Chakraborty. 2022. Parameterized Verification under Release Acquire is PSPACE-complete. In PODC \u201922: ACM Symposium on Principles of Distributed Computing Salerno Italy July 25-29 2022 Alessia Milani and Philipp Woelfel (Eds.). ACM 482\u2013492. doi:10.1145\/3519270.3538445","DOI":"10.1145\/3519270.3538445"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav and Udi Boker. 2020. Decidable verification under a causally consistent shared memory. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation PLDI 2020 London UK June 15-20 2020 Alastair F. Donaldson and Emina Torlak (Eds.). ACM 211\u2013226. doi:10.1145\/3385412.3385966","DOI":"10.1145\/3385412.3385966"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav and Udi Boker. 2022. What\u2019s Decidable About Causally Consistent Shared Memory? ACM Trans. Program. Lang. Syst. 44 2 (2022) 8:1\u20138:55. doi:10.1145\/3505273","DOI":"10.1145\/3505273"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav and Roy Margalit. 2019. Robustness against release\/acquire semantics. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2019 Phoenix AZ USA June 22-26 2019 Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM 126\u2013141. doi:10.1145\/3314221.3314604","DOI":"10.1145\/3314221.3314604"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav Egor Namakonov Jonas Oberhauser Anton Podkopaev and Viktor Vafeiadis. 2021. Making weak memory models fair. Proc. ACM Program. Lang. 5 OOPSLA (2021) 1\u201327. doi:10.1145\/3485475","DOI":"10.1145\/3485475"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"L. Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28 9 (1979) 690\u2013691.","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Alberto Marcone. 2001. Fine Analysis of the Quasi-Orderings on the Power Set. Order 18 4 (2001) 339\u2013347. doi:10.1023\/A:1013952225669","DOI":"10.1023\/A:1013952225669"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Roy Margalit and Ori Lahav. 2021. Verifying observational robustness against a c11-style memory model. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201333. doi:10.1145\/3434285","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"E. C. Milner. 1985. Basic WQO- and BQO-Theory. Springer Netherlands Dordrecht 487\u2013502. doi:10.1007\/978-94-009-5315-4_14","DOI":"10.1007\/978-94-009-5315-4_14"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"M. Pouzet. 1985. Applications of Well Quasi-Ordering and Better Quasi-Ordering. Springer Netherlands Dordrecht 503\u2013519. doi:10.1007\/978-94-009-5315-4_15","DOI":"10.1007\/978-94-009-5315-4_15"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Azalea Raad Luc Maranget and Viktor Vafeiadis. 2022. Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal stores. Proc. ACM Program. Lang. 6 POPL (2022) 1\u201331. doi:10.1145\/3498683","DOI":"10.1145\/3498683"},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","unstructured":"P. Sewell S. Sarkar S. Owens F. Z. Nardelli and M. O. Myreen. 2010. x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53 (2010) 89\u201397. Issue 7.","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,7,16]],"date-time":"2026-07-16T13:40:44Z","timestamp":1784209244000},"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"}}]}}