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.
CITATION STYLE
Bouajjani, A., Enea, C., Mukund, M., & Roy, R. (2019). On verifying TSO robustness for event-driven asynchronous programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11028 LNCS, pp. 225–239). Springer Verlag. https://doi.org/10.1007/978-3-030-05529-5_15
Mendeley helps you to discover research relevant for your work.