DISENTANGLING PARALLELISM AND INTERFERENCE IN GAME SEMANTICS

被引:0
作者
Castellan, Simon [1 ]
Clairambault, Pierre [2 ]
机构
[1] Univ Rennes, Inria, CNRS, IRISA, Rennes, France
[2] Aix Marseille Univ, CNRS, LIS, Marseille, France
关键词
Denotational semantics; game semantics; concurrent games; FULL ABSTRACTION; EVENT STRUCTURES; PCF;
D O I
10.46298/LMCS-20(3:24)2024
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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 (IAA(/))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.
引用
收藏
页数:130
相关论文
共 71 条
  • [1] A fully abstract game semantics for general references
    Abramsky, S
    Honda, K
    McCusker, G
    [J]. THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 334 - 344
  • [2] Abramsky S., 1999, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), P431, DOI 10.1109/LICS.1999.782638
  • [3] Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI 10.1006/inco2000.2930
  • [4] Game Semantics for Access Control
    Abramsky, Samson
    Jagadeesan, Radha
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 249 : 135 - 156
  • [5] Abramsky Samson, 1996, ELECT NOTES THEOR CO, V3, P2, DOI [10.1016/S1571-0661(05)80398-6, DOI 10.1016/S1571-0661(05)80398-6]
  • [6] Abramsky Samson, 1999, Computational logic
  • [7] Symmetry in Concurrent Games
    Castellan, Simon
    Clairambault, Pierre
    Winskel, Glynn
    [J]. PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [8] Two Sides of the Same Coin: Session Types and Game Semantics A Synchronous Side and an Asynchronous Side
    Castellan, Simon
    Yoshida, Nobuko
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
  • [9] The concurrent game semantics of Probabilistic PCF
    Castellan, Simon
    Clairambault, Pierre
    Paquet, Hugo
    Winskel, Glynn
    [J]. LICS'18: PROCEEDINGS OF THE 33RD ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 2018, : 215 - 224
  • [10] THIN GAMES WITH SYMMETRY AND CONCURRENT HYLAND-ONG GAMES
    Castellan, Simon
    Clairambault, Pierre
    Winskel, Glynn
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (01) : 18:1 - 18:85