TSO Games -- On the decidability of safety games under the total store order semantics

TL;DR

This paper extends classical Total Store Order semantics to turn-based safety games, analyzing the decidability of various message transfer scenarios between players and buffers.

Contribution

It provides a complete decidability classification for safety games under extended TSO semantics with different message transfer conditions.

Findings

Decidability results vary depending on message transfer rules.

Complete classification of decidability for all game variants.

Framework applicable to analyzing concurrent system behaviors.

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.