Barwell, Adam D.
[VerfasserIn];
Hou, Ping
[VerfasserIn];
Yoshida, Nobuko
[VerfasserIn];
Zhou, Fangyi
[VerfasserIn]
;
Adam D. Barwell and Ping Hou and Nobuko Yoshida and Fangyi Zhou
[MitwirkendeR]
Designing Asynchronous Multiparty Protocols with Crash-Stop Failures (Artifact)
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.