MobilityReadingGroup

Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types

Nobuko YOSHIDA, Fangyi ZHOU, Francisco FERREIRA

Multiparty session types (MPST) provide a typing discipline for message passing concurrency, ensuring deadlock freedom for distributed processes. This paper first summarises the relationship between MPST and communicating finite state machines (CFSMs), which offers not only theoretical justifications of MPST but also a guidance to implement MPST in practice. As one of the applications, we present νScr (NuScr), an extensible toolchain for MPST-based multiparty protocols. The toolchain can convert multiparty protocols in the Scribble protocol description language into global types in the MPST theory; global types are projected into local types, and local types are converted to their corresponding CFSMs. The toolchain also generates APIs from CFSMs that implement endpoints in the protocol. Our design allows for language-independent code generation, and opens possibilities to generate APIs in various programming languages. We design our toolchain with modularity and extensibility in mind, so that extensions of core MPST can be easily integrated within our framework. As a case study, we show the implementation of the nested protocol extension in νScr, to showcase our extensibility.

@inproceedings{YZF2021,
  author = {Nobuko Yoshida and Fangyi Zhou and Francisco Ferreira},
  title = {{Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types}},
  booktitle = {23rd International Symposium on Fundamentals of Computation Theory},
  series = {LNCS},
  volume = {12867},
  pages = {18--35},
  publisher = {Springer},
  year = 2021
}

@inproceedings{YZF2021,
  author = {Nobuko Yoshida and Fangyi Zhou and Francisco Ferreira},
  title = {{Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types}},
  booktitle = {23rd International Symposium on Fundamentals of Computation Theory},
  series = {LNCS},
  volume = {12867},
  pages = {18--35},
  publisher = {Springer},
  doi = "10.1007/978-3-030-86593-1_2",
  year = 2021
}