Globally governed session semantics
File(s)
Published version
Author(s)
Kouzapas, Dimitrios
Yoshida, Nobuko
Type
Report
Abstract
This paper proposes a new 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.
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.
Date Issued
2013-01-01
Citation
Departmental Technical Report: 13/4, 2013, pp.1-32
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
32
Journal / Book Title
Departmental Technical Report: 13/4
Copyright Statement
© 2013 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
13/4