Reachability and Safety Games under TSO Semantics (Extended Version)

We consider games played on the transtion graph of concurrent programs running under the TotalStore Order (TSO) weak memory model. Games are frequently used to model the interaction between a system and its environment, in this case between the concurrent processes and the nondeterminisitic TSO buffer updates. The game is played by two players, who alternatinglymake a move: Theprocess playercan execute any enabled instruction of the processes, while theupdate playertakes care of updating the messages in the buffers that are between each process andthe shared memory. We show that the reachability and safety problem of this game reduce to theanalysis of single-process (non-concurrent) programs. In particular, they exhibit only finite-statebehaviour. Because of this, we introduce different notions offairness, which force the two players tobehave in a more realistic way. Both the reachability and safety problem then become undecidable.