Document Open Access Logo

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

Authors Adam D. Barwell , Ping Hou , Nobuko Yoshida , Fangyi Zhou



PDF
Thumbnail PDF

Artifact Description

DARTS.9.2.9.pdf
  • Filesize: 0.59 MB
  • 3 pages

Document Identifiers

Author Details

Adam D. Barwell
  • University of St. Andrews, UK
  • University of Oxford, UK
Ping Hou
  • University of Oxford, UK
Nobuko Yoshida
  • University of Oxford, UK
Fangyi Zhou
  • Imperial College London, UK
  • University of Oxford, UK

Acknowledgements

We thank the anonymous reviewers for their useful comments and suggestions. We thank Jia Qing Lim for his contribution to the Effpi extension. We thank Alceste Scalas for useful discussions and advice in the development of this paper and for his assistance with Effpi.

Cite AsGet BibTex

Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 9:1-9:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/DARTS.9.2.9

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy

Abstract

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Source code generation
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
  • Theory of computation → Distributed computing models
Keywords
  • Session Types
  • Concurrency
  • Failure Handling
  • Code Generation
  • Scala

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing asynchronous multiparty protocols with crash-stop failures. CoRR, abs/2305.06238, 2023. URL: https://doi.org/10.48550/arXiv.2305.06238.
  2. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In 8th International Symposium on Trustworthy Global Computing - Volume 8358, TGC 2013, pages 22-41, Berlin, Heidelberg, 2014. Springer-Verlag. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail