MobilityReadingGroup

Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection

Lorenzo GHERI , Nobuko YOSHIDA

Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as a global type, from which a collection of local types (local process implementations) is obtained by endpoint projection. A global type is a single disciplining entity for the whole system, specified by one designer that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their components: a different designer is in charge of providing a subprotocol for each component. The problem of modular specification of global protocols has been addressed in the literature, but the state of the art focuses only on dual input/output compatibility. Our work overcomes this limitation. We propose the first MPST theory of multiparty compositionality for distributed protocol specification that is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introduce hybrid types for describing subprotocols interacting with each other, define a novel compatibility relation, explicitly describe an algorithm for composing multiple subprotocols into a well-formed global type, and prove that compositionality preserves projection, thus retaining semantics guarantees, such as liveness and deadlock freedom. Finally, we test our work against real-world case studies and we smoothly extend our novel compatibility to MPST with delegation and explicit connections.

@inproceedings{GY2023,
  author = {Lorenzo Gheri and Nobuko Yoshida},
  title = {{Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection}},
  booktitle = {OOPSLA 2023: Conference on Object-Oriented Programming Systems, Languages and Applications},
  series = {PACMPL},
  volume = {7},
  issue = {OOPSLA},
  pages = {112--142},
  publisher = {ACM},
  year = 2023
}

@inproceedings{GY2023,
  author = {Lorenzo Gheri and Nobuko Yoshida},
  title = {{Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection}},
  booktitle = {OOPSLA 2023: Conference on Object-Oriented Programming Systems, Languages and Applications},
  series = {PACMPL},
  volume = {7},
  issue = {OOPSLA},
  pages = {112--142},
  publisher = {ACM},
  doi = "10.1145/3586031",
  year = 2023
}