一句话:提出角色参数化多体会话类型理论,并为 Go 生成静态类型端点 API,以安全实现动态参与者协议。
论文研究参与者数量与种类动态实例化的消息传递协议的安全编程。作者提出首个支持带索引角色的参数化协议的分布式多体会话类型(MPST)理论:静态推断协议诱导的角色变体,并将协议解耦投影到各变体,使分布式端点可由不同程序员、技术或语言独立实现。作者证明角色变体推断与良构性检查可判定、投影正确,并实现 Go 工具链,生成协议与变体专用的轻量类型包装 API 族;经原生 Go 类型检查的端点程序只执行符合源协议的 I/O。该框架支持多通道、混合传输与通道传递,并用微基准和真实应用评估适用性与运行时性能。
This paper presents a framework for the static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated. We develop the first theory of distributed multiparty session types (MPST) to support parameterised protocols with indexed roles—our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each variant. This enables safe MPST-based programming of the parameterised endpoints in distributed settings: each endpoint can be implemented separately by different programmers, using different techniques (or languages). We prove the decidability of role variant inference and well-formedness checking, and the correctness of projection. We implement our theory as a toolchain for programming such role-parametric MPST protocols in Go. Our approach is to generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The APIs ensure a well-typed Go endpoint program (by native Go type checking) will perform only compliant I/O actions w.r.t. the source protocol. We leverage the abstractions of MPST to support the specification and implementation of Go applications involving multiple channels, possibly over mixed transports (e.g., Go channels, TCP), and channel passing via a unified programming interface. We evaluate the applicability and run-time performance of our generated APIs using microbenchmarks and real-world applications.
@article{paperbot633,
title = {Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures},
author = {David Castro and Raymond Hu and Sung-Shik Jongmans and Nicholas Ng and Nobuko Yoshida},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290342}
}