Hybrid Multiparty Session Types -- Full Version

TL;DR

This paper introduces a novel MPST framework with hybrid types for modular, compositional protocol specification, overcoming previous limitations and ensuring semantic guarantees like liveness and deadlock freedom.

Contribution

It proposes the first semantics-preserving MPST theory for compositionality using hybrid types, with algorithms and proofs ensuring well-formed global types from subprotocols.

Findings

Developed hybrid types for subprotocol interaction

Defined a new compatibility relation for composition

Proved that compositionality preserves liveness and deadlock freedom

Abstract

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 semantic 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.