Constructive characterisations of the must-preorder for asynchrony

TL;DR

This paper extends the standard must-preorder characterization to asynchronous communication models with shared buffers, providing a constructive, mechanised proof approach in Coq for reasoning about program refinement.

Contribution

It demonstrates that existing must-preorder characterisations apply to asynchronous semantics with forwarder servers, using a constructive, calculus-independent approach mechanised in Coq.

Findings

Standard characterisations extend to asynchronous buffers with forwarders.

Mechanised proofs in Coq verify program relations under the must-preorder.

Brouwer's bar induction aids reasoning about liveness in program transformations.

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.