{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:38:10Z","timestamp":1742927890254,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030993351"},{"type":"electronic","value":"9783030993368"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present <jats:italic>Probabilistic Total Store Ordering (PTSO)<\/jats:italic> \u2013 a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational semantics of PTSO induces an infinite-state Markov chain. We resolve the inherent non-determinism due to process schedulings and memory updates according to given probability distributions. We provide a comprehensive set of results showing the decidability of several properties for PTSO, namely (i) <jats:italic>Almost-Sure (Repeated) Reachability<\/jats:italic>: whether a run, starting from a given initial configuration, almost surely visits (resp. almost surely repeatedly visits) a given set of target configurations. (ii) <jats:italic>Almost-Never (Repeated) Reachability<\/jats:italic>: whether a run from the initial configuration, almost never visits (resp. almost never repeatedly visits) the target. (iii) <jats:italic>Approximate Quantitative (Repeated) Reachability<\/jats:italic>: to approximate, up to an arbitrary degree of precision, the measure of runs that start from the initial configuration and (repeatedly) visit the target. (iv) <jats:italic>Expected Average Cost:<\/jats:italic> to approximate, up to an arbitrary degree of precision, the expected average cost of a run from the initial configuration to the target. We derive our results through a nontrivial combination of results from the classical theory of (infinite-state) Markov chains, the theories of <jats:italic>decisive<\/jats:italic> and <jats:italic>eager<\/jats:italic> Markov chains, specific techniques from combinatorics, as well as, decidability and complexity results for the classical (non-probabilistic) TSO semantics. As far as we know, this is the first work that considers probabilistic verification of programs running on weak memory models.<\/jats:p>","DOI":"10.1007\/978-3-030-99336-8_12","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"317-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Probabilistic Total Store Ordering"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8229-3481","authenticated-orcid":false,"given":"Mohamed Faouzi","family":"Atig","sequence":"additional","affiliation":[]},{"given":"Raj Aryan","family":"Agarwal","sequence":"additional","affiliation":[]},{"given":"Adwait","family":"Godbole","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0925-398X","authenticated-orcid":false,"given":"Krishna","family":"S.","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"L.\u00a0Lamport. How to make a multiprocessor that correctly executes multiprocess programs. IEEE Trans. on Computers, C-28:690\u2013691, 1979.","DOI":"10.1109\/TC.1979.1675439"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Sarita\u00a0V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66\u201376, 1996.","DOI":"10.1109\/2.546611"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Zohar Manna and Amir Pnueli. The temporal logic of reactive and concurrent systems - specification. Springer, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Peter Sewell, Susmit Sarkar, Scott Owens, Francesco\u00a0Zappa Nardelli, and Magnus\u00a0O. Myreen. x86-tso: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM, 53(7):89\u201397, 2010.","DOI":"10.1145\/1785414.1785443"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"M.Z. Kwiatkowska. Survey of fairness notions. Information and Software Technology, 31(7):371\u2013386, 1989.","DOI":"10.1016\/0950-5849(89)90159-6"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Alberto Ros and Stefanos Kaxiras. Racer: TSO consistency via race detection. In 49th Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO 2016, Taipei, Taiwan, October 15-19, 2016, pages 33:1\u201333:13. IEEE Computer Society, 2016.","DOI":"10.1109\/MICRO.2016.7783736"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Marco Elver and Vijay Nagarajan. TSO-CC: consistency directed cache coherence for TSO. In HPCA 2014, pages 165\u2013176. IEEE, 2014.","DOI":"10.1109\/HPCA.2014.6835927"},{"key":"12_CR9","unstructured":"Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Litmus: Running tests against hardware. In Parosh\u00a0Aziz Abdulla and K.\u00a0Rustan\u00a0M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, volume 6605 of Lecture Notes in Computer Science, pages 41\u201344. Springer, 2011."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Changhui Lin, Vijay Nagarajan, and Rajiv Gupta. Efficient sequential consistency using conditional fences. In Valentina Salapura, Michael Gschwind, and Jens Knoop, editors, 19th International Conference on Parallel Architectures and Compilation Techniques, PACT 2010, Vienna, Austria, September 11-15, 2010, pages 295\u2013306. ACM, 2010.","DOI":"10.1145\/1854273.1854312"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Luca de\u00a0Alfaro. From fairness to chance. Electron. Notes Theor. Comput. Sci., 22:55\u201387, 1999.","DOI":"10.1016\/S1571-0661(05)80597-3"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Mohamed\u00a0Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. On the verification problem for weak memory models. In Manuel\u00a0V. Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 7\u201318. ACM, 2010.","DOI":"10.1145\/1706299.1706303"},{"key":"12_CR13","unstructured":"Parosh\u00a0Aziz Abdulla, Mohamed\u00a0Faouzi Atig, Ahmed Bouajjani, and Tuan\u00a0Phong Ngo. A load-buffer semantics for total store ordering. Logical Methods in Computer Science, 14(1), 2018."},{"key":"12_CR14","unstructured":"W.\u00a0Feller. An Introduction to Probability Theory and Its Applications, volume\u00a01 of Texts in Statistical Science. John Wiley, 3rd edition, 1968."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"V.\u00a0G. Kulkarni. Modeling and Analysis of Stochastic Systems. Texts in Statistical Science. CRC Press, 2nd edition, 2009.","DOI":"10.1201\/b12749"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Noomene\u00a0Ben Henda, and Richard Mayr. Decisive markov chains. LMCS, 3(4), 2007.","DOI":"10.2168\/LMCS-3(4:7)2007"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Noomene\u00a0Ben Henda, Richard Mayr, and Sven Sandberg. Eager markov chains. In Susanne Graf and Wenhui Zhang, editors, Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006., volume 4218 of Lecture Notes in Computer Science, pages 24\u201338. Springer, 2006.","DOI":"10.1007\/11901914_5"},{"key":"12_CR18","unstructured":"Pante St\u01cenic\u01ce. Good lower and uper bounds on binomial coefficients. 2(3), 2001."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Mohamed\u00a0Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. What\u2019s decidable about weak memory models? In Helmut Seidl, editor, 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, volume 7211 of Lecture Notes in Computer Science, pages 26\u201346. Springer, 2012.","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"12_CR20","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008."},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Carl\u00a0G. Ritson and Scott Owens. Benchmarking weak memory models. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP \u201916, New York, NY, USA, 2016. Association for Computing Machinery.","DOI":"10.1145\/2851141.2851150"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Changhui Lin, Vijay Nagarajan, and Rajiv Gupta. Fence scoping. In SC \u201914: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pages 105\u2013116, 2014.","DOI":"10.1109\/SC.2014.14"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Yuelu Duan, Abdullah Muzahid, and Josep Torrellas. Weefence: Toward making fences free in tso. In Proceedings of the 40th Annual International Symposium on Computer Architecture, ISCA \u201913, page 213\u2013224, New York, NY, USA, 2013. Association for Computing Machinery.","DOI":"10.1145\/2485922.2485941"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Changhui Lin, Vijay Nagarajan, and Rajiv Gupta. Efficient sequential consistency using conditional fences. In Proceedings of the 19th International Conference on Parallel Architectures and Compilation Techniques, PACT \u201910, page 295\u2013306, New York, NY, USA, 2010. Association for Computing Machinery.","DOI":"10.1145\/1854273.1854312"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Mohamed\u00a0Faouzi Atig, Raj\u00a0Aryan Agarwal, Adwait Godbole, and Krishna S. Probabilistic total store ordering. ArXiv, https:\/\/arxiv.org\/abs\/2201.10213, 2022.","DOI":"10.1007\/978-3-030-99336-8_12"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis. Making weak memory models fair. ArXiv, abs\/2012.01067, 2020.","DOI":"10.1145\/3485475"},{"key":"12_CR27","unstructured":"Chao Wang, Gustavo Petri, Yi\u00a0Lv, Teng Long, and Zhiming Liu. Decidability of liveness on the TSO memory model. CoRR, abs\/2107.09930, 2021."},{"key":"12_CR28","unstructured":"Marta\u00a0Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585\u2013591. Springer, 2011."},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Kousha Etessami and Mihalis Yannakakis. Recursive markov decision processes and recursive stochastic games. J. ACM, 62(2):11:1\u201311:69, 2015.","DOI":"10.1145\/2699431"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Br\u00e1zdil, Stefan Kiefer, Anton\u00edn Kucera, and Ivana\u00a0Hutarov\u00e1 Varekov\u00e1. Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci., 81(1):288\u2013310, 2015.","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Javier Esparza, Anton\u00edn Kucera, and Richard Mayr. Model checking probabilistic pushdown automata. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 12\u201321. IEEE Computer Society, 2004.","DOI":"10.1109\/LICS.2004.1319596"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Br\u00e1zdil, Krishnendu Chatterjee, Anton\u00edn Kucera, Petr Novotn\u00fd, and Dominik Velan. Deciding fast termination for probabilistic VASS with nondeterminism. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 462\u2013478. Springer, 2019.","DOI":"10.1007\/978-3-030-31784-3_27"},{"key":"12_CR33","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Br\u00e1zdil, Stefan Kiefer, Anton\u00edn Kucera, Petr Novotn\u00fd, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. In Thomas\u00a0A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS \u201914, Vienna, Austria, July 14 - 18, 2014, pages 22:1\u201322:10. ACM, 2014.","DOI":"10.1145\/2603088.2603161"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Tom\u00e1s Br\u00e1zdil, Stefan Kiefer, and Anton\u00edn Kucera. Efficient analysis of probabilistic programs with an unbounded counter. J. ACM, 61(6):41:1\u201341:35, 2014.","DOI":"10.1145\/2629599"},{"key":"12_CR35","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Christel Baier, S.\u00a0Purushothaman Iyer, and Bengt Jonsson. Simulating perfect channels with probabilistic lossy channels. Inf. Comput., 197(1-2):22\u201340, 2005.","DOI":"10.1016\/j.ic.2004.12.001"},{"key":"12_CR36","unstructured":"Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre Carlier. Analysing decisive stochastic processes. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume\u00a055 of LIPIcs, pages 101:1\u2013101:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2016."},{"key":"12_CR37","unstructured":"Parosh\u00a0Aziz Abdulla, Noomene\u00a0Ben Henda, Luca de\u00a0Alfaro, Richard Mayr, and Sven Sandberg. Stochastic games with lossy channels. In Roberto\u00a0M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 35\u201349. Springer, 2008."},{"key":"12_CR38","unstructured":"E.M. Clarke, O.\u00a0Grumberg, and D.\u00a0Peled. Model Checking. MIT Press, Dec. 1999."},{"key":"12_CR39","unstructured":"J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. D Van Nostad Co., 1966."},{"key":"12_CR40","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. pages 327\u2013338, 1985.","DOI":"10.1109\/SFCS.1985.12"},{"key":"12_CR41","doi-asserted-by":"crossref","unstructured":"Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-tso. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 391\u2013407. Springer, 2009.","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. A note on the attractor-property of infinite-state markov chain. Inf. Process. Lett., 97(2):58\u201363, January 2006.","DOI":"10.1016\/j.ipl.2005.09.011"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99336-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T05:08:18Z","timestamp":1731647298000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99336-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030993351","9783030993368"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99336-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/esop","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":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","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":"21","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":"0","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.5","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":"7","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)"}}]}}