Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)

  • Adam David Barwell (Creator)
  • Ping Hou (Creator)
  • Nobuko Yoshida (Creator)
  • Fangyi Zhou (Creator)



We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop fail- ures and crash-handling behaviours. Teatrino accompanies the novel MPST theory in the related article, and enables users to generate fault-tolerant protocol-conforming Scala code from Scribble protocols. Local types are projected from the global protocol, enabling correctness-by-construction, and are expressed directly as Scala types via the Effpi concurrency library. Teatrino extends both Scribble and Effpi with support for crash-stop behaviour. The generated Scala code is execut- able and can be further integrated with existing systems. The accompanying theory in the related article guarantees deadlock-freedom and liveness properties for failure handling protocols and their implementation. This artifact includes examples, extended from both session type and distributed systems literature, featured in the related article.
Date made available2023

Cite this