Safe and Asynchronous Mixed-Choice for Timed Interactions

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 and thus, greatly limits their applications to real-world systems. This thesis aims to address this deficiency by presenting Timeout Asynchronous Session Types (TOAST for short) which model timed, asynchronous communication in the binary setting. In this thesis we explore the relationship between timeouts and mixed-choice, and show how timing constraints can be deployed to ensure that a given mixed-choice is safe and does not compromise the decidability of properties of timed, asynchronous session types. TOAST extends prior works on asynchronous timed session types with the means to describe these safe mixed-choice. The formal theory of TOAST features new behavioural semantics for timed, asynchronous mixed-choice and a process calculus featuring timeout processes, process timers and time-sensitive conditional statements to facilitate the implementation of not just timeouts, but more broadly safe mixed-choice. The unique features of the TOAST process calculus are based upon the structures found in real programming languages, such as the receive-after expression in Erlang. Following the theory of TOAST, this thesis presents a proof-of-concept toolchain implemented in Erlang for generating program stubs from TOAST.