Das Kapitel untersucht die MUST-Preorder, eine Verfeinerungsbeziehung, die entscheidend ist, um sicheres Code-Refactoring in nichtdeterministischen asynchronen Client-Server-Systemen zu gewährleisten. Es führt eine auf Asynchron zugeschnittene Version von Morris Preorder ein, die die Kündigung durch eine geeignete Lebendigkeit-Eigenschaft ersetzt. Der Text untersucht die Vor- und Nachteile der MUST-Vorordnung und betont ihren lebenserhaltenden Charakter und ihre Unabhängigkeit von bestimmten Kalkulationen. Sie vertieft sich in die Komplexität asynchroner Kommunikation, modelliert sie über Output-gepufferte Agenten mit Feedback und diskutiert die damit verbundenen technischen Schwierigkeiten. Das Kapitel präsentiert bahnbrechende Verhaltensbeschreibungen der MUST-Vorordnung, die ihre Solidität und Vollständigkeit in asynchronen Umgebungen demonstrieren. Außerdem wird eine koinduktive Vorordnung eingeführt, die praktische Beweismethoden erleichtert und ihre Verwendung beim Nachweis von Codehubverfeinerungen veranschaulicht. Der Text schließt mit einer Diskussion über verwandte Arbeiten, zukünftige Richtungen und die Mechanisierung der Theorie in Coq, die eine solide Grundlage für weitere Forschung und praktische Anwendungen bietet.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
De Nicola and Hennessy’s \(\textsc {must}\)-preorder is a liveness preserving 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, 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 \(\textsc {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 \(\textsc {must}\)-preorder.
Finally, our proofs show that Brouwer’s bar induction principle is a useful technique to reason on liveness preserving program transformations.
Hinweise
L. Stefanesco—Work done at MPI-SWS, Germany.
1 Introduction
Code refactoring is a routine task to develop or update software, and it requires methods to ensure that a program \(p\) can be safely replaced by a program \(q\). One way to address this issue is via refinement relations, i.e. preorders. For programming languages, the most well-known one is Morris extensional preorder [43, pag. 50], defined by letting \(p \le q\) if for all contexts C, whenever C[p] reduces to a normal form N, then C[q] also reduces to N.
Comparing servers This paper studies a version of Morris preorder for nondeterministic asynchronous client-server systems. In this setting it is natural to reformulate the preorder by replacing reduction to normal forms (i.e. termination) with a suitable liveness property. Let
denote a client-server system, that is a parallel composition in which the identities of the server \(p\) and the client \(r\) are distinguished, and whose computations have the form
where each step represents either an internal computation of one of the two components, or an interaction between them. Interactions correspond to handshakes, where two components ready to perform matching input/output actions advance together. We express liveness by saying that \(p\text { must pass } r\), denoted \( p \textsc {must} r\), if in every maximal computation of
there exists a state
such that \(\textsc {good}(r_i)\), where \(\textsc {good}\) is a decidable predicate indicating that the client has reached a successful state. Servers are then compared according to their capacity to satisfy clients, i.e. via contexts of the form
and the predicate \(\textsc {must}\). Morris preorder then becomes the \(\textsc {must}\)-preorder by De Nicola and Hennessy [25] :
Anzeige
Advantages The \(\textsc {must}\)-preorder is by definition liveness preserving, because \( p \textsc {must} r\) literally means that “in every execution something good must happen (on the client side)”. Results on
thus shed light on liveness-preserving program transformations.
The \(\textsc {must}\)-preorder is independent of any particular calculus, as its definition requires simply (1) a reduction semantics for the parallel composition
, and (2) a predicate \(\textsc {good}\) over programs. Hence
may relate servers written in different languages. For instance, servers written in OCaml may be compared to servers written in Java according to clients written in Python, because all these languages use the same basic protocols for communication.
Drawback The definition of the \(\textsc {must}\)-preorder is contextual: proving
requires analysing an infinite amount of clients, and so the definition of the preorder does not entail an effective proof method. A solution to this problem is to define an alternative (semantic) characterisation of the preorder
, i.e. a preorder \(\preccurlyeq _{ alt }\) that coincides with
and does away with the universal quantification over clients (i.e. contexts). In synchronous settings, i.e. when both input and output actions are blocking, such alternative characterisations have been thoroughly investigated, typically via a behavioural approach based on labelled transition systems.
Fig. 1.
The behaviours of a server \(p_0\) and of a client \(r_0\).
Labelled transition systems A program \(p\) is associated with a labelled transition system (LTS) representing its behaviour, which we denote by \(\textsc {lts}(p)\). Figure 1 presents two instances of LTSs, where transitions are labelled by input actions such as \(\texttt {str}\), output actions such as \(\overline{\texttt {str}}\), or the internal action \(\tau \) (not featured in Figure 1), while dotted nodes represent successful states, i.e. those satisfying the predicate \(\textsc {good}\). There, the server \(p_0\) is ready to input either a string or a float. It is the environment that, by offering an output of either type, will make \(p\) move to either \(p_1\) or \(p_2\). The client \(r_0\), on the other hand, is ready to either output a string, or input an integer. The input \(\texttt {int}\) makes the client move to the successful state \(r_2\), while the output \(\overline{\texttt {str}}\) makes the client move to the state \(r_1\), where it can still perform the input \(\texttt {int}\) to reach the successful state \(r_3\). In an asynchronous setting, output transitions enjoy a commutativity property on which we will return later. Programs \(p\) are usually associated with their behaviours \(\textsc {lts}(p)\) via inference rules that we omit in the main body of the paper, as they are standard.
Anzeige
Alternative preorders for synchrony Program behaviours, i.e. LTSs, are used to define the alternative preorders for
following one of two different approaches: \(\textsc {must}\)-sets or acceptance sets.
Both approaches were originally proposed for Milner’s Calculus of Communicating Systems (\(\textsc {CCS} \)) [42], where communication is synchronous. The first alternative preorder, which we denote by \(\mathrel {\preccurlyeq _{\textsf{MS}}}\), was put forth by De Nicola [25], and it compares server behaviours according to their \(\textsc {must}\)-sets, i.e. the sets of actions that they may perform after doing a given sequence of actions. The second alternative preorder, which we denote by \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), was put forth by Hennessy [32], and it compares the acceptance sets of servers, i.e. how servers can be moved out of their potentially deadlocked states, namely, states from which the servers cannot evolve autonomously. Both these preorders characterise
in the following sense:
(1)
(2)
While these alternative preorders do away with the universal quantification over clients, they are not practical to use directly, as they still universally quantify over (finite) traces of actions. A more practical approach [1] is to use a coinductively defined preorder \(\mathrel {\preccurlyeq _{\textsf{co}}}\) based on \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) [1, 10, 41]. This preorder has two advantages: first, its definition quantifies universally only on single actions; second, it allows the user to use standard coinductive methods, as found in the literature on bisimulation. In the case where the LTS is image-finite, such as for CCS and most process calculi, the coinductive preorder is sound and complete:
(3)
Asynchrony In distributed systems, communication is inherently asynchronous. For instance, the standard TCP transmission on the Internet is asynchronous. Actor languages like Elixir and Erlang implement asynchrony via mailboxes, and both Python and JavaScript offer developers the constructs async/wait, to return promises (of results) or wait for them. In this paper we model asynchrony via output-buffered agents with feedback, as introduced by Selinger [49]. These are LTSs obeying the axioms in Figure 2, where \(a\) denotes an input action, \(\overline{a}\) denotes an output action, \(\tau \) denotes the internal action, and \(\alpha \) ranges over all these actions. For instance, the Output-commutativity axiom states that an output \(\overline{a}\) can always be postponed: if \(\overline{a}\) is followed by any action \(\alpha \), it can commute with it. In other words, outputs are non-blocking, as illustrated by the LTS for \(r_0\) in Figure 1. We defer a more detailed discussion of these axioms to Section 2.
Fig. 2.
First-order axioms for output-buffered agents with feedback as given by Selinger [49], extended with the Backward-output-determinacy axiom.
Technical difficulties The practical importance of asynchrony motivates a specific study of
. Efforts in this direction have been made, all of which focussed on process calculi [15, 21, 34, 52], while the axioms in Figure 2 apply to LTSs. Note that these axioms impose conditions only over outputs, and this asymmetric treatment of inputs and outputs substantially complicates the proofs of completeness and soundness of the alternative characterisations of
. To underline the subtleties due to asynchrony, we note that the completeness result for asynchronous CCS given by Castellani and Hennessy in [21], and subsequently extended to the \(\pi \)-calculus by Hennessy [34], is false (see [8, Appendix I]).
Contributions and paper structure.
Our main contributions may be summarised as follows (where for each of them, we indicate where it is presented in the paper):
The first behavioural characterisations of the \(\textsc {must}\)-preorder (Theorem 1, Theorem 3) that are calculus independent, in that both our definitions and our proofs work directly on LTSs. Contrary to all the previous works on the topic, we show that the standard alternative preorders characterise the \(\textsc {must}\)-preorder also in Selinger asynchronous setting. To this end, it suffices to enrich the server semantics with forwarding, i.e. ensure that servers are ready to input any message, as long as they store it back in a global shared buffer. This idea, although we use it here in a slightly different form, was pioneered by Honda et al. [38]. In this paper we propose a construction that works on any LTS (Lemma 2) and we show the following counterparts of Equations (1), (2), and (3) where \(\textsc {Fdb}\) denotes the LTSs of output-buffered agents with feedback, and \(\textsc {FW}\) is the function that enhances them with forwarding:
Quite surprisingly, the alternative preorders \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), \(\mathrel {\preccurlyeq _{\textsf{MS}}}\) and \(\mathrel {\preccurlyeq _{\textsf{co}}}\) need not be changed. We present these results in Sections 3 and 4. We use the coinductive preorder \(\mathrel {\preccurlyeq _{\textsf{co}}}\) to prove the correctness of a form of code hoisting (6).
The first characterisations of the \(\textsc {must}\)-preorder that fully exploit asynchrony, i.e. disregard irrelevant (that is, non-causal) orders of visible actions in traces ([8, Corollary 4]).
The first constructive account of the \(\textsc {must}\)-preorder. We show that if the \(\textsc {must}\) and termination predicates are defined intensionally (in the sense of Brede and Herbelin [17]), then
can be characterised constructively. The original definitions of \(\textsc {must}\) and termination given by De Nicola [25], though, are extensional. We show how to use Brouwer bar induction principle to prove that the two approaches are logically equivalent (Corollary 2). Since Rahli et al. [46] have shown bar induction to be compatible with constructive type theory, we argue that our development is entirely constructive.
The first mechanisation of the theory of \(\textsc {must}\)-preorder in a fully nondeterministic setting, which consists of around 8000 lines of Coq. In [8, Appendix J] we gather the Coq versions of all the definitions and the results presented in the main body of the paper.
In Sections 5 and 6, we discuss the impact of the above contributions, as well as related and future work. In Section 2, we recall the necessary background definitions and illustrate them with a few examples.
Fig. 3.
Highlights of our Sts and Lts typeclasses.
2 Preliminaries
We model individual programs such as servers \(p\) and clients \(r\) as LTSs obeying Selinger axioms, while client-server systems
are modelled as state transition systems with a reduction semantics. We now formally define this two-level semantics.
Labelled transition systems A labelled transition system (LTS) is a triple \(\mathcal {L}= \langle A, L , \longrightarrow \rangle \) where \(A\) is the set of states, L is the set of labels and \({\longrightarrow } \subseteq A\times L \times A\) is the transition relation. When modelling programs as LTSs, we use transition labels to represent program actions. The set of labels in Selinger LTSs has the same structure as the set of actions in Milner’s calculus CCS: one assumes a set of names \(\mathcal {N} \), denoting input actions and ranged over by \(a, b, c\), a complementary set of conames \(\overline{\mathcal {N}}\), denoting output actions and ranged over by \(\overline{a}, \overline{b}, \overline{c}\), and an invisible action \(\tau \), representing internal computation. The set of all actions, ranged over by \(\alpha , \beta , \gamma \), is given by \(\textsf{Act}_\tau \;\;\mathrel {{\mathop {=}\limits ^{\textsf{def}}}}\;\; \mathcal {N} \uplus \overline{\mathcal {N}} \uplus \{ \tau \} \). We use \(\mu , \mu '\) to range over the set of visible actions \(\mathcal {N} \uplus \overline{\mathcal {N}}\), and we extend the complementation function \(\overline{\cdot }\) to this set by letting \({\overline{\overline{a}}} \mathrel {{\mathop {=}\limits ^{\textsf{def}}}}a\). In the following, we will always assume \(L = \textsf{Act}_\tau \). Once the LTS is fixed, we write \(p\longrightarrow p'\) to mean that \((p,\alpha ,p')~\in ~{\longrightarrow }\) and \( p\longrightarrow \) to mean \(\exists p'. \;p\longrightarrow p'\).
We use \(\mathcal {L}\) to range over LTSs. To reason simultaneously on different LTSs, we will use the symbols \(\mathcal {L}_A\) and \(\mathcal {L}_B\) to denote respectively the LTSs \(\langle A, L, \longrightarrow _A \rangle \) and \(\langle B, L, \longrightarrow _B \rangle \).
In our mechanisation LTSs are borne out by the typeclass Lts in Figure 3. The states of the LTS have type \(A\), labels have type L, and lts_step is the characteristic function of the transition relation, which we assume to be decidable. We let \(O(p) = \{ \overline{a} \in \overline{\mathcal {N}} \ |\ p \longrightarrow \} \) and \(I(p) = \{ a\in \mathcal {N} \ |\ p \longrightarrow \} \) be respectively the set of outputs and the set of inputs of state \(p\). We assume that the set \(O(p)\) is finite for any \(p\). In our mechanisation, the set \(O(p)\) is rendered by the function lts_outputs, and we shall also use a function lts_performs that lets us decide whether a state can perform a transition labelled by a given action.
Fig. 4.
The STS of server-client systems.
Client-server systems A client-server system (or system, for short) is a pair
in which \(p\) is deemed to be the server of client \(r\). In general, every system
is the root of a state transition system (STS), \(\langle S, \longrightarrow \rangle \), where \(S\) is the set of states and \(\longrightarrow \) is the reduction relation. For the sake of simplicity1 we derive the reduction relation from the LTS semantics of servers and clients as specified by the rules in Figure 4. In our mechanisation (Figure 3), sts_step is the characteristic function of the reduction relation \(\longrightarrow \), and sts_stable is the function that states whether a state can reduce or not. Both functions are assumed decidable.
Definition 1
(Computation). Given an STS \(\langle S, \longrightarrow \rangle \) and a state \(s_0 \in S\), a computation of \(s_0\) is a finite or infinite reduction sequence starting from \(s_0\). A computation is maximal if either it cannot be extended or it is infinite.
To formally define the \(\textsc {must}\)-preorder, we assume a decidable predicate \(\textsc {good}\) over clients. A computation
is successful if there exists a state
such that \(\textsc {good}(r_i)\). We assume the predicate \(\textsc {good}\) to be invariant under outputs:
All the previous works on asynchronous calculi implicitly make this assumption, since they rely on ad-hoc actions such as \(\omega \) or \(\checkmark \) to signal success and they treat them as outputs. In [8, Appendix H] we show that this assumption holds for the language ACCS (the asynchronous variant of CCS) extended with the process \(\mathop {\textsf {1}}\), which is used as a syntactic means to denote GOOD states. Moreover, when considering an equivalence on programs \(\simeq \) that is compatible with transitions, in the sense of Figure 5, we assume the predicate \(\textsc {good}\) to be preserved also by this equivalence. These assumptions are met by the frameworks in [15, 21, 34].
Definition 2
(Client satisfaction). We write \(p \textsc {must}r \) if every maximal computation of
is successful.
Definition 3
(\(\textsc {must}\)-preorder ). We let
whenever for every client r we have that \(p \textsc {must}r\) implies \(q \textsc {must}r\).
Example 1
Consider the system
, where \(p_0\) and \(r_0\) are the server and client given in Figure 1. The unique maximal computation of this system is
. This computation is successful since it leads the client to the \(\textsc {good}\) state \(r_3\). Hence, client \(r_0\) is satisfied by server \(p_0\). Since Output-commutativity implies an absence of causality between the output \(\overline{\texttt {str}}\) and the input \(\texttt {int}\) in the client, it is the order between the input \(\texttt {str}\) and the output \(\overline{\texttt {int}}\) in the server that guides the order of client-server interactions. \(\square \)
A closer look at Selinger axioms Let us now discuss the axioms in Figure 2. The Output-commutativity axiom expresses the non-blocking behaviour of outputs: an output cannot be a cause of any subsequent transition, since it can also be executed after it, leading to the same resulting state. Hence, outputs are concurrent with any subsequent transition. The Feedback axiom says that an output followed by a complementary input can also synchronise with it to produce a \(\tau \)-transition. These first two axioms specify properties of outputs that are followed by another transition. Instead, the following three axioms, Output-confluence, Output-determinacy and Output-tau, specify properties of outputs that are co-initial with another transition2. The Output-determinacy and Output-tau axioms apply to the case where the co-initial transition is an identical output or a \(\tau \)-transition respectively, while the Output-confluence axiom applies to the other cases. When taken in conjunction, these three axioms state that outputs cannot be in conflict with any co-initial transition, except when this is a \(\tau \)-transition: in this case, the Output-tau axiom allows for a confluent nondeterminism between the \(\tau \)-transition on one side and the output followed by the complementary input on the other side.
We now explain the novel Backward-output-determinacy axiom. It is the dual of Output-determinacy, as it states that also backward transitions with identical outputs lead to the same state. The intuition is that if two programs arrive at the same state by removing the same message from the mailbox, then they must coincide. This axiom need not be assumed in [49] because it can be derived from Selinger axioms when modelling a calculus like ACCS equipped with a parallel composition operator \(\parallel \) (see [8, Lemma 53]). We use the Backward-output-determinacy axiom only to prove a technical property of clients (see [8, Lemma 25]) that is used to prove our completeness result.
Calculi A number of asynchronous calculi [16, 21, 36, 38, 44, 48] have an LTS that enjoys the axioms in Figure 2, at least up to some structural equivalence \(\equiv \). The reason is that these calculi syntactically enforce outputs to have no continuation, i.e. outputs can only be composed in parallel with other processes3. For example, Selinger [49] shows that the axioms of Figure 2 hold for the LTS of the calculus ACCS (the asynchronous variant of CCS4) modulo bisimulation, and in (see [8, Lemma 55]) we prove that they hold also for the LTS of ACCS modulo \(\equiv \):
Lemma 1
We have that \(\langle {\texttt {ACCS}}_{\equiv }, L, {\longrightarrow }_{\equiv } \rangle \in \textsc {Fdb}\).
To streamline reasoning modulo some (structural) equivalence we introduce the typeclass LtsEq, whose instances are LTSs equipped with an equivalence \(\simeq \) that satisfies the property in Figure 5. Defining output-buffered agents with feedback using LtsEq does not entail any loss of generality, because the equivalence \(\simeq \) can be instantiated using the identity over the states \(A\). Further details can be found in [8, Appendix H.1].
When convenient we denote LTSs using the following minimal syntax for ACCS:
(5)
as well as its standard LTS5 whose properties we discuss in detail in [8, Appendix H]. This is exactly the syntax used in [15, 49], without the operators of restriction and relabelling. Here the syntactic category g defines guards, i.e. the terms that may be used as arguments for the \(+\) operator. As in most process calculi, 0 denotes the terminated process that cannot do any action. Note that, apart from \(\mathop {\textsf {0}}\), only input-prefixed and \(\tau \)-prefixed terms are allowed as guards, and that the output prefix operator is replaced by atoms\(\overline{a}\). In fact, this syntax is completely justified by Selinger axioms, which, as we argued above, specify that outputs cannot cause any other action, nor be in conflict with it.
Fig. 5.
Axiom stating that equivalence \(\simeq \) is compatible with a transition relation.
Definition 4
(Transition sequence). Given an LTS \(\langle A, L , \longrightarrow \rangle \) and a state \(p_0 \in A\), a transition sequence of \(p_0\) is a finite or infinite sequence of the form \(p_0 \alpha _1 p_1 \alpha _2 p_2 \cdots \) with \(p_i \in A\) and \(\alpha _i \in L\), and such that, for every \(n \ge 1\) such that \(p_n\) is in the sequence we have \(p_{n-1} \xrightarrow {\alpha _n} p_{n}\).
If a transition sequence is made only of \(\tau \)-transitions, it is called a computation by abuse of notation, the idea being that usually \(\tau \)-steps are related to reduction steps via the Harmony lemma (see footnote on page 7).
We give now an example that illustrates the use of the testing machinery in our asynchronous setting. This is also a counter-example to the completeness of the alternative preorder proposed in [21], as discussed in detail in [8, Appendix I].
Example 2
Let \(\varOmega = \textsf{rec} x. \tau . x\) and \(\text {{Pierre}} = b.(\tau .\varOmega \mathrel {+}c.\overline{d}) \). The LTS of Pierre is as follows:
Pierre models a citizen confronted with an unpopular pension reform. To begin with, Pierre can only do the input \(b\), which models his getting aware of the brute-force imposition of the reform by the government. After performing the input, Pierre reaches the state \( \tau .\varOmega \mathrel {+}c.\overline{d} \), where he behaves in a nondeterministic manner. He can internally choose not to trust the government for any positive change, in which case he will diverge, refusing any further interaction. But this need not happen: in case the government offers the action \(\overline{c}\), which models a positive change in political decision, Pierre can decide to accept this change, and then he expresses his agreement with the output \(\overline{d}\), which stands for “done”. \(\square \)
Example 3
We prove now the inequality
by leveraging the possibility of divergence of \(\text {{Pierre}} \) after the input \(b\). Fix an \(r\) such that \( \text {{Pierre}} \textsc {must}r \). Note that, since 0 is the terminated process, the condition for the server 0 to satisfy r is that r reaches by itself a successful state in each of its maximal computations. We distinguish two cases, according to whether \(r\longrightarrow \) or
.
i) Let \(r\longrightarrow r'\) for some \(r'\). Consider the maximal computation
in which \(\text {{Pierre}} \) diverges and \(r\) does not move after the first output. Since \(\text {{Pierre}} \textsc {must}r\), either \(\textsc {good}(r)\) or \(\textsc {good}(r')\). In case \(\textsc {good}(r')\), by Equation (4) we get also \(\textsc {good}(r)\). Hence \( \mathop {\textsf {0}} \textsc {must}r\).
ii) Let
. Suppose \(r= r_0 \longrightarrow r_1 \longrightarrow r_2 \longrightarrow \ldots \) is a maximal computation of \(r\). Then
has a maximal computation
. As \(\text {{Pierre}} \textsc {must}r\), there must exist an \(i \in \mathbb {N} \) such that \(\textsc {good}(r_i)\). Hence \( \mathop {\textsf {0}} \textsc {must}r\). \(\square \)
The argument in Example 3 can directly use Definition 3 because it is very simple to reason on the process \(\mathop {\textsf {0}}\). The issues brought about by the contextuality of Definition 3, though, hinder showing general properties of
. Consider the following form of code hoisting:
(6)
If we see the above nondeterministic sums as representing the two branches of a conditional statement, this refinement corresponds to hoisting the shared action \(\overline{a}\) before the conditional statement, a common compiler optimisation. Proving Equation (6) via the contextual definition of
is cumbersome. This motivates the study of alternative characterisations for
, and in the rest of the paper we present several preorders that fit the purpose, in particular the coinductive preorder \(\mathrel {\preccurlyeq _{\textsf{co}}}\), which we will use to establish Equation (6) in Section 3.3.
We conclude this section by recalling auxiliary and rather standard notions: given an LTS \(\langle A, L, \longrightarrow \rangle \), the weak transition relation \(p\mathrel {\overset{ s}{\Longrightarrow }} p'\), where \( s\in \textsf{Act}^\star \), is defined via the rules
\(p\mathrel {\overset{ s}{\Longrightarrow }} q\) if \(p\longrightarrow p'\) and \(p'\mathrel {\overset{ s}{\Longrightarrow }} q\)
[wt-mu]
\(p\mathrel {\overset{\mu .s}{\Longrightarrow }} q\) if \(p\longrightarrow p'\) and \(p'\mathrel {\overset{s}{\Longrightarrow }} q\)
We write \( p\mathrel {\overset{ s}{\Longrightarrow }} \) to mean \(\exists p'. \;p\mathrel {\overset{ s}{\Longrightarrow }} p'\).
We write \(p\downarrow \) and say that \(p\)converges if every computation of \(p\) is finite, and we lift the convergence predicate to finite traces by letting the relation \({\mathrel {\Downarrow }} \subseteq A\times \textsf{Act}^\star \) be the least one that satisfies the following rules
[cnv-epsilon]
\(p\mathrel {\Downarrow }\varepsilon \) if \(p\downarrow \),
[cnv-mu]
\( p\mathrel {\Downarrow }\mu .s\) if \(p \downarrow \) and \(p\mathrel {\overset{\mu }{\Longrightarrow }} p'\implies p'\mathrel {\Downarrow }s\).
To understand the next section, one should keep in mind that all the predicates defined above have an implicit parameter: the LTS of programs. By changing this parameter, we may change the meaning of the predicates. For instance, letting \(\varOmega \) be the ACCS process \(\textsf{rec} x. \tau . x\), in the standard LTS \(\langle \texttt {ACCS}, \textsf{Act}_\tau , \longrightarrow \rangle \) we have \( \varOmega \longrightarrow \varOmega \) and \(\lnot (\varOmega \downarrow )\), while in the LTS \(\langle \texttt {ACCS}, \textsf{Act}_\tau , \emptyset \rangle \) we have
and thus \(\varOmega \downarrow \). In other words, the same predicates can be applied to different LTSs, and since the alternative characterisations of
are defined using such predicates, they can relate different LTSs.
3 Preorders based on acceptance sets
We first recall the definition of the standard alternative preorder \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), and show how to use it to characterise
in our asynchronous setting. We also present a new characterisation that disregards the order of non-causally related actions. We then explain the tools we use to prove these characterisations, and in particular their soundness. This section ends with the coinductive version \(\mathrel {\preccurlyeq _{\textsf{co}}}\) of \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), which we use to prove the hoisting refinement (6).
3.1 Trace-based characterisations
The ready set of a program \(p\) is defined as \(R( p) = I( p) \cup O( p)\), and it contains all the visible actions that \(p\) can immediately perform. If a program \(p\) is stable, i.e. it cannot perform any \(\tau \)-transition, we say that it is a potential deadlock. In general, the ready set of a potential deadlock \(p\) shows how to make \(p\) move to a different state, possibly one that can perform further computation: if \(R( p) = \emptyset \) then there is no way to make \(p\) move on, while if \(R( p)\) contains some action, then \(p\) is a state waiting for the environment to interact with it. Indeed, potential deadlocks are called waiting states in [38]. In particular, in an asynchronous setting the outputs of a potential deadlock \(p\) show how it can unlock the inputs of a client, which in turn may lead the client to a novel state that can make \(p\) move, possibly to a state that can perform further computation. A standard manner to capture all the ways out of the potential deadlocks that a program \(p\) encounters after executing a trace \(s\) is its acceptance set:
.
In our presentation we indicate explicitly the third parameter of \(\mathcal {A}\), i.e. the transition relation of the LTS at hand, because when necessary we will manipulate this parameter. For any two LTSs \(\mathcal {L}_A, \mathcal {L}_B\) and servers \( p\in A, q\in B\), we write \(\mathcal {A}( p, s,\longrightarrow _A) \ll \mathcal {A}( q, s, \longrightarrow _B)\) if for every \(R \in \mathcal {A}( q, s, \longrightarrow _B)\) there exists \(\widehat{R} \in \mathcal {A}( p, s,\longrightarrow _A)\) such that \(\widehat{R} \subseteq R\). We can now recall the definition of the behavioural preorder à la Hennessy, \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), which is based on acceptance sets [32].
Definition 5
We write
\( p\mathrel {\preccurlyeq _{\textsf{cnv}}}q\) whenever \(\forall s\in \textsf{Act}^\star . \;p \Downarrow _{A} s \implies q \Downarrow _{B} s \),
In the synchronous setting, the behavioural preorder \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) is closely related to the denotational semantics based on Acceptance Trees proposed by Hennessy in [31, 32]. There the predicates need not be annotated with the LTS that they are used on, because those works treat a unique LTS. Castellani and Hennessy [21] show in their Example 4 that the condition on acceptance sets, i.e.\(\mathrel {\preccurlyeq _{\textsf{acc}}}\), is too demanding in an asynchronous setting.
Letting \(p= a.\mathop {\textsf {0}}\) and \(q= \mathop {\textsf {0}}\), they show that
but
, because \(\mathcal {A}( p, \epsilon ) =\{ \{ a \} \}\) and \(\mathcal {A}( q, \epsilon ) =\{ \emptyset \}\), and corresponding to the ready set \(\emptyset \in \mathcal {A}( q, \epsilon )\) there is no ready set \(\widehat{R} \in \mathcal {A}( p, s)\) such that \(\widehat{R} \subseteq \emptyset \). Intuitively this is the case because acceptance sets treat inputs and outputs similarly, while in an asynchronous setting only outputs can be tested.
Nevertheless \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) characterises
, if servers are enhanced as with forwarding. We now introduce this concept.
Forwarders We say that an LTS \(\mathcal {L}\) is of output-buffered agents with forwarding, for short is Fwd, if it satisfies all the axioms in Figure 2 except Feedback, and also the two following axioms:
(7)
The Input-Boomerang axiom states a kind of input-enabledness property, which is however more specific as it stipulates that the target state of the input should loop back to the source state via a complementary output. This is the essence of the behaviour of a forwarder, whose role is simply to pass on a message and then get back to its original state. The Fwd-Feedback axiom is a weak form of Selinger’s Feedback axiom, which is better understood in conjunction with the Input-Boomerang axiom: if the transition sequence \(p\longrightarrow p'\longrightarrow q\) in the Fwd-Feedback axiom is taken to be the transition sequence \(p'\longrightarrow p\longrightarrow p'\) in the Input-Boomerang axiom, then we see that it must be \(q=p\) in the Fwd-Feedback axiom. Moreover, no \(\tau \) action is issued when moving from p to q, since no synchronisation occurs in this case: the message is just passed on.
To prove that \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) is sound and complete with respect to
:
1.
we define a function \(\textsc {FW}: \textsc {Fdb}\longrightarrow \textsc {Fwd}\) that lifts any LTS \(\mathcal {L}\in \textsc {Fdb}\) into a suitable LTS \(\textsc {FW}(\mathcal {L})\in \textsc {Fwd}\), and
2.
we check the predicates \(\mathrel {\Downarrow }\) and \(\mathcal {A}(-,-,-)\) over the LTS \(\textsc {FW}(\mathcal {L})\).
Let \( MO \) denote the set of all finite multisets of output actions, for instance we have \(\varnothing , \{\!| \overline{ a } |\!\}, \{\!| \overline{ a }, \overline{ a } |\!\}, \{\!| \overline{ a }, \overline{ b }, \overline{ a }, \overline{ b }|\!\} \in MO \). We let \(M, N, \ldots \) range over \( MO \). The symbol M stands for mailbox. We denote with \(\uplus \) the multiset union.
Definition 6
Let
for every \(\mathcal {L}= \langle A, L, \longrightarrow \rangle \), where the states in \(\textsc {FW}(\mathcal {L})\) are pairs denoted \(p \triangleright M\), such that \(p \in A\) and \(M \in MO \), and the transition relation
is defined via the rules in Figure 6.
Fig. 6.
Lifting of an LTS to an LTS with forwarding.
Let us briefly comment on Definition 6 and the rules in Figure 6. The pair \(p\triangleright M\) is a kind of asymmetric parallel composition between a process \(p\) and a mailbox M. Rule \({\small {\textsc {[L-Proc]}}} \) says that the process can evolve independently of the mailbox. Rule \({\small {\textsc {[L-Comm]}}} \) says that an input in the process can synchronise with a complementary output in the mailbox. Rules \({\small {\textsc {[L-Minp]}}} \) and \({\small {\textsc {[L-Mout]}}} \) express the essence of the forwarding behaviour: the pair \(p\triangleright M\) may input any message from the environment and store it into the mailbox M (Rule \({\small {\textsc {[L-Minp]}}} \)); dually, the pair \(p\triangleright M\) may output any message in the mailbox M towards the environment (Rule \({\small {\textsc {[L-Mout]}}} \)). Note that in both cases, the interaction occurs between the mailbox M and the environment, without any participation of the process \(p\).
Example 4
If a calculus is fixed, then the function \(\textsc {FW}\) may have a simpler definition. For instance Castellani and Hennessy [21] define it in their calculus TACCS by letting \(\mathrel {\overset{\alpha }{\longrightarrow }_\textsf{fw}}\) be the least relation over TACCS such that (1) for every \(\alpha \in \textsf{Act}_\tau . \;\longrightarrow \subseteq \mathrel {\overset{\alpha }{\longrightarrow }_\textsf{fw}}\), and (2) for every \(\text{\AA }\in \mathcal {N} . \;p \mathrel {\overset{a}{\longrightarrow }_\textsf{fw}} p \mathrel {\parallel }\overline{a}\). \(\square \)
The transition relation
is reminiscent of the one introduced in Definition 8 by Honda and Tokoro in [38]. The construction given in our Definition 6, though, does not yield the LTS of Honda and Tokoro, as
adds the forwarding capabilities to the states only at the top-level, instead of descending structurally into terms. As a consequence, in the LTS of [38] \(a.\mathop {\textsf {0}}+ \mathop {\textsf {0}}\longrightarrow \overline{ b}\), while
.
Example 5
As the set \(\mathcal {N} \) is countable, every process \(p\) that belongs to the LTS
is infinitely-branching: for every mailbox M we have \(p\triangleright M \mathrel {\overset{a_i}{\longrightarrow }_\textsf{fw}} p\triangleright (\{\!|\overline{a_i}|\!\} \uplus M)\) for every \(a_i \in \mathcal {N} \). This is illustrated by the following picture, where for simplicity we omit the subscript \(\textsf{fw}\) under the arrows.
\(\square \)
The intuition behind Definition 6 is that, when a client interacts with a server asynchronously, the client can send any message it likes, regardless of the inputs that the server can actually perform. In fact, asynchronous clients behave as if the server was saturated with forwarders, namely processes of the form \(a. \overline{a}\), for any \(a\in \mathcal {N} \).
The function \(\textsc {FW}\) enjoys two crucial properties: it lifts any LTS of output-buffered agents with feedback to an LTS with forwarding, and the lifting preserves the \(\textsc {must}\) predicate. We can thus reason on
using LTSs in \(\textsc {Fwd}\).
Lemma 2
For every LTS \(\mathcal {L}\in \textsc {Fdb}\), \(\textsc {FW}(\mathcal {L}) \in \textsc {Fwd}\).
For every \(\mathcal {L}_A, \mathcal {L}_B, \mathcal {L}_C \in \textsc {Fdb}, p\in A, q\in B, r\in C\),
1.
\( p \textsc {must}r\) if and only if \(\textsc {FW}(p) \textsc {must}r\),
2.
if and only if
.
We now simplify the definition of acceptance sets to reason on LTSs that are in Fwd: for any LTS \(\mathcal {L}= \langle A, \textsf{Act}, \longrightarrow \rangle \in \textsc {Fwd}\) and program \( p\in A\) we let
. This definition suffices to characterise
because in each LTS that is Fwd every state performs every input, thus comparing inputs has no impact on the preorder \(\mathrel {\preccurlyeq _{\textsf{acc}}}\) of Definition 5. More formally, for every \(\mathcal {L}_A, \mathcal {L}_B\in \textsc {Fwd}\) and every \(p\in A\) and \(q\in B\), we let
Let \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fwd}\). For every \(p\in A, q\in B, p\mathrel {\preccurlyeq _{\textsf{acc}}}q\) if and only if \(p\preccurlyeq ^{\textsf{fw}}_{\textsf {acc}}q\).
Proof
The only if implication is trivial, so we discuss the if one. Suppose that \( p\preccurlyeq ^{\textsf{fw}}_{\textsf {acc}}q\) and that for some \(s\) we have that \(R \in \mathcal {A}(q,s,\longrightarrow _B)\). Let X be the possibly empty subset of R that contains only output actions. Since \(\mathcal {L}_B\) is Fwd we know by definition that \(R = {X} \cup {\mathcal {N}}\). By definition \(X \in \mathcal {A}_{\textsf{fw}}(q,s,\longrightarrow _B)\), and thus by hypothesis there exists a set of output actions \(Y \in \mathcal {A}_{\textsf{fw}}(p,s,\longrightarrow _A)\) such that \(Y \subseteq X\). It follows that the set \({{Y} \cup {\mathcal {N}}} \in \mathcal {A}(p,s,\longrightarrow _A)\), and trivially \(Y \cup \mathcal {N} \subseteq {X} \cup {\mathcal {N}} = R\). \(\square \)
In view of the second point of Lemma 3, to prove completeness it suffices to show that \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) includes
over LTSs with forwarding. This is indeed true:
Lemma 5
For every \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fwd}\) and \(p\in A, q\in B\), if
then we have \({ p} \mathrel {\preccurlyeq _{\textsf{AS}}}{ q}\).
By a slight abuse of notation, given an LTS \(\mathcal {L}= \langle A, L, \longrightarrow \rangle \) and a state \(p\in A\), we denote with \(\textsc {FW}( p)\) the LTS rooted at \(p\triangleright \varnothing \) in \(\textsc {FW}(\mathcal {L})\).
Theorem 1
For every \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fdb}\) and \(p\in A, q\in B,\)
This theorem is the linchpin of this paper, as all other results presented in this paper are corollaries. To begin with, instantiating this theorem to a calculus which can be given an LTS that satisfies the axioms for output-buffered agents with feedback such as ACCS (Lemma 1), the core join-calculus [29] or KLAIM [24], we get a characterisation of the \(\textsc {must}\)-preorder essentially for free. In our Coq development, we instantiate it with \(\texttt {ACCS} \):
Corollary 1
For every
iff \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{AS}}}\textsc {FW}(q).\)
Another application of Theorem 1 is a novel behavioural characterisation of the \(\textsc {must}\)-preorder, which fully exploits asynchrony, i.e. disregards irrelevant non-causal orders of visible actions in traces. For space reasons, we defer the discussion of this result to [8, Appendix G].
So far, we have seen the more direct applications of Theorem 1. Before we explain two other applications, namely the coinductive characterisation of the \(\textsc {must}\)-preorder and the relation of
with the failure refinement, we outline the proof of Theorem 1, and, in particular, the technical tools we used.
The full proof of Theorem 1, which is given in [8], as well as in the Coq development, comprises two parts: [8, Appendix D] deals with completeness, where the main aim is to show Lemma 5, and [8, Appendix E] deals with soundness. Here we outline the main tools we use to prove the soundness of the \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) preorder: Bar-induction, which allows us to relate the standard definition of \(\textsc {must}\) with an inductive one that is more practical to use, especially in a constructive setting, and the LTS of sets, which is derived from the LTS of the processes.
Bar induction: from extensional to intensional definitions We present the inductive characterisations of \(\downarrow \) and \(\textsc {must}\) in any state transition system (STS) \(\langle S, \rightarrow \rangle \) that is countably branching. In practice, this condition is satisfied by most concrete LTS of programming languages, which usually contain countably many terms; this is the case for ACCS and for the asynchronous \(\pi \)-calculus.
Following the terminology of [17] we introduce extensional and intensional predicates associated to any decidable predicate \(Q: S \rightarrow \mathbb {B}\) over an STS \(\langle S, \rightarrow \rangle \), where \(\mathbb {B}\) denotes the set of booleans.
Definition 7
The extensional predicate\(\textsf{ext}_Q(s)\) is defined, for \(s \in S\), as
$$ \forall \eta \text { maximal execution of }S . \;\eta _0 = s \implies \exists n \in \mathbb {N} ,\; Q(\eta _n) $$
The intensional predicate\(\textsf{int}_Q\) is the inductive predicate (least fixpoint) defined by the following rules:
For instance, by letting
we have by definition that
that is the standard definitions of \(\downarrow \) and \(\textsc {must}\) are extensional. Our aim now is to prove that they coincide with their intensional counterparts. The reader not familiar with this terminology may find in [8, Appendix B] an informal and hopefully intuitive explanation. Since we will use the intensional predicates in the rest of the paper a little syntactic sugar is in order, let
The proofs of soundness, i.e. that the inductively defined predicates imply the extensional ones, are by rule induction:
Lemma 6
For \(p\in S\),
(a)
\(p\downarrow _i\) implies \(p\downarrow \),
(b)
for every \(r. \;p \textsc {must}_ir\) implies \( p \textsc {must}r\).
The proofs of completeness are more delicate. To the best of our knowledge, the ones about CCS [6, 22] proceed by induction on the greatest number of steps necessary to arrive at termination or at a successful state. Since the STS of \(\langle \textsc {CCS}, \longrightarrow \rangle \) is finite branching, Kőnig’s lemma guarantees that such a bound exists. This technique does not work on infinite-branching STSs, for example the one of CCS with infinite sums [9]. If we reason in classical logic, we can prove completeness without Kőnig’s lemma and also over infinite-branching STSs via a proof ad absurdum: suppose \(p \downarrow \). If \(\lnot (p \downarrow _i)\) no finite derivation tree exists to prove \(p \downarrow _i\), and then we construct an infinite sequence of \(\tau \) moves starting with p, thus \(\lnot (p \downarrow )\). Since we strive to be constructive we replace reasoning ad absurdum with a constructive axiom: (decidable) bar induction. In the rest of this section we discuss this axiom, and adapt it to our client-server setting. This requires a little terminology.
Bar induction The axiom we want to use is traditionally stated using natural numbers. We use the standard notations \(\mathbb {N} ^\star \) for finite sequences of natural numbers, \(\mathbb {N} ^\omega \) for infinite sequences, and \(\mathbb {N} ^\infty = \mathbb {N} ^\star \cup \mathbb {N} ^\omega \) for finite or infinite sequences. Remark that, in constructive logics, given \(u \in \mathbb {N} ^\infty \), we cannot do a case analysis on whether u is finite or infinite. The set \(\mathbb {N} ^\infty \) equipped with the prefix order can be seen as a tree, denoted \(T_{\mathbb {N} }\), in the sense of set theory: a tree is an ordered set \((A, \le )\) such that, for each \(a \in A\), the set \(\{ b \mid b < a \}\) is well-ordered by <. A path in a tree A is a maximal element in A. In the tree \(\mathbb {N} ^\infty \), each node has \(\omega \) children, and the paths are exactly the infinite sequences \(\mathbb {N} ^\omega \).
A predicate \(P \subseteq \mathbb {N} ^\star \) over finite words is a bar if every infinite sequence of natural numbers has a finite prefix in P. Note that a bar defines a subtree of \(T_{\mathbb {N} }\)extensionally, because it defines each path of the tree, as a path \(u \in \mathbb {N} ^\omega \) is in the tree if and only if there exists a finite prefix which is in the bar P.
A predicate \(Q \subseteq \mathbb {N} ^\star \) is hereditary if
$$ \forall w \in \mathbb {N} ^\star , \;\; \text {if}\;\; \forall n \in \mathbb {N} , w \cdot n \in Q \;\;\text {then}\;\; w \in Q. $$
Bar induction states that the extensional predicate associated to a bar implies its intensional counterpart: a predicate \(P_{ int } \subseteq \mathbb {N} ^\star \) which contains Q and which is hereditary.
Axiom 8
Given two predicates \(P_{ int }, Q\) over \(\mathbb {N} ^\star \), such that:
1.
for all \(\pi \in \mathbb {N} ^\omega \), there exists \(n \in \mathbb {N} \) such that \((\pi _1, \dots , \pi _n) \in Q\);
2.
for all \(w \in \mathbb {N} ^*\), it is decidable whether \(Q(w)\) or \(\lnot Q(w)\);
3.
for all \(w \in \mathbb {N} ^*\), \(Q(w) \Rightarrow P_{ int }(w)\);
4.
\(P_{ int }\) is hereditary;
then \(P_{ int }\) holds over the empty word: \(P_{ int }(\varepsilon )\).
Bar induction is a generalisation of the fan theorem, i.e. the constructive version of Kőnig’s lemma [28, pag. 56], and states that any extensionally well-founded tree T can be turned into an inductively-defined tree t that realises T [17, 39].
Our mechanisation of bar induction principle is formulated as a Proposition that is proved using classical reasoning, since it is not provable directly in the type theory of Coq. Unfortunately, while bar induction is a constructive principle, mainstream proof assistants do not support it yet, which is why on the one hand we had to postulate it as a proof principle while on the other hand we proved it in classical logic using the Excluded Middle axiom. This principle though has a computational content, Spector bar recursion6, which, currently, cannot be used in mainstream proof assistants such as Coq. Developing a type theory with a principle of bar induction is recent and ongoing work [30, 46].
Encoding states The version of bar induction we just outlined is not directly suitable for our purposes, as we need to reason about sequences of reductions rather than sequences of natural numbers. The solution is to encode STS states by natural numbers. This leads to the following issue: the nodes of the tree \(T_{\mathbb {N} }\) have a fixed arity, namely \(\mathbb {N} \), while processes have variably many reducts, including zero if they are stable. To deal with this glitch, it suffices to assume that there exists the following family of surjections:
A map \(f: A \rightarrow B\) is a surjection if it has a section \(g: B \rightarrow A\), that is, \(f \circ g = \textrm{Id}_B\).
This definition implies the usual one which states the existence of an antecedent \(x \in A\) for any \(y \in B\), and it is equivalent to it if we assume the Axiom of Choice.
Using this map F as a decoding function, any sequence of natural numbers corresponds to a path in the STS. Its subjectivity means that all paths of the LTS can be represented as such a sequence. This correspondence allows us to transport bar induction from sequences of natural numbers to executions of processes.
Note that such a family of surjections F exists for ACCS processes, and generally to most programming languages, because the set \(\textsf{Act}_\tau \) is countable, and so are processes. This leads to the following version of bar induction where words and sequences are replaced by finite and infinite executions.
Proposition 1
(Decidable bar induction over an STS). Let \(\langle S, \rightarrow \rangle \) be an STS such that a surjection as in (8) exists. Given two predicates \(Q, P_{ int }\) over finite executions, if
1.
for all infinite execution \(\eta \), there exists \(n \in \mathbb {N} \) such that \((\eta _1, \dots , \eta _n) \in Q\);
2.
for all finite execution \(\zeta \), \(Q(\zeta )\) or \(\lnot Q(\zeta )\) is decidable;
3.
for all finite execution \(\zeta \), \(Q(\zeta ) \Rightarrow P_{ int }(\zeta )\);
4.
\(P_{ int }\) is hereditary, as defined above except that \(\zeta \cdot q\) is a partial operation defined when \(\zeta \) is empty or its last state is p and \(p \rightarrow q\);
then \(P_{ int }\) holds over the empty execution: that is \(P_{ int }(\varepsilon )\) holds.
The last gap towards a useful principle is the requirement that every state in our STS has an outgoing transition. This condition is necessary to ensure the existence of the surjection in Equation (8). To ensure this requirement given any countably-branching STS, we enrich it by adding a sink state, which (a) is only reachable from stable states of the original STS, and (b) loops. This is a typical technique, see for instance [40, pag. 17].
Definition 10
Define
, where
is defined inductively as follows:
A maximal execution of \( Sink (S, \rightarrow )\) is always infinite, and it corresponds (in classical logic) to either an infinite execution of S or a maximal execution of S followed by infinitely many \(\top \). We finally prove the converse of Lemma 6.
Proposition 2
Given a countably branching STS \(\langle S, \rightarrow \rangle \), and a decidable predicate Q on S, we have that, for all \(s \in S\), \(\textsf{ext}_Q(s) \implies \textsf{int}_Q(s).\)
Now we thus obtain completeness of the intensional predicates.
Corollary 2
For every \(p\in A\) we have
1.
\(p\downarrow \) if and only if \(p\downarrow _i\), and
2.
for every \(r\) we have that \(p \textsc {must}r\) if and only if \(p \textsc {must}_ir\).
Proof
Direct consequence of Proposition 2, and Equation (ext-preds) and Equation (int-preds) above.
As we have outlined why Corollary 2 is true, from now on we use \(\downarrow _i\) and \(\textsc {must}_i\) instead of \(\downarrow \) and \(\textsc {must}\). In [8, Appendix B.2] we prove the properties of these predicates, that we use in the rest of the paper.
The LTS of sets Recall that soundness of \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) means that
. The naïve reasoning does not work. Fix two servers \(p\) and \(q\) such that \(p\mathrel {\preccurlyeq _{\textsf{AS}}}q\). We need to prove that for every client \(r\), if \(p \textsc {must}_ir\) then \(p \textsc {must}_ir\). Rule induction on the predicate \(p \textsc {must}_ir\) fails, as demonstrated by the following example.
Example 6
Consider the two servers \(p= \tau .(\overline{a} \mathrel {\parallel }\overline{b}) \mathrel {+}\tau .(\overline{a} \mathrel {\parallel }\overline{c})\) and \(q= \overline{a} \mathrel {\parallel }(\tau .\overline{b} \mathrel {+}\tau .\overline{c})\) of Equation (6). Fix a client \(r\) such that \(p \textsc {must}_ir\). Rule induction yields the following inductive hypothesis:
In the proof of \(q \textsc {must}_ir\) we have to consider the case where there is a communication between \(q\) and \(r\) such that, for instance, \(q\longrightarrow \tau .\overline{b} \mathrel {+}\tau .\overline{c}\) and \(r\longrightarrow r'\). In that case, we need to show that \(\tau .\overline{b} \mathrel {+}\tau .\overline{c}\; \textsc {must}_ir'\). Ideally, we would like to use the inductive hypothesis. This requires us to exhibit a \(p'\) such that
and \( p' \mathrel {\preccurlyeq _{\textsf{acc}}}\tau .\overline{b} \mathrel {+}\tau .\overline{c}\). However, note that there is no way to derive
, because
. The inductive hypothesis thus cannot be applied, and the naïve proof does not go through. \(\square \)
This example suggests that defining an auxiliary predicate \(\textsc {must}_{\textsf {aux}}\) in some sense equivalent to \(\textsc {must}_i\), but that uses explicitly weak outputs of servers, should be enough to prove that \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) is sound with respect to
. Unfortunately, though, there is an additional nuisance to tackle: server nondeterminism.
Example 7
Assume that we defined the predicate \(\textsc {must}_i\) using weak transitions on the server side. Recall the argument put forward in the previous example. The inductive hypothesis now becomes the following:
To use the inductive hypothesis we have to choose a \(p'\) such that \(p\mathrel {\overset{\overline{a}}{\Longrightarrow }} p'\) and \(p' \mathrel {\preccurlyeq _{\textsf{AS}}}\tau .\overline{b} \mathrel {+}\tau .\overline{c}\). This is still not enough for the entire proof to go through, because (modulo further \(\tau \)-moves) the particular \(p'\) we pick has to be related also to either \(\overline{b}\) or \(\overline{c}\). It is not possible to find such a \(p'\), because the two possible candidates are either \(\overline{b}\) or \(\overline{c}\); neither of which can satisfy \(p' \mathrel {\preccurlyeq _{\textsf{AS}}}\tau .\overline{b} \mathrel {+}\tau .\overline{c}\), as the right-hand side has not committed to a branch yet.
If instead of a single state \(p\) in the novel definition of \(\textsc {must}_i\) we used a set of states and a suitable transition relation, the choice of either \(\overline{b}\) or \(\overline{c}\) would be suitably delayed. It suffices for instance to have the following states and transitions: \(\{ p \} \mathrel {\overset{\overline{a}}{\Longrightarrow }} \{ \overline{b}, \overline{c} \}.\)\(\square \)
Now that we have motivated the main intuitions behind the definition of our novel auxiliary predicate \(\textsc {must}_{\textsf {aux}}\), we proceed with the formal definitions.
Definition 11
(LTS of sets). Let \(\mathcal {P}^{+}( Z )\) be the set of non-empty parts of Z. For any LTS \(\langle A, L , ~\longrightarrow ~ \rangle \), \( X \in \mathcal {P}^{+}( A) \) and \(\alpha \in L\), we define the sets
$$ D{(\alpha , X)} = \{ p' \ |\ \exists p\in X . \;p\longrightarrow p' \},\quad WD {(\alpha , X)} = \{ p' \ |\ \exists p\in X . \;p\mathrel {\overset{\alpha }{\Longrightarrow }} p' \}. $$
We construct the LTS \(\langle \mathcal {P}^{+}( A), \textsf{Act}_\tau , \longrightarrow \rangle \) by letting \( X \longrightarrow D{(\alpha , X)}\) whenever \(D{(\alpha , X)} \ne \emptyset \). Similarly, we have \(X \mathrel {\overset{ \alpha }{\Longrightarrow }} WD {(\alpha , X)}\) whenever \( WD {(\alpha , X)} \ne \emptyset \).
Intuitively, this definition lifts the standard notion of state derivative to sets of states. This construction is standard [11, 12, 23] and goes back to the determinisation of nondeterministic automata.
Fig. 7.
Rules to define inductively the predicate \(\textsc {must}_{\textsf {aux}}\).
Let \(\textsc {must}_{\textsf {aux}}\) be defined via the rules in Figure 7. This predicate lets us reason on \(\textsc {must}_i\) via sets of servers, in the following sense:
Lemma 7
For every LTSs \(\mathcal {L}_A, \mathcal {L}_B\) and every set of servers \(X \in \mathcal {P}^{+}(A)\), we have that \(X \textsc {must}_{\textsf {aux}}r\) if and only if for every \(p\in X . \;p \textsc {must}_ir\).
The LTS of sets has two important applications in this paper: first, it is used to define the \( \textsc {must}_{\textsf {aux}}\) relation, on which we rely to prove the soundness of the characterisation (see [8, Appendix E]). Additionally, it is used in the definition of the coinductive characterisation, which is the topic of the next section.
3.3 The action-based coinductive characterisation
We conclude this section by introducing a characterisation of the \(\textsc {must}\)-preorder that is more practical than \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), as it allows one to use the usual coinductive techniques. In addition, in the asynchronous case where processes are enhanced with forwarding, being able to use the coinductive proof method allows us to deal easily with the additional transitions due to forwarding. As a demonstration, we use this preorder to prove the code hoisting refinement shown in (6).
First, we recall the definition of this alternative preorder, which, like the other ones, is the same as in the synchronous case [1, 10, 41].
Definition 12
(Coinductive preorder). For all image-finite LTSs \(\mathcal {L}_A\), \(\mathcal {L}_B\) and all \(X \in \mathcal {P}^{+}(A), q\in B\), we let the coinductive preorder\(\mathrel {\preccurlyeq _{\textsf{co}}}\) be defined as the greatest relation such that whenever \(X \mathrel {\preccurlyeq _{\textsf{co}}}q\), the following requirements hold:
1.
\(X \downarrow \text { implies } q\downarrow \),
2.
For each \(q'\) such that \(q\longrightarrow q'\), we have that \(X \mathrel {\preccurlyeq _{\textsf{co}}}q'\),
3.
\(X \downarrow \) and
imply that there exist \(p\in X\) and \(p'\in A\) such that
and \(R(p') \subseteq R(q)\),
4.
For any \(\mu \in \textsf{Act} \), if \(X \mathrel {\Downarrow }{\mu }\), then for every \(X'\) and \(q'\) such that \(X \mathrel {\overset{\mu }{\Longrightarrow }} X'\) and \(q\longrightarrow q'\), we have that \(X' \mathrel {\preccurlyeq _{\textsf{co}}}q'\).
This preorder characterises
when the set X of servers is a singleton.
Theorem 2
For every image-finite LTS \(\mathcal {L}_A\), \(\mathcal {L}_B\in \textsc {Fdb}\), every \(p\in A\) and \(q\in B\), we have that
if and only if \(\{ \textsc {FW}(p) \} \mathrel {\preccurlyeq _{\textsf{co}}}FW(q)\).
The idea of the proof is to establish that the coinductive preorder characterises a version of the \(\textsc {must}\)-preorder that also has a set of servers on its LHS, and is defined as follows:
Observe that Definition 12 is based on single actions, instead of traces like \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), thus it gives us a practical proof method. To make this point, we now prove the code hoisting refinement (6). According to Theorem 2, it suffices to prove:
As for proofs by induction, when using coinduction it is helpful to prove a more general statement, which yields a useful coinductive hypothesis. This vocabulary corresponds to the proof theoretic point of view of coinduction, which matches how Coq implements coinductive proofs using cofix. In practice, the prover can use the coinductive hypothesis after the predicate defined coinductively has been unfolded at least once. In the set-theoretic setting used in Definition 12, this corresponds to choosing a relation R that is closed under the operations given in the definition. This is borne out by [8, Lemma 47].
4 Preorders based on must-sets and failure refinement
We now establish the second standard characterisation of the \(\textsc {must}\)-preorder, defined using \(\textsc {must}\)-sets, again thanks to Theorem 1. As an application, we relate the failure refinement used by the CSP community to the \(\textsc {must}\)-preorder.
We begin by defining formally the \(\mathrel {\preccurlyeq _{\textsf{MS}}}\) preorder, and we relate it to the \(\textsc {must}\)-preorder. For every \(X \subseteq _{ fin } \textsf{Act} \), that is for every finite set of visible actions, with a slight abuse of notation we write \(p\mathrel {\textsc {must}} X\) whenever \(p\mathrel {\overset{ \varepsilon }{\Longrightarrow }} p'\) implies that \(p' \mathrel {\overset{ \mu }{\Longrightarrow }}\) for some \(\mu \in X\), and we say that X is a \(\textsc {must}\)-set of \(p\). Let \( ( p \, \textsf{after} \, s , \longrightarrow ) = \{ p' \ |\ p\mathrel {\overset{s}{\Longrightarrow }} p' \}\). For every \(\mathcal {L}_A, \mathcal {L}_B\) and \(p\in A, q\in B\), let \(p\preccurlyeq _{\textsc {m}}q\) whenever \(\forall s\in \textsf{Act}^\star \) we have that \(p\mathrel {\Downarrow }{ s}\) implies that \((\forall X \subseteq _{ fin } \textsf{Act} \) if \( (p \, \textsf{after} \, s, \longrightarrow _A) \mathrel {\textsc {must}} X\) then \( (q \, \textsf{after} \, s, \longrightarrow _B) \mathrel {\textsc {must}} X).\)
Definition 13
For all \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fdb}\) and servers \(p\in A\) and \(q\in B\), we let \(p\mathrel {\preccurlyeq _{\textsf{MS}}}q\) whenever \(p\mathrel {\preccurlyeq _{\textsf{cnv}}}q\wedge p\preccurlyeq _{\textsc {m}}q\).
Lemma 8
Let \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fdb}\). For all \(p\in A\) and \(q\in B\) such that \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{cnv}}}\textsc {FW}(q)\), we have that \(\textsc {FW}(p) \preccurlyeq _{\textsc {m}}\textsc {FW}(q)\) if and only if \(\textsc {FW}(p) \preccurlyeq ^{\textsf{fw}}_{\textsf {acc}}\textsc {FW}(q)\).
As a direct consequence, we obtain the following result.
Theorem 3
Let \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fdb}\). For all \(p\in A\) and \(q\in B\), we have that
if and only if \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{MS}}}\textsc {FW}(q)\).
Failure refinement\(\textsc {must}\)-sets have been used mainly by De Nicola and collaborators, for instance in [15, 26], and are closely related to the failure refinement proposed in [19] by Hoare, Brookes and Roscoe for TCSP (the process algebra based on Hoare’s language CSP [18, 37]). Following [19], a failure of a process \(p\) is a pair \((s, X)\) such that \(p \mathrel {\overset{ s}{\Longrightarrow }} p'\) and
for all \(\mu \in X\). Then, failure refinement is defined by letting \(p\mathrel {\le _{\textsf {fail}}}q\) whenever the failures of \(q\) are also failures of \(p\). This refinement was designed to give a denotational semantics to processes, and mechanisations in Isabelle/HOL have been developed to ensure that the refinement is well defined [5, 50]. Both Hennessy [32, pag. 260] and [20] highlight that the failure model can be justified operationally via the \(\textsc {must}\) testing equivalence: it is folklore dating back to [25, Section 4] that failure equivalence and
coincide. Thanks to Theorem 3 we conclude that in fact
coincides with the failure divergence refinement [51], that is, the intersection of \(\mathrel {\le _{\textsf {fail}}}\) and \(\mathrel {\preccurlyeq _{\textsf{cnv}}}\).
Corollary 3
Let \(\mathcal {L}_A, \mathcal {L}_B \in \textsc {Fdb}\). For every \(p\in A\) and \(q\in B\), we have that
if and only if \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{cnv}}}\textsc {FW}(q)\) and \(\textsc {FW}(p) \mathrel {\le _{\textsf {fail}}}\textsc {FW}(q)\).
5 Related work
Here we discuss in detail the works more closely related to the results of this paper. Further discussion on related work may be found in [8, Appendix A].
The first investigation on the \(\textsc {must}\)-preorder in an asynchronous setting was put forth by [21]. While their very clear examples shed light on the preorder, their alternative preorder (Definition 6 in that paper) is more complicated than necessary: it uses the standard LTS of TACCS, its lifting to an LTS with forwarding, and two somewhat ad-hoc notions: a predicate \({\mathop {\rightsquigarrow }\limits ^{I}}\) and a condition on multisets of inputs. Moreover that preorder is not complete because of a glitch in the treatment of divergence. The details of the counter-example we found to that completeness result are given in [8, Appendix I].
In [34] Hennessy outlines how to adapt the approach of [21] to a typed asynchronous \(\pi \)-calculus. While the LTS with forwarding is replaced by a Context LTS, the predicates to define the alternative preorder are essentially the same as those used in the preceding work with Castellani. Acceptance sets are given in Definition 3.19 there, and the predicate \({\mathop {\rightsquigarrow }\limits }\) is denoted \(\searrow \), while the generalised acceptance sets of [21] are given in Definition 3.20. Owing to the glitch in the completeness of [21], it is not clear that Theorem 3.28 of [34] is correct either.
Also the authors of [15] consider the \(\textsc {must}\)-preorder in ACCS. There is a major difference between their approach and ours. When studying theories for asynchronous programs, one can either
(1)
keep the definitions used for synchronous programs, and enhance the LTS with forwarders; or
(2)
adapt the definitions, and keep the standard LTS.
In the first case, the complexity is moved into the LTS, which becomes infinite-branching and infinite-state. In the second case, the complexity is moved into the definitions used to reason on the LTS (i.e. in the meta-language), and in particular in the definition of the alternative preorder, which deviates from the standard one. The authors of [15] follow the second approach. This essentially explains why they employ the standard LTS of CCS and to tackle asynchrony they reason on traces via (1) a preorder \(\preceq \) (Table 2 of that paper) that defines on input actions the phenomena due to asynchrony; and (2) a rather technical operation on traces, namely \(s \ominus s' = ( \{\!|s|\!\}_{i} \setminus \{\!|s'|\!\}_{i}) \setminus \overline{( \{\!|s|\!\}_{o} \setminus \{\!|s'|\!\}_{o} )}\). We favour instead the approach in (1), for it helps achieve a modular mechanisation.
The authors of [27] give yet another account of the \(\textsc {must}\)-preorder. Even though non-blocking outputs can be written in their calculus, they use a left-merge operator that allows writing blocking outputs. The contexts that they use to prove the completeness of their alternative preorder use such blocking outputs, consequently their arguments need not tackle the asymmetric treatment of input and output actions. This explains why they can use smoothly a standard LTS, while [21] and [15] have to resort to more complicated structures.
Theorem 5.3 of the PhD thesis by [52] states an alternative characterisation of the \(\textsc {must}\)-preorder, but it is given with no proof. The alternative preorder given in Definition 5.8 of that thesis turns out to be a mix of the ones by [21] and [15]. In particular, the definition of the alternative preorder relies on the LTS with forwarding, there denoted \(\longrightarrow _A\) (Point 1. in Definition 5.1 defines exactly the input transitions that forward messages into the global buffer). The condition that compares convergence of processes is the same as in [21], while server actions are compared using \(\textsc {must}\)-sets, and not acceptance sets. In fact, Definition 5.7 there is titled “acceptance sets ” but it actually defines \(\textsc {must}\)-sets.
6 Conclusion
In this paper we have shown that the standard characterisations of the \(\textsc {must}\)-preorder by De Nicola and Hennessy [25, 32] are sound and complete also in an asynchronous setting, provided servers are enhanced with the forwarding ability. Lemma 2 shows that this lifting is always possible. We have also shown that the standard coinductive characterisation carries over to the asynchronous setting. Our results are supported by the first mechanisation of the \(\textsc {must}\)-preorder, and increase proof (i.e. code) factorisation and reusability since the alternative preorders do not need to be changed when shifting between synchronous and asynchronous semantics: it is enough to parameterise the proofs on the set of non-blocking actions. Corollary 3 states that \(\textsc {must}\)-preorder and failure refinement essentially coincide. This might spur further interest in the mechanisations of failure refinement, carried out so far in Isabelle/HOL [5, 50], possibly opening up opportunities of joint efforts for automated checking.
Proof method for\(\textsc {must}\)-preorder Theorems 1, 2 and 3 endow researchers in programming languages for message-passing software with a proof method for
, namely: to define for their calculi an LTS that enjoys the axioms of output-buffered agents with feedback. An example of this approach is Corollary 1.
Live programs have barred trees We argued that a proof of \(p \textsc {must}r\) is a proof of liveness (of the client). This paper is thus de facto an example that proving liveness amounts to prove that a computational tree has a bar (identified by the predicate \(\textsc {good}\)), and hence bar induction is a natural way to reason constructively on liveness-preserving manipulations on programs. While this fact seems to be by and large unexploited by the PL community, we believe that it may be of interest to practitioners reasoning on liveness properties in theorem provers in particular, and to the PL community at large.
Mechanisation Boreale and Gadducci [13] remark that the \(\textsc {must}\)-preorder lacks a tractable proof method. In constrast, we argue that our contributions, in particular the coinductive characterisation (Theorem 2), being fully mechanised in Coq, let practitioners pursue non-trivial results about testing preorders for real-world programming languages. To make this point, we have proved a form of code-hoisting using this characterisation. Our mechanisation lowers the barrier to entry for researchers versed into theorem provers and wishing to use testing preorders; adds to the toolkit of Coq users an alternative to the well-known (and already mechanised) bisimulation equivalence [45]; and provides a starting point for researchers willing to study testing preorders and analogous refinements within type theory. Researchers working on testing preorders may benefit from it, as there are analogies between reasoning techniques for May, \(\textsc {must}\), Compliance, Should, and Fair testing. For instance Baldan et al. show with pen and paper that a technique similar to forwarding works to characterise the \(\textsc {may}\)-preorder [4].
Future work Thanks to Theorems 1, 2 and 3 we can now set out to (1) devise an axiomatisation of
for asynchronous calculi, as done in [14, 32, 33, 35] for synchronous ones; (2) study for which asynchronous calculi
is a pre-congruence; (3) machine-check semantic models of subtyping for session types [10]; (4) study the decidability of
.
More in general, given the practical relevance of asynchronous communication, it seems crucial not only to adapt the large body of theory for synchronous communication to the asynchronous setting but also to resort to machine supported reasoning to do it. This paper is meant to be a step in this direction.
Data availability The mechanised proofs have been archived on Zenodo[7].
Acknowledgments
We thank the anonymous reviewers for their helpful comments, and Roberto Amadio for useful remarks. The first author would like to acknowledge his “N+1 honoris causa” Pierre-Evariste Dagand for the systematic and useful feedback, Guillaume Geoffroy for suggesting the use of bar induction, and Hugo Herbelin for discussions on the topic. This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101003349).
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
In general the reduction semantics and the LTS of a calculus are defined independently, and connected via the Harmony lemma ([47], Lemma 1.4.15 page 51). We have a mechanised proof of it.
In the calculus TACCS (a variant of ACCS tailored for testing semantics) of [21] there is a construct of asynchronous output prefix, but its behaviour is to spawn the corresponding atom in parallel with the continuation, so it does not act as a prefix.
The syntax of ACCS, which is closely inspired by that of the asynchronous \(\pi \)-calculus with input- and \(\tau \)-guarded choice [2, 3], is given in Equation (5) and discussed later.
denote a client-server system, that is a parallel composition in which the identities of the server \(p\) and the client \(r\) are distinguished, and whose computations have the form
where each step represents either an internal computation of one of the two components, or an interaction between them. Interactions correspond to handshakes, where two components ready to perform matching input/output actions advance together. We express liveness by saying that \(p\text { must pass } r\), denoted \( p \textsc {must} r\), if in every maximal computation of
there exists a state
such that \(\textsc {good}(r_i)\), where \(\textsc {good}\) is a decidable predicate indicating that the client has reached a successful state. Servers are then compared according to their capacity to satisfy clients, i.e. via contexts of the form
and the predicate \(\textsc {must}\). Morris preorder then becomes the \(\textsc {must}\)-preorder by De Nicola and Hennessy [25] :
thus shed light on liveness-preserving program transformations.
, and (2) a predicate \(\textsc {good}\) over programs. Hence
may relate servers written in different languages. For instance, servers written in OCaml may be compared to servers written in Java according to clients written in Python, because all these languages use the same basic protocols for communication.
requires analysing an infinite amount of clients, and so the definition of the preorder does not entail an effective proof method. A solution to this problem is to define an alternative (semantic) characterisation of the preorder
, i.e. a preorder \(\preccurlyeq _{ alt }\) that coincides with
and does away with the universal quantification over clients (i.e. contexts). In synchronous settings, i.e. when both input and output actions are blocking, such alternative characterisations have been thoroughly investigated, typically via a behavioural approach based on labelled transition systems.
following one of two different approaches: \(\textsc {must}\)-sets or acceptance sets.
in the following sense:
While these alternative preorders do away with the universal quantification over clients, they are not practical to use directly, as they still universally quantify over (finite) traces of actions. A more practical approach [1] is to use a coinductively defined preorder \(\mathrel {\preccurlyeq _{\textsf{co}}}\) based on \(\mathrel {\preccurlyeq _{\textsf{AS}}}\) [1, 10, 41]. This preorder has two advantages: first, its definition quantifies universally only on single actions; second, it allows the user to use standard coinductive methods, as found in the literature on bisimulation. In the case where the LTS is image-finite, such as for CCS and most process calculi, the coinductive preorder is sound and complete:
Asynchrony In distributed systems, communication is inherently asynchronous. For instance, the standard TCP transmission on the Internet is asynchronous. Actor languages like Elixir and Erlang implement asynchrony via mailboxes, and both Python and JavaScript offer developers the constructs async/wait, to return promises (of results) or wait for them. In this paper we model asynchrony via output-buffered agents with feedback, as introduced by Selinger [49]. These are LTSs obeying the axioms in Figure 2, where \(a\) denotes an input action, \(\overline{a}\) denotes an output action, \(\tau \) denotes the internal action, and \(\alpha \) ranges over all these actions. For instance, the Output-commutativity axiom states that an output \(\overline{a}\) can always be postponed: if \(\overline{a}\) is followed by any action \(\alpha \), it can commute with it. In other words, outputs are non-blocking, as illustrated by the LTS for \(r_0\) in Figure 1. We defer a more detailed discussion of these axioms to Section 2.
. Efforts in this direction have been made, all of which focussed on process calculi [15, 21, 34, 52], while the axioms in Figure 2 apply to LTSs. Note that these axioms impose conditions only over outputs, and this asymmetric treatment of inputs and outputs substantially complicates the proofs of completeness and soundness of the alternative characterisations of
. To underline the subtleties due to asynchrony, we note that the completeness result for asynchronous CCS given by Castellani and Hennessy in [21], and subsequently extended to the \(\pi \)-calculus by Hennessy [34], is false (see [8, Appendix I]).
can be characterised constructively. The original definitions of \(\textsc {must}\) and termination given by De Nicola [25], though, are extensional. We show how to use Brouwer bar induction principle to prove that the two approaches are logically equivalent (Corollary 2). Since Rahli et al. [46] have shown bar induction to be compatible with constructive type theory, we argue that our development is entirely constructive.
are modelled as state transition systems with a reduction semantics. We now formally define this two-level semantics.
in which \(p\) is deemed to be the server of client \(r\). In general, every system
is the root of a state transition system (STS), \(\langle S, \longrightarrow \rangle \), where \(S\) is the set of states and \(\longrightarrow \) is the reduction relation. For the sake of simplicity1 we derive the reduction relation from the LTS semantics of servers and clients as specified by the rules in Figure 4. In our mechanisation (Figure 3), 
is successful if there exists a state
such that \(\textsc {good}(r_i)\). We assume the predicate \(\textsc {good}\) to be invariant under outputs:All the previous works on asynchronous calculi implicitly make this assumption, since they rely on ad-hoc actions such as \(\omega \) or \(\checkmark \) to signal success and they treat them as outputs. In [8, Appendix H] we show that this assumption holds for the language 
is successful.
whenever for every client r we have that \(p \textsc {must}r\) implies \(q \textsc {must}r\).
, where \(p_0\) and \(r_0\) are the server and client given in Figure 1. The unique maximal computation of this system is
. This computation is successful since it leads the client to the \(\textsc {good}\) state \(r_3\). Hence, client \(r_0\) is satisfied by server \(p_0\). Since Output-commutativity implies an absence of causality between the output \(\overline{\texttt {str}}\) and the input \(\texttt {int}\) in the client, it is the order between the input \(\texttt {str}\) and the output \(\overline{\texttt {int}}\) in the server that guides the order of client-server interactions. \(\square \)
as well as its standard LTS5 whose properties we discuss in detail in [8, Appendix H]. This is exactly the syntax used in [15, 49], without the operators of restriction and relabelling. Here the syntactic category g defines guards, i.e. the terms that may be used as arguments for the \(+\) operator. As in most process calculi, 0 denotes the terminated process that cannot do any action. Note that, apart from \(\mathop {\textsf {0}}\), only input-prefixed and \(\tau \)-prefixed terms are allowed as guards, and that the output prefix operator is replaced by atoms \(\overline{a}\). In fact, this syntax is completely justified by Selinger axioms, which, as we argued above, specify that outputs cannot cause any other action, nor be in conflict with it.
by leveraging the possibility of divergence of \(\text {{Pierre}} \) after the input \(b\). Fix an \(r\) such that \( \text {{Pierre}} \textsc {must}r \). Note that, since 0 is the terminated process, the condition for the server 0 to satisfy r is that r reaches by itself a successful state in each of its maximal computations. We distinguish two cases, according to whether \(r\longrightarrow \) or
.
in which \(\text {{Pierre}} \) diverges and \(r\) does not move after the first output. Since \(\text {{Pierre}} \textsc {must}r\), either \(\textsc {good}(r)\) or \(\textsc {good}(r')\). In case \(\textsc {good}(r')\), by Equation (4) we get also \(\textsc {good}(r)\). Hence \( \mathop {\textsf {0}} \textsc {must}r\).
. Suppose \(r= r_0 \longrightarrow r_1 \longrightarrow r_2 \longrightarrow \ldots \) is a maximal computation of \(r\). Then
has a maximal computation
. As \(\text {{Pierre}} \textsc {must}r\), there must exist an \(i \in \mathbb {N} \) such that \(\textsc {good}(r_i)\). Hence \( \mathop {\textsf {0}} \textsc {must}r\). \(\square \)
. Consider the following form of code hoisting:
If we see the above nondeterministic sums as representing the two branches of a conditional statement, this refinement corresponds to hoisting the shared action \(\overline{a}\) before the conditional statement, a common compiler optimisation. Proving Equation (6) via the contextual definition of
is cumbersome. This motivates the study of alternative characterisations for
, and in the rest of the paper we present several preorders that fit the purpose, in particular the coinductive preorder \(\mathrel {\preccurlyeq _{\textsf{co}}}\), which we will use to establish Equation (6) in Section 3.3.
and thus \(\varOmega \downarrow \). In other words, the same predicates can be applied to different LTSs, and since the alternative characterisations of
are defined using such predicates, they can relate different LTSs.
in our asynchronous setting. We also present a new characterisation that disregards the order of non-causally related actions. We then explain the tools we use to prove these characterisations, and in particular their soundness. This section ends with the coinductive version \(\mathrel {\preccurlyeq _{\textsf{co}}}\) of \(\mathrel {\preccurlyeq _{\textsf{AS}}}\), which we use to prove the hoisting refinement (6).
.
but
, because \(\mathcal {A}( p, \epsilon ) =\{ \{ a \} \}\) and \(\mathcal {A}( q, \epsilon ) =\{ \emptyset \}\), and corresponding to the ready set \(\emptyset \in \mathcal {A}( q, \epsilon )\) there is no ready set \(\widehat{R} \in \mathcal {A}( p, s)\) such that \(\widehat{R} \subseteq \emptyset \). Intuitively this is the case because acceptance sets treat inputs and outputs similarly, while in an asynchronous setting only outputs can be tested.
, if servers are enhanced as with forwarding. We now introduce this concept.
The Input-Boomerang axiom states a kind of input-enabledness property, which is however more specific as it stipulates that the target state of the input should loop back to the source state via a complementary output. This is the essence of the behaviour of a forwarder, whose role is simply to pass on a message and then get back to its original state. The Fwd-Feedback axiom is a weak form of Selinger’s Feedback axiom, which is better understood in conjunction with the Input-Boomerang axiom: if the transition sequence \(p\longrightarrow p'\longrightarrow q\) in the Fwd-Feedback axiom is taken to be the transition sequence \(p'\longrightarrow p\longrightarrow p'\) in the Input-Boomerang axiom, then we see that it must be \(q=p\) in the Fwd-Feedback axiom. Moreover, no \(\tau \) action is issued when moving from p to q, since no synchronisation occurs in this case: the message is just passed on.
:
for every \(\mathcal {L}= \langle A, L, \longrightarrow \rangle \), where the states in \(\textsc {FW}(\mathcal {L})\) are pairs denoted \(p \triangleright M\), such that \(p \in A\) and \(M \in MO \), and the transition relation
is defined via the rules in Figure 6.
is reminiscent of the one introduced in Definition 8 by Honda and Tokoro in [38]. The construction given in our Definition 6, though, does not yield the LTS of Honda and Tokoro, as
adds the forwarding capabilities to the states only at the top-level, instead of descending structurally into terms. As a consequence, in the LTS of [38] \(a.\mathop {\textsf {0}}+ \mathop {\textsf {0}}\longrightarrow \overline{ b}\), while
.
is infinitely-branching: for every mailbox M we have \(p\triangleright M \mathrel {\overset{a_i}{\longrightarrow }_\textsf{fw}} p\triangleright (\{\!|\overline{a_i}|\!\} \uplus M)\) for every \(a_i \in \mathcal {N} \). This is illustrated by the following picture, where for simplicity we omit the subscript \(\textsf{fw}\) under the arrows. 
using LTSs in \(\textsc {Fwd}\).
if and only if
.
. This definition suffices to characterise
because in each LTS that is Fwd every state performs every input, thus comparing inputs has no impact on the preorder \(\mathrel {\preccurlyeq _{\textsf{acc}}}\) of Definition 5. More formally, for every \(\mathcal {L}_A, \mathcal {L}_B\in \textsc {Fwd}\) and every \(p\in A\) and \(q\in B\), we letWe have the following logical equivalence.
over LTSs with forwarding. This is indeed true:
then we have \({ p} \mathrel {\preccurlyeq _{\textsf{AS}}}{ q}\).
iff \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{AS}}}\textsc {FW}(q).\)
with the failure refinement, we outline the proof of Theorem 1, and, in particular, the technical tools we used.
, where
is defined inductively as follows: 
. The naïve reasoning does not work. Fix two servers \(p\) and \(q\) such that \(p\mathrel {\preccurlyeq _{\textsf{AS}}}q\). We need to prove that for every client \(r\), if \(p \textsc {must}_ir\) then \(p \textsc {must}_ir\). Rule induction on the predicate \(p \textsc {must}_ir\) fails, as demonstrated by the following example.
and \( p' \mathrel {\preccurlyeq _{\textsf{acc}}}\tau .\overline{b} \mathrel {+}\tau .\overline{c}\). However, note that there is no way to derive
, because
. The inductive hypothesis thus cannot be applied, and the naïve proof does not go through. \(\square \)
. Unfortunately, though, there is an additional nuisance to tackle: server nondeterminism.
imply that there exist \(p\in X\) and \(p'\in A\) such that
and \(R(p') \subseteq R(q)\),
when the set X of servers is a singleton.
if and only if \(\{ \textsc {FW}(p) \} \mathrel {\preccurlyeq _{\textsf{co}}}FW(q)\).
if and only if \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{MS}}}\textsc {FW}(q)\).
for all \(\mu \in X\). Then, failure refinement is defined by letting \(p\mathrel {\le _{\textsf {fail}}}q\) whenever the failures of \(q\) are also failures of \(p\). This refinement was designed to give a denotational semantics to processes, and mechanisations in Isabelle/HOL have been developed to ensure that the refinement is well defined [5, 50]. Both Hennessy [32, pag. 260] and [20] highlight that the failure model can be justified operationally via the \(\textsc {must}\) testing equivalence: it is folklore dating back to [25, Section 4] that failure equivalence and
coincide. Thanks to Theorem 3 we conclude that in fact
coincides with the failure divergence refinement [51], that is, the intersection of \(\mathrel {\le _{\textsf {fail}}}\) and \(\mathrel {\preccurlyeq _{\textsf{cnv}}}\).
if and only if \(\textsc {FW}(p) \mathrel {\preccurlyeq _{\textsf{cnv}}}\textsc {FW}(q)\) and \(\textsc {FW}(p) \mathrel {\le _{\textsf {fail}}}\textsc {FW}(q)\).
, namely: to define for their calculi an LTS that enjoys the axioms of output-buffered agents with feedback. An example of this approach is Corollary 1.
for asynchronous calculi, as done in [14, 32, 33, 35] for synchronous ones; (2) study for which asynchronous calculi
is a pre-congruence; (3) machine-check semantic models of subtyping for session types [10]; (4) study the decidability of
.
