Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols
Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols
复制标题
DOI：
10.4230/lipics.ecoop.2023.6
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
David Castro-Perez;N. Yoshida
中科院分区：
文献类型：
--
作者：
David Castro-Perez;N. Yoshida
多方会话类型（MPST）是一种类型规则，保证并发和分布式系统中没有死锁和通信错误。然而，现有的MPST框架不支持具有动态无界参与者的协议，并且不能表达需要将新参与者引入到协议中的许多常见编程模式。这就为MPST在支持创建新参与者（进程、轻量级线程等）并通过消息传递进行通信的语言（如Go或Erlang）中的采用带来了障碍。本文提出了动态更新多方会话协议，一个新的MPST理论（DMST），支持协议与无限数量的新鲜参与者，其通信拓扑结构是动态更新的。我们证明了DMst保证死锁自由和活性。我们实现了一个工具链GoScr（Go-Scribble），它从DMst生成Go实现，通过构造确保不同的参与者只执行符合给定协议规范的I/O操作。我们通过以下方式评估我们的工具链：（1）从现有的基准测试、教科书和文献中实现代表性的并行和并发算法;（2）对于计算昂贵的基准测试，与幼稚的实现相比，GoScr不会引入显著的开销;（3）建立了三个现实的协议（动态任务委托，递归域名系统，和并行Min-Max策略）在GoScr中，不能用以前的会话类型理论表示。
Multiparty Session Types (MPST) are a typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants , and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This paper proposes Dynamically Updatable Multiparty Session Protocols , a new MPST theory ( DMst ) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable . We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst , ensuring by construction , that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.