Safe asynchronous mixed-choice for timed interactions

TL;DR

This paper introduces TOAST, an extension to asynchronous session types that allows mixed-choice with timing constraints, enabling safe modeling of timeouts in asynchronous communication.

Contribution

It presents TOAST, a novel type system extension that permits mixed-choice with timing constraints while ensuring communication safety and progress.

Findings

TOAST guarantees progress with mixed-choice.

A calculus with process timers models timeouts effectively.

Formal correspondence between TOAST and process calculus is established.

Abstract

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 $\mathtt{receive\text{-}after}$ pattern, much like Erlang, and informally illustrate the correspondence with TOAST specifications.