Timeout Asynchronous Session Types: Safe Asynchronous Mixed-Choice For Timed Interactions
Jonah Pears, Laura Bocchi, Maurizio Murgia, Andy King

TL;DR
This paper introduces TOAST, an extension of asynchronous session types that allows safe mixed-choice with timing constraints, enabling accurate modeling of timeouts in web and cloud services.
Contribution
It presents TOAST, a novel type system extension that permits mixed-choice in asynchronous timed session types while ensuring communication safety and progress.
Findings
TOAST guarantees progress with mixed-choice and timing constraints.
A calculus with process timers models timeouts similar to Erlang.
Type system proves subject reduction for timeout modeling.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Petri Nets in System Modeling
