Title: That's Enough: Asynchrony with Standard Choreography Primitives,
Abstract: Choreographies are widely used for the specification of concurrent and
distributed software architectures. Since asynchronous communications are
ubiquitous in real-world systems, previous works have proposed different
approaches for the formal modelling of asynchrony in choreographies. Such
approaches typically rely on ad-hoc syntactic terms or semantics for capturing
the concept of messages in transit, yielding different formalisms that have to
be studied separately.
In this work, we take a different approach, and show that such extensions are
not needed to reason about asynchronous communications in choreographies.
Rather, we demonstrate how a standard choreography calculus already has all the
needed expressive power to encode messages in transit (and thus asynchronous
communications) through the primitives of process spawning and name mobility.
The practical consequence of our results is that we can reason about real-world
systems within a choreography formalism that is simpler than those hitherto
proposed.