Dimitrios Kouzapas ; Nobuko Yoshida - Globally Governed Session Semantics

lmcs:775 - Logical Methods in Computer Science, December 30, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:20)2014
Globally Governed Session SemanticsArticle

Authors: Dimitrios Kouzapas ; Nobuko Yoshida ORCID

    This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global session scenarios and usable for proving correctness of optimisations for globally coordinating threads and processes. The induced bisimulation is strictly more fine-grained than the standard session bisimulation. The difference between the governed and standard bisimulations only appears when more than two interleaved multiparty sessions exist. This distinct feature enables to reason real scenarios in the large-scale distributed system where multiple choreographic sessions need to be interleaved. The compositionality of the governed bisimilarity is proved through the soundness and completeness with respect to the governed reduction-based congruence. Finally, its usage is demonstrated by a thread transformation governed under multiple sessions in a real usecase in the large-scale cyberinfrustracture.


    Volume: Volume 10, Issue 4
    Published on: December 30, 2014
    Imported on: August 8, 2013
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems; Funder: UK Research and Innovation; Code: EP/L00058X/1
    • From Data Types to Session Types---A Basis for Concurrency and Distribution; Funder: UK Research and Innovation; Code: EP/K034413/1
    • Deep Drug Discovery and Deployment; Funder: UK Research and Innovation; Code: PTDC/CCI-BIO/29266/2017
    • Conversation-Based Governance for Distributed Systems by Multiparty Session Types; Funder: UK Research and Innovation; Code: EP/K011715/1
    • From Inherent Concurrency to Massive Parallelism through Type-based Optimizations; Funder: European Commission; Code: 612985

    12 Documents citing this article

    Consultation statistics

    This page has been seen 1431 times.
    This article's PDF has been downloaded 320 times.