MobilityReadingGroup

Explicit Connection Actions in Multiparty Session Types

Raymond HU, Nobuko YOSHIDA

This work extends asynchronous multiparty session types (MPST) with explicit connection actions to support protocols with optional and dynamic participants. The actions by which endpoints are connected and disconnected are a key element of real-world protocols that is not treated in existing MPST; we demonstrate Web service and microservices use cases from our industry collaborations, which also require an expanded form of multiparty choice. These extensions do not satisfy the conservative syntactic restrictions used to ensure safety in standard MPST. Instead, we develop an approach to validate MPST safety and progress for these enriched protocols based on bounded global models of MPSTs. We present a core formalism, showing the soundness of our approach, and an implementation for MPST-based distributed programming with our extensions in Java. We discuss implementation issues related to the extensions: a practical treatment of choice subtyping for MPST progress, and multiparty correlation of dynamic binary connections.

@inproceedings{HY2017,
  author = {Raymond Hu and Nobuko Yoshida},
  title = {{Explicit Connection Actions in Multiparty Session Types}},
  booktitle = {20th International Conference on Fundamental Approaches to Software Engineering},
  series = {LNCS},
  volume = {10202},
  pages = {116--133},
  publisher = {Springer},
  year = 2017
}

@inproceedings{HY2017,
  author = {Raymond Hu and Nobuko Yoshida},
  title = {{Explicit Connection Actions in Multiparty Session Types}},
  booktitle = {20th International Conference on Fundamental Approaches to Software Engineering},
  series = {LNCS},
  volume = {10202},
  pages = {116--133},
  publisher = {Springer},
  doi = "10.1007/978-3-662-54494-5_7",
  year = 2017
}