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