Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-22012-8_34 | ICALP (2) |
Keywords | Field | DocType |
key insight,memory model,expected sequential consistency,total store,sc computation | Sequential consistency,Computer science,Algorithm,Robustness (computer science),Linear temporal logic,Memory model,Total store ordering,Mutual exclusion,Semantics,Computation | Conference |
Volume | ISSN | Citations |
6756 | 0302-9743 | 20 |
PageRank | References | Authors |
0.79 | 12 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ahmed Bouajjani | 1 | 2663 | 184.84 |
| Roland Meyer | 2 | 203 | 15.99 |
| Eike Möhlmann | 3 | 45 | 4.01 |