References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole & Shankara Narayanan Krishna (2022): Probabilistic Total Store Ordering. In: Ilya Sergey: Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Lecture Notes in Computer Science 13240. Springer, pp. 317–345, doi:10.1007/978-3-030-99336-8_12.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani & Tuan Phong Ngo (2016): The Benefits of Duality in Verifying Concurrent Programs under TSO. In: Josée Desharnais & Radha Jagadeesan: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, LIPIcs 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 5:1–5:15, doi:10.4230/LIPIcs.CONCUR.2016.5.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani & Tuan Phong Ngo (2018): A Load-Buffer Semantics for Total Store Ordering. Log. Methods Comput. Sci. 14(1), doi:10.23638/LMCS-14(1:9)2018.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson & Ahmed Rezine (2012): Counter-Example Guided Fence Insertion under TSO. In: Cormac Flanagan & Barbara König: Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 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 7214. Springer, pp. 204–219, doi:10.1007/978-3-642-28756-5_15.
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Adwait Amit Godbole, Yacoub G. Hendi, Shankara Narayanan Krishna & Stephan Spengler (2023): Parameterized Verification under TSO with Data Types. In: Sriram Sankaranarayanan & Natasha Sharygina: 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 13993. Springer, pp. 588–606, doi:10.1007/978-3-031-30823-9_30.
  6. Parosh Aziz Abdulla, Mohamed Faouzi Atig & Ngo Tuan Phong (2015): The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. In: Jan Vitek: Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Lecture Notes in Computer Science 9032. Springer, pp. 308–332, doi:10.1007/978-3-662-46669-8_13.
  7. Parosh Aziz Abdulla, Mohamed Faouzi Atig & Rojin Rezvan (2020): Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4(POPL), pp. 26:1–26:29, doi:10.1145/3371094.
  8. Parosh Aziz Abdulla, Ahmed Bouajjani & Julien d'Orso (2008): Monotonic and Downward Closed Games. J. Log. Comput. 18(1), pp. 153–169, doi:10.1093/logcom/exm062.
  9. Parosh Aziz Abdulla & Bengt Jonsson (1994): Undecidable Verification Problems for Programs with Unreliable Channels. In: Serge Abiteboul & Eli Shamir: Automata, Languages and Programming, 21st International Colloquium, ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings, Lecture Notes in Computer Science 820. Springer, pp. 316–327, doi:10.1007/3-540-58201-0_78.
  10. Parosh Aziz Abdulla & Bengt Jonsson (1996): Verifying Programs with Unreliable Channels. Inf. Comput. 127(2), pp. 91–101, doi:10.1006/inco.1996.0053.
  11. ARM (2014): ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition. Available at https://developer.arm.com/documentation/ddi0406/latest/.
  12. Mohamed Faouzi Atig (2020): What is decidable under the TSO memory model?. ACM SIGLOG News 7(4), pp. 4–19, doi:10.1145/3458593.3458595.
  13. Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt & Madanlal Musuvathi (2010): On the verification problem for weak memory models. In: Manuel V. Hermenegildo & Jens Palsberg: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. ACM, pp. 7–18, doi:10.1145/1706299.1706303.
  14. Ahmed Bouajjani, Egor Derevenetc & Roland Meyer (2013): Checking and Enforcing Robustness against TSO. In: Matthias Felleisen & Philippa Gardner: 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 7792. Springer, pp. 533–553, doi:10.1007/978-3-642-37036-6_29.
  15. Ahmed Bouajjani, Roland Meyer & Eike Möhlmann (2011): Deciding Robustness against Total Store Ordering. In: Luca Aceto, Monika Henzinger & JiríSgall: Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, Lecture Notes in Computer Science 6756. Springer, pp. 428–440, doi:10.1007/978-3-642-22012-8_34.
  16. Daniel Brand & Pitro Zafiropulo (1983): On Communicating Finite-State Machines. J. ACM 30(2), pp. 323–342, doi:10.1145/322374.322380.
  17. Ashok K. Chandra, Dexter Kozen & Larry J. Stockmeyer (1981): Alternation. J. ACM 28(1), pp. 114–133, doi:10.1145/322234.322243.
  18. Alain Finkel & Philippe Schnoebelen (2001): Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1-2), pp. 63–92, doi:10.1016/S0304-3975(00)00102-X.
  19. Erich Grädel, Wolfgang Thomas & Thomas Wilke (2002): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science 2500. Springer, doi:10.1007/3-540-36387-4.
  20. IBM (2021): Power ISA, Version 3.1b. Available at https://files.openpower.foundation/s/dAYSdGzTfW4j2r2/download/OPF_PowerISA_v3.1B.pdf.
  21. Intel Corporation (2012): Intel 64 and IA-32 Architectures Software Developers Manual. Available at https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html.
  22. Leslie Lamport (1979): How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28(9), pp. 690–691, doi:10.1109/TC.1979.1675439.
  23. René Mazala (2001): Infinite Games. In: Erich Grädel, Wolfgang Thomas & Thomas Wilke: Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], Lecture Notes in Computer Science 2500. Springer, pp. 23–42, doi:10.1007/3-540-36387-4_2.
  24. Scott Owens, Susmit Sarkar & Peter Sewell (2009): A Better x86 Memory Model: x86-TSO. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Lecture Notes in Computer Science 5674. Springer, pp. 391–407, doi:10.1007/978-3-642-03359-9_27.
  25. Philippe Schnoebelen (2002): Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), pp. 251–261, doi:10.1016/S0020-0190(01)00337-4.
  26. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli & Magnus O. Myreen (2010): x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM 53(7), pp. 89–97, doi:10.1145/1785414.1785443.
  27. SPARC International, Inc. (1994): SPARC Architecture Manual Version 9. Available at https://sparc.org/wp-content/uploads/2014/01/SPARCV9.pdf.gz.
  28. Stephan Spengler & Sanchari Sil (2023): TSO Games – On the decidability of safety games under the total store order semantics, doi:10.48550/arXiv.2309.02862.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org