Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, and Rajarshi Roy
Proc. NETYS 2018, Springer LNCS 11028 (2019), 225-239.
© Springer-Verlag Berlin Heidelberg
We present a method for checking whether an event-driven asynchronous program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. We show that this verification problem can be reduced in polynomial time to a reachability problem in a program with two threads, provided that the original program satisfies a criterion called robustness against concurrency, introduced recently in the literature. This result allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity.