Parameterized Verification under The Total Store Order Memory Modelis EXPTIME-Complete

Abstract: In this paper, we study the problem of parameterized verification of a concurrent program running under the Total Store Order (TSO) memory  model. A concurrent program is a finite set of processes that are instances of the same pushdown system and which communicate through a set of shared variables. A memory model is a set of rules that decides in what order the memory operations done by one process are observed by the other processes. TSO is a weak memory model. In TSO, a FIFO buffer is inserted between each process and the shared memory, where a write operation is added to the buffer and it then getsnon-deterministically updated to the shared memory. This causes the order of read and write operations inside a process to be distorted when it is observed by other processes. The main result we show is that the parameterized state reachability problem of a concurrent program running under TSO is EXPTIME-complete. Note that this is an extension of a previous result which showed that the problem is PSPACE-complete when the processes are instances of a finite state system. The main advantage of extending the analysis to pushdown systems is that the concurrent programs can then use recursion.