Abstract
We present Probabilistic Total Store Ordering (PTSO) – 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) Almost-Sure (Repeated) Reachability: whether a run, starting from a given initial configuration, almost surely visits (resp. almost surely repeatedly visits) a given set of target configurations. (ii) Almost-Never (Repeated) Reachability: whether a run from the initial configuration, almost never visits (resp. almost never repeatedly visits) the target. (iii) Approximate Quantitative (Repeated) Reachability: 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) Expected Average Cost: 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 decisive and eager 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.
Chapter PDF
Similar content being viewed by others
References
L. Lamport. How to make a multiprocessor that correctly executes multiprocess programs. IEEE Trans. on Computers, C-28:690–691, 1979.
Sarita V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66–76, 1996.
Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986.
Zohar Manna and Amir Pnueli. The temporal logic of reactive and concurrent systems - specification. Springer, 1992.
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. x86-tso: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89–97, 2010.
M.Z. Kwiatkowska. Survey of fairness notions. Information and Software Technology, 31(7):371–386, 1989.
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–33:13. IEEE Computer Society, 2016.
Marco Elver and Vijay Nagarajan. TSO-CC: consistency directed cache coherence for TSO. In HPCA 2014, pages 165–176. IEEE, 2014.
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Litmus: Running tests against hardware. In Parosh Aziz Abdulla and K. Rustan M. 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ücken, Germany, March 26-April 3, 2011. Proceedings, volume 6605 of Lecture Notes in Computer Science, pages 41–44. Springer, 2011.
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–306. ACM, 2010.
Luca de Alfaro. From fairness to chance. Electron. Notes Theor. Comput. Sci., 22:55–87, 1999.
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. On the verification problem for weak memory models. In Manuel V. 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–18. ACM, 2010.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. A load-buffer semantics for total store ordering. Logical Methods in Computer Science, 14(1), 2018.
W. Feller. An Introduction to Probability Theory and Its Applications, volume 1 of Texts in Statistical Science. John Wiley, 3rd edition, 1968.
V. G. Kulkarni. Modeling and Analysis of Stochastic Systems. Texts in Statistical Science. CRC Press, 2nd edition, 2009.
Parosh Aziz Abdulla, Noomene Ben Henda, and Richard Mayr. Decisive markov chains. LMCS, 3(4), 2007.
Parosh Aziz Abdulla, Noomene Ben 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, Bei**g, China, October 23-26, 2006., volume 4218 of Lecture Notes in Computer Science, pages 24–38. Springer, 2006.
Pante Stǎnicǎ. Good lower and uper bounds on binomial coefficients. 2(3), 2001.
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. What’s 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–46. Springer, 2012.
Christel Baier and Joost-Pieter Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008.
Carl G. Ritson and Scott Owens. Benchmarking weak memory models. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’16, New York, NY, USA, 2016. Association for Computing Machinery.
Changhui Lin, Vijay Nagarajan, and Rajiv Gupta. Fence sco**. In SC ’14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pages 105–116, 2014.
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 ’13, page 213–224, New York, NY, USA, 2013. Association for Computing Machinery.
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 ’10, page 295–306, New York, NY, USA, 2010. Association for Computing Machinery.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, and Krishna S. Probabilistic total store ordering. Ar**v, https://arxiv.org/abs/2201.10213, 2022.
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis. Making weak memory models fair. Ar**v, abs/2012.01067, 2020.
Chao Wang, Gustavo Petri, Yi Lv, Teng Long, and Zhiming Liu. Decidability of liveness on the TSO memory model. CoRR, abs/2107.09930, 2021.
Marta Z. 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–591. Springer, 2011.
Kousha Etessami and Mihalis Yannakakis. Recursive markov decision processes and recursive stochastic games. J. ACM, 62(2):11:1–11:69, 2015.
Tomás Brázdil, Stefan Kiefer, Antonín Kucera, and Ivana Hutarová Vareková. Runtime analysis of probabilistic programs with unbounded recursion. J. Comput. Syst. Sci., 81(1):288–310, 2015.
Javier Esparza, Antonín 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–21. IEEE Computer Society, 2004.
Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, 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–478. Springer, 2019.
Tomás Brázdil, Stefan Kiefer, Antonín Kucera, Petr Novotný, and Joost-Pieter Katoen. Zero-reachability in probabilistic multi-counter automata. In Thomas A. 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 ’14, Vienna, Austria, July 14 - 18, 2014, pages 22:1–22:10. ACM, 2014.
Tomás Brázdil, Stefan Kiefer, and Antonín Kucera. Efficient analysis of probabilistic programs with an unbounded counter. J. ACM, 61(6):41:1–41:35, 2014.
Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, and Bengt Jonsson. Simulating perfect channels with probabilistic lossy channels. Inf. Comput., 197(1-2):22–40, 2005.
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 55 of LIPIcs, pages 101:1–101:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
Parosh Aziz Abdulla, Noomene Ben Henda, Luca de Alfaro, Richard Mayr, and Sven Sandberg. Stochastic games with lossy channels. In Roberto M. 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–49. Springer, 2008.
E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Dec. 1999.
J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. D Van Nostad Co., 1966.
M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. pages 327–338, 1985.
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–407. Springer, 2009.
Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. A note on the attractor-property of infinite-state markov chain. Inf. Process. Lett., 97(2):58–63, January 2006.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Abdulla, P.A., Atig, M.F., Agarwal, R.A., Godbole, A., S., K. (2022). Probabilistic Total Store Ordering. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-99336-8_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99335-1
Online ISBN: 978-3-030-99336-8
eBook Packages: Computer ScienceComputer Science (R0)