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.
翻译:我们通过将经典全存储顺序(TSO)语义扩展至回合制双人安全性游戏来研究其推广形式。在每方回合中,玩家可选择任意通信进程并执行其下一步转移。根据单方或双方玩家是否将消息从进程缓冲区传输至共享内存,我们考虑了安全性游戏问题的不同表述形式。针对所有可能的变体,我们给出了完整的可判定性图景。