Causality vs. Interleavings in Concurrent Game Semantics

Authors Simon Castellan, Pierre Clairambault



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.32.pdf
  • Filesize: 0.59 MB
  • 14 pages

Document Identifiers

Author Details

Simon Castellan
Pierre Clairambault

Cite AsGet BibTex

Simon Castellan and Pierre Clairambault. Causality vs. Interleavings in Concurrent Game Semantics. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.32

Abstract

We investigate relationships between interleaving and causal notions of game semantics for concurrent programming languages, focusing on the existence of canonical compact causal representations of the interleaving game semantics of programs. We perform our study on an affine variant of Idealized Parallel Algol (IPA), for which we present two games model: and interleaving model (an adaptation of Ghica and Murawski’s fully abstract games model for IPA up to may-testing), and a causal model (a variant of Rideau and Winskel’s games on event structures). Both models are sound and adequate for affine IPA. Then, we relate the two models. First we give a causality-forgetting operation mapping functorially the causal model to the interleaving one. We show that from an interleaving strategy we can reconstruct a causal strategy, from which it follows that the interleaving model is the observational quotient of the causal one. Then, we investigate several reconstructions of causal strategies from interleaving ones, showing finally that there are programs which are inherently causally ambiguous, with several distinct minimal causal representations.
Keywords
  • Game semantics
  • concurrency
  • causality
  • event structures

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, and C.-H. Luke Ong. Applying game semantics to compositional software modeling and verification. In Kurt Jensen and Andreas Podelski, editors, TACAS 2004, volume 2988 of Lecture Notes in Computer Science, pages 421-435. Springer, 2004. Google Scholar
  2. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Concurrent games. ArXiv, 2015. URL: http://arxiv.org/abs/1604.04390.
  3. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 232-243. IEEE, 2015. Google Scholar
  4. Dan R. Ghica. Geometry of synthesis: a structured approach to VLSI design. In Martin Hofmann and Matthias Felleisen, editors, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 363-375. ACM, 2007. Google Scholar
  5. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic, 151(2-3):89-114, 2008. Google Scholar
  6. Dan R. Ghica, Andrzej S. Murawski, and C.-H. Luke Ong. Syntactic control of concurrency. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings, volume 3142 of Lecture Notes in Computer Science, pages 683-694. Springer, 2004. Google Scholar
  7. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. Google Scholar
  8. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. Google Scholar
  9. Paul-André Melliès and Samuel Mimram. Asynchronous games: Innocence without alternation. In Luís Caires and Vasco Thudichum Vasconcelos, editors, CONCUR, volume 4703 of LNCS, pages 395-411. Springer, 2007. Google Scholar
  10. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS) 2006, 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81-90. IEEE Computer Society, 2006. Google Scholar
  11. Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, pages 409-418. IEEE Computer Society, 2011. Google Scholar
  12. Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, volume 11, pages 409-418, 2011. Google Scholar
  13. Ulrich Schöpp. On the relation of interaction semantics to continuations and defunctionalization. Logical Methods in Computer Science, 10(4), 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail