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. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Bouajjani, A., Meyer, R., & Möhlmann, E. (2011). Deciding robustness against total store ordering. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6756 LNCS, pp. 428–440). https://doi.org/10.1007/978-3-642-22012-8_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
