Journal article
Crash-stop failures in asynchronous multiparty session types
- Abstract:
-
Session types provide a typing discipline for message-passing systems. However, their theory often assumes 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 a new asynchronous multiparty session types (MPST) theory with crash-stop failures, where processes may crash arbitrarily and cease to interact after crashing. We augment asynchronous MPST and processes with crash handling branches, and integrate crash-stop failure semantics into types and processes. 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.
Our new theory covers the entire spectrum, ranging from the ideal world of total reliability to entirely unreliable scenarios where any process may crash, using optional reliability assumptions. Under these assumptions, we demonstrate the sound and complete correspondence between global and local type semantics, which guarantee deadlock-freedom, protocol conformance, and liveness of well-typed processes by construction, even in the presence of crashes.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Version of record, pdf, 901.3KB, Terms of use)
-
- Publisher copy:
- 10.46298/lmcs-21(2:5)2025
Authors
+ European Commission
More from this funder
- Funder identifier:
- https://ror.org/00k4n6c32
- Grant:
- 101093006
- Programme:
- Horizon EU TaRDIS
+ Department for Science, Innovation and Technology
More from this funder
- Funder identifier:
- https://ror.org/028z36n30
- Programme:
- Advanced Research and Invention Agency (ARIA) Safeguarded AI
+ Engineering and Physical Sciences Research Council
More from this funder
- Funder identifier:
- https://ror.org/0439y7842
- Grant:
- EP/K011715/1
- EP/T006544/2
- EP/K034413/1
- EP/L00058X/1
- EP/N027833/2
- EP/N028201/1
- EP/V000462/1
- EP/X015955/1
- EP/Y005244/1
- EP/T014709/2
- Publisher:
- Episciences
- Journal:
- Logical Methods in Computer Science More from this journal
- Volume:
- 21
- Issue:
- 2
- Pages:
- 5:1–5:71
- Publication date:
- 2025-04-18
- Acceptance date:
- 2025-02-18
- DOI:
- EISSN:
-
1860-5974
- ISSN:
-
1860-5974
- Language:
-
English
- Keywords:
- Pubs id:
-
2093694
- Local pid:
-
pubs:2093694
- Deposit date:
-
2025-03-12
- ARK identifier:
Terms of use
- Copyright holder:
- Barwell et al.
- Copyright date:
- 2025
- Rights statement:
- © A.D. Barwell, P. Hou, N. Yoshida, and F. Zhou. This is an open access article under a Creative Commons license.
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record