Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.11197 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908469661007872 |
|---|---|
| author | Pears, Jonah Bocchi, Laura Murgia, Maurizio King, Andy |
| author_facet | Pears, Jonah Bocchi, Laura Murgia, Maurizio King, Andy |
| contents | Mixed-choice has long been barred from models of asynchronous communication since it compromises the decidability of key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling timeouts -- a core property of web and cloud services. To address this deficiency, we present (binary) Timeout Asynchronous Session Types (TOAST) as an extension to (binary) asynchronous timed session types, that permits mixed-choice. TOAST deploys timing constraints to regulate the use of mixed-choice so as to preserve communication safety. We provide a new behavioural semantics for TOAST which guarantees progress in the presence of mixed-choice. Building upon TOAST, we provide a calculus featuring process timers which is capable of modelling timeouts using a receive-after pattern, much like Erlang, and capture the correspondence with TOAST specifications via a type system for which we prove subject reduction. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_11197 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions Pears, Jonah Bocchi, Laura Murgia, Maurizio King, Andy Logic in Computer Science Mixed-choice has long been barred from models of asynchronous communication since it compromises the decidability of key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling timeouts -- a core property of web and cloud services. To address this deficiency, we present (binary) Timeout Asynchronous Session Types (TOAST) as an extension to (binary) asynchronous timed session types, that permits mixed-choice. TOAST deploys timing constraints to regulate the use of mixed-choice so as to preserve communication safety. We provide a new behavioural semantics for TOAST which guarantees progress in the presence of mixed-choice. Building upon TOAST, we provide a calculus featuring process timers which is capable of modelling timeouts using a receive-after pattern, much like Erlang, and capture the correspondence with TOAST specifications via a type system for which we prove subject reduction. |
| title | Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.11197 |