DARTS.9.2.9.pdf
- Filesize: 0.59 MB
- 3 pages
Document
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)
Authors
Adam D. Barwell 
,
Ping Hou ,
Nobuko Yoshida ,
Fangyi Zhou
-
Part of:
Issue:
Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Volume: DARTS, Volume 9 (ECOOP 2023)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-11
Artifact Description
Document Identifiers
Author Details
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
https://doi.org/10.4230/DARTS.9.2.9
Artifact
DARTS-9-2-9-artifact-94cc09960ca3a9558cc30925291eca5d.tar.gz
(Filesize: 1.28 GB)
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)
0PDF Downloads
References
- 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.
- 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.