一句话：为共享状态并发博弈语义构造因果模型，分离并行与干扰，得到四个完全抽象结果并扩展语义立方体。
博弈语义以组合方式刻画带效应程序行为，其经典成就是 Abramsky 语义立方体：对顺序确定程序，用策略上的 innocence、well-bracketing、visibility 等条件对应效应缺失，统一给出完全抽象结果。但顺序确定之外的结果难以纳入统一框架。Ghica 与 Murawski 针对共享状态并发（IA）的完全抽象模型缺少对应的纯并行概念，导致并行性与干扰纠缠。本文构造该模型的因果版本，同样对 IA 完全抽象，并给出组合性条件 parallel innocence 与 sequentiality，分别禁止干扰与并行，得到四个完全抽象结果。这是首次将 Abramsky 语义立方体扩展到顺序确定世界之外。
Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a variety of computational effects, in a single framework. This is known as the semantic cube or Abramsky's cube, which for sequential deterministic programs establishes a correspondence between certain conditions on strategies (''innocence'', ''well-bracketing'', ''visibility'') and the absence of matching computational effects. Outside of the sequential deterministic realm, there are still a wealth of game semantics-based full abstraction results; but they no longer fit in a unified canvas. In particular, Ghica and Murawski's fully abstract model for shared state concurrency (IA) does not have a matching notion of pure parallel program-we say that parallelism and interference (i.e. state plus semaphores) are entangled. In this paper we construct a causal version of Ghica and Murawski's model, also fully abstract for IA. We provide compositional conditions parallel innocence and sequentiality, respectively banning interference and parallelism, and leading to four full abstraction results. To our knowledge, this is the first extension of Abramsky's semantic cube programme beyond the sequential deterministic world.
@article{paperbot2724,
title = {Disentangling Parallelism and Interference in Game Semantics},
author = {Simon Castellan and Pierre Clairambault},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:24)2024}
}