Safe asynchronous mixed-choice for timed interactions
share
Mixed-choice has long been barred from models of asynchronous communication since it compromises key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling timeouts – a key programming feature to handle failures. To address this deficiency, we present (binary) TimeOut Asynchronous Session Types (TOAST) as an extension to (binary) asynchronous timed session types to permit mixed-choice. TOAST deploy 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 𝚛𝚎𝚌𝚎𝚒𝚟𝚎-𝚊𝚏𝚝𝚎𝚛 pattern, much like Erlang, and informally illustrate the correspondence with TOAST specifications.
READ FULL TEXT