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.
翻译:博弈语义是一种指称语义,它以组合方式呈现各类带效应程序的计算行为。其著名成就之一是在单一框架内为具有多种计算效应的编程语言获得了完全抽象结果。这被称为语义立方或Abramsky立方,对于顺序确定性程序,它建立了策略上的特定条件("纯真性"、"良括号性"、"可见性")与相应计算效应缺失之间的对应关系。在顺序确定性范畴之外,仍存在大量基于博弈语义的完全抽象结果,但它们不再适用于统一框架。特别地,Ghica和Murawski针对共享状态并发(IA)的完全抽象模型缺乏对应的纯并行程序概念——我们认为并行性与干扰(即状态加信号量)在此模型中相互纠缠。本文构建了Ghica和Murawski模型的因果版本,该模型对IA同样具有完全抽象性。我们提出了并行纯真性与顺序性这两个组合条件,分别禁止干扰与并行性,从而导出四个完全抽象结果。据我们所知,这是Abramsky语义立方计划首次向顺序确定性范畴之外的领域拓展。