Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection
复制标题
混合多方会话类型：通过端点投影实现协议规范的组合性
DOI：
10.1145/3586031
复制
发表时间：
2023
影响因子：
--
通讯作者：
Gheri L
中科院分区：
文献类型：
--
作者：
Gheri L
多方会话类型(MPST)是分布式消息传递系统的规范和验证框架。系统的通信协议被指定为全局类型，通过端点投影从全局类型中获得局部类型的集合(局部进程实现)。全局类型是整个系统的单一规范实体，由完全了解通信协议的设计人员指定。另一方面，分布式系统通常用它们的组件来描述：不同的设计者负责为每个组件提供一个子协议。在文献中已经解决了全局协议的模块化规范的问题，但最新技术仅关注双输入/输出兼容性。我们的工作克服了这一限制。我们提出了分布式协议规范的第一个多方可组合性MPST理论，即保持语义，允许两个或多个组件的组合，并保持完整的MPST表达。我们引入了混合类型来描述相互作用的子协议，定义了一种新的兼容关系，明确地描述了一种将多个子协议组合成结构良好的全局类型的算法，并证明了组合性保持投影，从而保持了活跃性和死锁自由等语义保证。最后，我们针对真实世界的案例研究对我们的工作进行了测试，并顺利地将我们的新兼容性扩展到具有委托和显式连接的MPST。
Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as aglobal type, from which a collection oflocal types(local process implementations) is obtained byendpoint projection. A global type is a single disciplining entity for the whole system, specified byone designerthat has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of theircomponents: 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 ofmultiparty compositionality for distributed protocol specificationthat is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introducehybrid typesfor describing subprotocols interacting with each other, define a novelcompatibility relation, explicitly describe an algorithm for composing multiple subprotocols into awell-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.