@inproceedings{conf/icalp/BouajjaniMM2011, Author = {Ahmed Bouajjani and Roland Meyer and Eike Möhlmann}, Title = {Deciding Robustness against Total Store Ordering}, Year = {2011}, Pages = {428-440}, Editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jiri}, Publisher = {Springer Berlin Heidelberg}, Series = {Lecture Notes in Computer Science}, Edition = {6756}, Booktitle = {Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II}, Doi = {10.1007/978-3-642-22012-8_34}, Url = {http://dx.doi.org/10.1007/978-3-642-22012-8_34}, type = {inproceedings}, note = {We address the problem of deciding robustness of a program against the total store ordering (TSO) relaxed memory model, i.e., of checking whether the behaviour under TSO coincides with the expected sequential consistency (SC) semantics. We prove that this}, Abstract = {We address the problem of deciding robustness of a program against the total store ordering (TSO) relaxed memory model, i.e., of checking whether the behaviour under TSO coincides with the expected sequential consistency (SC) semantics. We prove that this problem is PSpace-complete. The key insight is that violations to robustness can be detected on pairs of SC computations.} } @COMMENT{Bibtex file generated on }