Global progress for dynamically interleaved multiparty sessions
File(s)cdyp.pdf (592.36 KB)
Accepted version
Author(s)
Coppo, M
Dezani-Ciancaglini, M
Yoshida, N
Padovani, L
Type
Journal Article
Abstract
A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositional communication type system, a novel static interaction type system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.
Date Issued
2014-11-10
Date Acceptance
2014-03-06
Citation
Mathematical Structures in Computer Science, 2014, 760
ISSN
1469-8072
Publisher
Cambridge University Press (CUP)
Journal / Book Title
Mathematical Structures in Computer Science
Volume
760
Copyright Statement
© Cambridge University Press 2014. The final publication is available via Cambridge Journals Online at https://dx.doi.org/10.1017/S0960129514000188
Identifier
PII: S0960129514000188
Publication Status
Published