• Media type: E-Article; Text
  • Title: Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)
  • Contributor: Barwell, Adam D. [Author]; Hou, Ping [Author]; Yoshida, Nobuko [Author]; Zhou, Fangyi [Author]
  • imprint: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023
  • Language: English
  • DOI: https://doi.org/10.4230/DARTS.9.2.9
  • Keywords: Failure Handling ; Concurrency ; Scala ; Session Types ; Code Generation
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: We introduce Teatrino, a toolchain that supports handling multiparty protocols with crash-stop failures 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 executable 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.
  • Access State: Open Access