Designing Asynchronous Multiparty Protocols with Crash-Stop Failures
Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types (MPST) with crash-stop semantics to support failure handling protocols.
We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes.
Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scibble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. In Teatrino, both Scribble and Effpi are extended to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.
Wed 19 JulDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 17:00
|Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types|
Sung-Shik Jongmans Open University of the Netherlands; CWI, Francisco Ferreira Royal Holloway, University of LondonDOI
|Asynchronous Multiparty Session Type Implementability is Decidable – Lessons Learned from Message Sequence Charts|
Felix Stutz MPI-SWSDOI
|Dynamically Updatable Multiparty Session Protocols|
|Designing Asynchronous Multiparty Protocols with Crash-Stop Failures|
Adam D. Barwell University of St Andrews and University of Oxford, Ping Hou University of Oxford, Nobuko Yoshida University of Oxford, Fangyi Zhou Imperial College LondonDOI Pre-print
|ConDRust: Scalable Deterministic Concurrency from Verifiable Rust Programs|
Felix Suchert Center for Advancing Electronics Dresden, TU Dresden, Lisza Zeidler Composable Operating Systems Group, Barkhausen Institute, Dresden, Jeronimo Castrillon TU Dresden, Germany, Sebastian Ertel Composable Operating Systems Group, Barkhausen Institute, DresdenDOI
|Information Flow Analysis for Detecting Non-Determinism in Blockchain|
Luca Olivieri Ca’ Foscari University of Venice, Vincenzo Arceri University of Parma, Italy, Luca Negrini Ca’ Foscari University of Venice, Corvallis S.r.l., Fabio Tagliaferro CYS4 Srl, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia, Fausto Spoto U. VeronaDOI