Designing asynchronous multiparty protocols with crash-stop failures

Adam David Barwell, Ping Hou, Nobuko Yoshida, Fangyi Zhou

Research output: Contribution to conferencePaperpeer-review

10 Downloads (Pure)

Abstract

Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types (MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. In Teatrino, both Scribble and Effpi are extended to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.
Original languageEnglish
Pages1:1-1:30
Number of pages30
DOIs
Publication statusPublished - 11 Jul 2023
Event37th European Conference on Object-Oriented Programming - Seattle, United States
Duration: 17 Jul 202321 Jul 2023
https://2023.ecoop.org

Conference

Conference37th European Conference on Object-Oriented Programming
Abbreviated titleECOOP23
Country/TerritoryUnited States
CitySeattle
Period17/07/2321/07/23
Internet address

Keywords

  • Session types
  • Concurrency
  • Failure handling
  • Code generation
  • Scala

Fingerprint

Dive into the research topics of 'Designing asynchronous multiparty protocols with crash-stop failures'. Together they form a unique fingerprint.

Cite this