Distributed programming using role-parametric session types in go
File(s)DTRS18-4.pdf (1.46 MB)
Published version
Author(s)
Castro, David
Hu, Raymond
Jongmans, Sung-Shik
Ng, Nicholas
Yoshida, Nobuko
Type
Report
Abstract
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.
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.
Date Issued
2018-01-01
Citation
Departmental Technical Report: 18/4, 2018, pp.1-220
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
220
Journal / Book Title
Departmental Technical Report: 18/4
Copyright Statement
© 2018 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published