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 intro...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Association for Computing Machinery
2023
|
| _version_ | 1797112139551342592 |
|---|---|
| author | Barwell, A Hou, P Yoshida, N Zhou, F |
| author_facet | Barwell, A Hou, P Yoshida, N Zhou, F |
| author_sort | Barwell, A |
| collection | OXFORD |
| description | 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 deadlockfreedom, 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 Scribble multiparty protocol language to generate protocol-conforming
Scala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi
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. |
| first_indexed | 2024-03-07T08:19:59Z |
| format | Conference item |
| id | oxford-uuid:4c8c642f-6515-43ec-a1da-651c97c3d955 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T08:19:59Z |
| publishDate | 2023 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:4c8c642f-6515-43ec-a1da-651c97c3d9552024-01-23T10:37:53ZDesigning asynchronous multiparty protocols with crash-stop failuresConference itemhttp://purl.org/coar/resource_type/c_5794uuid:4c8c642f-6515-43ec-a1da-651c97c3d955EnglishSymplectic ElementsAssociation for Computing Machinery2023Barwell, AHou, PYoshida, NZhou, FSession 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 deadlockfreedom, 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 Scribble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi 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. |
| spellingShingle | Barwell, A Hou, P Yoshida, N Zhou, F Designing asynchronous multiparty protocols with crash-stop failures |
| title | Designing asynchronous multiparty protocols with crash-stop failures |
| title_full | Designing asynchronous multiparty protocols with crash-stop failures |
| title_fullStr | Designing asynchronous multiparty protocols with crash-stop failures |
| title_full_unstemmed | Designing asynchronous multiparty protocols with crash-stop failures |
| title_short | Designing asynchronous multiparty protocols with crash-stop failures |
| title_sort | designing asynchronous multiparty protocols with crash stop failures |
| work_keys_str_mv | AT barwella designingasynchronousmultipartyprotocolswithcrashstopfailures AT houp designingasynchronousmultipartyprotocolswithcrashstopfailures AT yoshidan designingasynchronousmultipartyprotocolswithcrashstopfailures AT zhouf designingasynchronousmultipartyprotocolswithcrashstopfailures |