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)语义的一种扩展,将其扩展为基于回合制的双人安全性游戏。在玩家回合中,该玩家可以选择任意一个通信进程并执行其下一个转移。我们根据是一个玩家还是两个玩家将消息从进程缓冲区传输到共享内存,考虑了安全性游戏问题的不同表述形式。我们给出了所有可能情形下完整的可判定性图景。