University of Hertfordshire

By the same authors

Standard

Distributed Programming using Role-Parametric Session Types in Go : Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures. / Castro, David; Hu, Raymond; Jongmans, Sung-Shik; Ng, Nicholas; Yoshida, Nobuko.

In: Proceedings of the ACM on Programming Languages, Vol. 3, No. POPL, 29, 02.01.2019.

Research output: Contribution to journalArticle

Harvard

APA

Vancouver

Author

Bibtex

@article{45b7ce1c1d464d38ae53e448ce81624a,
title = "Distributed Programming using Role-Parametric Session Types in Go: Statically-Typed Endpoint APIs for Dynamically-Instantiated Communication Structures",
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 asrole 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 awell-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.",
keywords = "Multiparty session types, Indexed roles, Distributed programming, Go",
author = "David Castro and Raymond Hu and Sung-Shik Jongmans and Nicholas Ng and Nobuko Yoshida",
note = "{\textcopyright} 2019 Copyright held by the owner/author(s); 46th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2019 ; Conference date: 16-01-2019 Through 19-01-2019",
year = "2019",
month = jan,
day = "2",
doi = "10.1145/3290342",
language = "English",
volume = "3",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
publisher = "ACM Digital Library",
number = "POPL",
url = "https://popl19.sigplan.org/home",

}

RIS

TY - JOUR

T1 - Distributed Programming using Role-Parametric Session Types in Go

T2 - 46th ACM SIGPLAN Symposium on Principles of Programming Languages

AU - Castro, David

AU - Hu, Raymond

AU - Jongmans, Sung-Shik

AU - Ng, Nicholas

AU - Yoshida, Nobuko

N1 - Conference code: 46

PY - 2019/1/2

Y1 - 2019/1/2

N2 - 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 asrole 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 awell-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.

AB - 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 asrole 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 awell-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.

KW - Multiparty session types

KW - Indexed roles

KW - Distributed programming

KW - Go

U2 - 10.1145/3290342

DO - 10.1145/3290342

M3 - Article

VL - 3

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 29

Y2 - 16 January 2019 through 19 January 2019

ER -