Constructive characterisations of the must-preorder for asynchrony

TL;DR

The paper addresses the practical difficulty of reasoning with the must-preorder for asynchronous, nondeterministic client–server systems by introducing a forwarding construction that augments servers to input any message and store it in a shared buffer. It shows that the standard synchronous characterisations of the must-preorder extend to asynchronous settings when using forwarders, and provides fully constructive, calculus-free accounts that are mechanised in Coq for Selinger's output-buffered agents with feedback. The main contributions include calculus-independent behavioural characterisations of the must-preorder in an asynchronous setting, a forwarding-based method that preserves existing preorders (MS, AS, and coinductive), and a constructive Coq formalisation (around 8000 lines) along with Brouwer bar induction to relate extensional and intensional definitions. These results pave the way for liveness-preserving program transformations and cross-language verification in asynchronous environments, with potential applications to refactoring and correctness proofs across languages implementing shared buffers and non-blocking outputs.

Abstract

De Nicola and Hennessy's must-preorder is a contextual refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to the universal quantification over clients, this definition does not yield a practical proof method for the must-preorder, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions. We show that the standard characterisations of the must-preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Coq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous pi-calculus. We show that the standard coinductive characterisation lets us prove in Coq that concrete programs are related by the must-preorder. Finally, our proofs show that Brouwer's bar induction principle is a useful technique to reason on liveness preserving program transformations.

Figures (3)

• Figure 1: The behaviours of a server $p_0$ and of a client $r_0$.
• Figure 2: First-order axioms for output-buffered agents with feedback as given by Selinger DBLP:conf/concur/Selinger97, extended with the Backward-output-determinacy axiom.
• Figure 3: Highlights of our Sts and Lts typeclasses.