{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:33:20Z","timestamp":1742949200593,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572555"},{"type":"electronic","value":"9783031572562"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the<jats:sc>x86<\/jats:sc>architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable).<\/jats:p><jats:p>In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete.<\/jats:p>","DOI":"10.1007\/978-3-031-57256-2_14","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"276-295","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification under TSO with an infinite Data Domain"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-4922-9363","authenticated-orcid":false,"given":"Florian","family":"Furbach","sequence":"additional","affiliation":[]},{"given":"Shashwat","family":"Garg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Aiswarya, C., Atig, M.F.: Data communicating processes with unreliable channels. In: LICS. pp. 166\u2013175. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934535, https:\/\/doi.org\/10.1145\/2933575.2934535","DOI":"10.1145\/2933575.2934535 10.1145\/2933575.2934535"},{"key":"14_CR2","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: A load-buffer semantics for total store ordering. LMCS 14(1) (2018)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Furbach, F., Garg, S.: Verification under TSO with an infinite data domain (2024)","DOI":"10.1007\/978-3-031-57256-2_14"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Furbach, F., Godbole, A.A., Hendi, Y.G., Krishna, S.N., Spengler, S.: Parameterized verification under TSO with data types. In: TACAS 2023. LNCS, vol. 13993, pp. 588\u2013606. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_30, https:\/\/doi.org\/10.1007\/978-3-031-30823-9_30","DOI":"10.1007\/978-3-031-30823-9_30 10.1007\/978-3-031-30823-9_30"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Phong, N.T.: The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In: ESOP 2015. LNCS, vol.\u00a09032, pp. 308\u2013332. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13, https:\/\/doi.org\/10.1007\/978-3-662-46669-8_13","DOI":"10.1007\/978-3-662-46669-8_13 10.1007\/978-3-662-46669-8_13"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Rezvan, R.: Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4(POPL), 26:1\u201326:29 (2020). https:\/\/doi.org\/10.1145\/3371094, https:\/\/doi.org\/10.1145\/3371094","DOI":"10.1145\/3371094 10.1145\/3371094"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Stenman, J.: Dense-timed pushdown automata. In: LICS. pp. 35\u201344. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/LICS.2012.15, https:\/\/doi.org\/10.1109\/LICS.2012.15","DOI":"10.1109\/LICS.2012.15 10.1109\/LICS.2012.15"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109\u2013127 (2000). https:\/\/doi.org\/10.1006\/inco.1999.2843, https:\/\/doi.org\/10.1006\/inco.1999.2843","DOI":"10.1006\/inco.1999.2843 10.1006\/inco.1999.2843"},{"key":"14_CR9","unstructured":"Abdulla, P.A., Delzanno, G.: On the coverability problem for constrained multiset rewriting. In: Proc. AVIS\u201906, The fifth Int. Workshop on on Automated Verification of Infinite-State Systems (2006)"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: LICS. pp. 160\u2013170. IEEE Computer Society (1993). https:\/\/doi.org\/10.1109\/LICS.1993.287591, https:\/\/doi.org\/10.1109\/LICS.1993.287591","DOI":"10.1109\/LICS.1993.287591 10.1109\/LICS.1993.287591"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 685\u2013725. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_21, https:\/\/doi.org\/10.1007\/978-3-319-10575-8_21","DOI":"10.1007\/978-3-319-10575-8_21 10.1007\/978-3-319-10575-8_21"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8, https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8 10.1016\/0304-3975(94)90010-8"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: SIGPLAN-SIGACT. pp. 7\u201318. ACM (2010). https:\/\/doi.org\/10.1145\/1706299.1706303, https:\/\/doi.org\/10.1145\/1706299.1706303","DOI":"10.1145\/1706299.1706303 10.1145\/1706299.1706303"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: CAV. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9, https:\/\/doi.org\/10.1007\/978-3-642-22110-1_9","DOI":"10.1007\/978-3-642-22110-1_9 10.1007\/978-3-642-22110-1_9"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: ESOP 2013. LNCS, vol.\u00a07792, pp. 533\u2013553. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29, https:\/\/doi.org\/10.1007\/978-3-642-37036-6_29","DOI":"10.1007\/978-3-642-37036-6_29 10.1007\/978-3-642-37036-6_29"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: CONCUR. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63141-0_10, https:\/\/doi.org\/10.1007\/3-540-63141-0_10","DOI":"10.1007\/3-540-63141-0_10 10.1007\/3-540-63141-0_10"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Burckhardt, S.: Principles of eventual consistency. FTPL 1(1-2), 1\u2013150 (2014). https:\/\/doi.org\/10.1561\/2500000011, https:\/\/doi.org\/10.1561\/2500000011","DOI":"10.1561\/2500000011 10.1561\/2500000011"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Cerans, K.: Deciding properties of integral relational automata. In: ICALP94 Proceedings. LNCS, vol.\u00a0820, pp. 35\u201346. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58201-0_56, https:\/\/doi.org\/10.1007\/3-540-58201-0_56","DOI":"10.1007\/3-540-58201-0_56 10.1007\/3-540-58201-0_56"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Elver, M., Nagarajan, V.: TSO-CC: consistency directed cache coherence for TSO. In: HPCA. pp. 165\u2013176. IEEE Computer Society (2014). https:\/\/doi.org\/10.1109\/HPCA.2014.6835927, https:\/\/doi.org\/10.1109\/HPCA.2014.6835927","DOI":"10.1109\/HPCA.2014.6835927 10.1109\/HPCA.2014.6835927"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63\u201392 (2001). https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X, https:\/\/doi.org\/10.1016\/S0304-3975(00)00102-X","DOI":"10.1016\/S0304-3975(00)00102-X 10.1016\/S0304-3975(00)00102-X"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Lower bounds for natural proof systems. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). pp. 254\u2013266 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.16","DOI":"10.1109\/SFCS.1977.16"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Krishna, S.N., Godbole, A., Meyer, R., Chakraborty, S.: Parameterized verification under release acquire is PSPACE-complete. In: Milani, A., Woelfel, P. (eds.) PODC. pp. 482\u2013492. ACM (2022). https:\/\/doi.org\/10.1145\/3519270.3538445, https:\/\/doi.org\/10.1145\/3519270.3538445","DOI":"10.1145\/3519270.3538445 10.1145\/3519270.3538445"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: CAV. LNCS, vol.\u00a05643, pp. 477\u2013492. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36, https:\/\/doi.org\/10.1007\/978-3-642-02658-4_36","DOI":"10.1007\/978-3-642-02658-4_36 10.1007\/978-3-642-02658-4_36"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: SIGPLAN-SIGACT. pp. 649\u2013662. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837643, https:\/\/doi.org\/10.1145\/2837614.2837643","DOI":"10.1145\/2837614.2837643 10.1145\/2837614.2837643"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. FMSD 35(1), 73\u201397 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0078-9, https:\/\/doi.org\/10.1007\/s10703-009-0078-9","DOI":"10.1007\/s10703-009-0078-9 10.1007\/s10703-009-0078-9"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (aug 1974). https:\/\/doi.org\/10.1145\/361082.361093, https:\/\/doi.org\/10.1145\/361082.361093","DOI":"10.1145\/361082.361093 10.1145\/361082.361093"},{"key":"14_CR27","unstructured":"Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Informaticae 88(3), 251\u2013274 (2008), http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi88-3-03"},{"key":"14_CR28","doi-asserted-by":"publisher","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI. pp. 446\u2013455. ACM (2007). https:\/\/doi.org\/10.1145\/1250734.1250785, https:\/\/doi.org\/10.1145\/1250734.1250785","DOI":"10.1145\/1250734.1250785 10.1145\/1250734.1250785"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: TPHOLs. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27, https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27 10.1007\/978-3-642-03359-9_27"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Ros, A., Kaxiras, S.: Racer: TSO consistency via race detection. In: MICRO. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/MICRO.2016.7783736, https:\/\/doi.org\/10.1109\/MICRO.2016.7783736","DOI":"10.1109\/MICRO.2016.7783736 10.1109\/MICRO.2016.7783736"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: ACM SIGPLAN, PLDI. pp. 175\u2013186. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993520, https:\/\/doi.org\/10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520 10.1145\/1993498.1993520"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010). https:\/\/doi.org\/10.1145\/1785414.1785443, https:\/\/doi.org\/10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443 10.1145\/1785414.1785443"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57256-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:21:21Z","timestamp":1731691281000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57256-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572555","9783031572562"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57256-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}