A uniform characterisation of the (a)synchronous must-preorder

TL;DR

This paper introduces a unified, axiomatic characterization of the must-preorder in message passing systems, simplifying and generalizing existing theories across synchronous and asynchronous settings.

Contribution

It provides the first uniform, calculus-independent characterization of the must-preorder applicable to multiple communication paradigms using label abstraction.

Findings

Unified proof of soundness and completeness for all settings

Constructive proofs mechanised in Rocq

Simplifies and generalizes existing theories

Abstract

In the setting of message passing software, De Nicola and Hennessy must-preorder defines when a program improves on another one. Since this preorder does not come equipped with a viable proof method, using it requires an alternative relation that characterises it. The literature presents at least four different definitions of such alternative preorders, depending on whether communication is synchronous or asynchronous and on whether there is value-passing or not. The existence of these different definitions complicates the overall theory, hinders the development of tools, and, upon the whole, suggests a lack of understanding of the properties necessary and sufficient to reason on the must-preorder. This paper presents the first alternative characterisation that works at least in all the four settings mentioned above. We achieve this result thanks to an axiomatic approach that is calculus independent, by highlighting the role of blocking and non-blocking actions, and by introducing the novel notion of label abstraction. Label abstractions capture the essence of safe substitutivity w.r.t. interactions, and they let us obtain a unique proof of soundness and a unique proof of completeness that work in all the mentioned settings. We believe this generalises and simplifies the overall theory, while letting us present the existing results in a uniform way. Our proofs are constructive and our result is entirely mechanised in Rocq.