Globally Governed Session Semantics
Dimitrios Kouzapas (University of Glasgow), Nobuko Yoshida (Imperial, College London)

TL;DR
This paper introduces a new bisimulation theory for multiparty session types that accounts for global choreography specifications, enabling more precise reasoning about complex, large-scale distributed systems with multiple interleaved sessions.
Contribution
It presents a globally governed bisimulation that is more fine-grained than standard session bisimulation, with proven compositionality and practical application in large-scale distributed systems.
Findings
The governed bisimulation is strictly more fine-grained than standard bisimulation.
It is compositional, with soundness and completeness proofs.
Demonstrated application in large-scale cyberinfrastructure.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
