Department of Information Technology

Deciding Robustness against Total Store Ordering


Roland Meyer

Date and Time

Thursday, November 24th, 2011 at 10:30


Polacksbacken, room 1145


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.

Back to the seminar page

Updated  2011-10-31 16:03:50 by Frédéric Haziza.