TSO Games -- On the decidability of safety games under the total store order semantics (extended LMCS version with appendix)

TL;DR

This work investigates the safety (reachability) problem for two-player games built on concurrent programs under the Total Store Ordering ($TSO$) memory model, extending the classical $TSO$ semantics to interactive game settings. It provides a complete decidability and complexity classification for all possible buffer-update timing variants, grouping them into four families: Group I, Group II, Group III, and Group IV. The decidable groups (I, II, IV) reduce to finite or bounded-buffer games and are shown to be $ExpTime$-complete, while Group III (where exactly one player can update, or the case where updates can occur after a move) is undecidable via reductions from Perfect Channel Systems. A key methodological contribution is the use of SC game results and bisimulations to transfer complexity bounds to a broad class of TSO games, and the appendix contains formal undecidability proofs for Group III. The findings illuminate how buffer-update attribution and timing critically affect decidability, with implications for controller synthesis and safety verification under relaxed memory models.The main approach combines reductions between $TSO$ and $SC$ games, bisimulation techniques, and reductions from alternating Turing machines (ATM) and lossy channel systems to establish lower bounds, while constructing finite abstractions to obtain upper bounds. The results give a precise ExpTime-complete frontier for the decidable variants and demonstrate undecidability for the most expressive buffer-update schemes, providing a nuanced map of when safety games are tractable under $TSO$. The work also lays groundwork for future work on weighted updates (fence insertion) and extensions to other memory models, as well as potential stochastic game formulations.Overall, the paper advances formal verification under weak memory by charting which $TSO$-based safety games are decidable, characterizing the exact complexity, and offering a framework (via SC-TSO bisimulations) for translating between models and leveraging known results in game theory and automata.

Abstract

We consider an extension of the classical Total Store Order (TSO) semantics by expanding it to turn-based 2-player safety games. During her turn, a player can select any of the communicating processes and perform its next transition. We consider different formulations of the safety game problem depending on whether one player or both of them transfer messages from the process buffers to the shared memory. We give the complete decidability picture for all the possible alternatives.

Figures (18)

• Figure 1: A concurrent program $\mathcal{P} = \langle\mathsf{Proc}^1, \mathsf{Proc}^2\rangle$ modelling (a simplified version of) the Dekker protocol.
• Figure 2: Groups of TSO games, where players A and B are allowed to update the buffer: always, before their own move, after their own move, or never. The games in group I (light grey), II (white) and IV (dark grey) are decidable (d), the games in group III (medium grey) are undecidable (u).
• Figure 3: Concurrent program $\mathcal{P} = \langle\mathsf{Proc}^1, \mathsf{Proc}^2\rangle$
• Figure 4: TSO semantics
• Figure 5: Configurations in a bisimulation

Theorems & Definitions (39)

• Lemma 4.1: Proposition 2.21 in DBLP:conf/dagstuhl/Mazala01
• Lemma 4.2: Chapter 2 in DBLP:conf/dagstuhl/2001automata
• Lemma 4.3
• proof
• Theorem 4.4
• proof
• Theorem 4.5
• proof
• Lemma 4.6
• proof