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)语义的扩展,将其推广至基于回合制的双玩家安全博弈。在每个回合中,玩家可选择任意一个通信进程并执行其下一状态转移。根据消息是由单一玩家还是两个玩家从进程缓冲区传输至共享内存,我们探讨了安全博弈问题的不同表述形式。针对所有可能的变体,我们给出了完整的可判定性图景。