# On Composing Communicating Systems

Franco Barbanera, Ivan Lanese, Emilio Tuosto

► To cite this version:

Franco Barbanera, Ivan Lanese, Emilio Tuosto. On Composing Communicating Systems. ICE 2022 - 15th Interaction and Concurrency Experience, Jun 2022, Lucca, Italy. pp.53-68, 10.4204/EPTCS.365.4. [https://hal-03915946](https://hal-03915946)

HAL Id: hal-03915946

https://inria.hal.science/hal-03915946

Submitted on 30 Dec 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Composing Communicating Systems *

Franco Barbanera

Dept. of Mathematics and Computer Science, University of Catania (Italy)

Ivan Lanese

Focus Team, University of Bologna/INRIA (Italy)

Emilio Tuosto

Gran Sasso Science Institute (Italy)

Communication is an essential element of modern software, yet programming and analysing communicating systems are difficult tasks. A reason for this difficulty is the lack of compositional mechanisms that preserve relevant communication properties.

This problem has been recently addressed for the well-known model of communicating systems, that is sets of components consisting of finite-state machines capable of exchanging messages. The main idea of this approach is to take two systems, select a participant from each of them, and derive from those participants a pair of coupled gateways connecting the two systems. More precisely, a message directed to one of the gateways is forwarded to the gateway in the other system, which sends it to the other system. It has been shown that, under some suitable compatibility conditions between gateways, this composition mechanism preserves deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange).

This paper considers the case of asymmetric synchronous communications where senders decide independently which message should be exchanged. We show here that preservation of lock freedom requires sequentiality of gateways, while this is not needed for preservation of either deadlock freedom or strong lock freedom.

## 1 Introduction

Communication is an essential constitutive element of modern software due to the fact that applications are increasingly developed in distributed architectures (e.g., service-oriented architectures, microservices, cloud, etc.). In practice, APIs and libraries featuring different communication mechanisms are available for practically any programming language. At a theoretical level, several models have been used to study interactions between systems (e.g., process algebras, transition systems, Petri nets, logical frameworks, etc.).

Reasoning and developing communicating systems are difficult endeavours. The so-called business logic, necessary to determine what has to be communicated, needs to be complemented with the so-called application level protocol specifying how information spreads across a system. Conceptual and programming errors may occur in the realisation of application level protocols. For instance, it may happen that some components in a system are prevented to communicate because all the expected partners terminated their execution (deadlock). Other typical errors occur when a system is not lock-free, that is when some components cannot progress because all their partners are perpetually involved in other

<footnote>* Research partly supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233, by the MIUR project PRIN 2017FTXR7S "IT-MaTTERS" (Methods and Tools for Trustworthy Smart Systems) and by the Progetto di Ateneo "Piaceri". The authors have also been partially supported by INdAM as members of GNCS (Gruppo Nazionale per il Calcolo Scientifico). The authors thank the reviewers for their helpful comments and also Mariangiola Dezani for her support.</footnote>
communications. A source of these problems is when a system can evolve in different ways depending on some conditions and components have inconsistent “views” of the state of the system. If this happens, some components may reach a state no longer “compatible” with the state of their partners and therefore communications cannot take place as expected.

We illustrate these problems with some simple examples for deadlock freedom (similar examples may be given for lock freedom). Suppose we want to model a client-server system where clients’ requests are acknowledged either with an answer or with “unknown” from servers. Due to its popularity, we choose CCS [16] to introduce this scenario, so take the following agents:

$$C = \bar{r}.a + \bar{r}.u \quad \text{and} \quad D = r.\bar{a} + r.\bar{u} \qquad (1)$$

where ports r, a, and u are respectively used to communicate requests, answers, and unknowns. (Recall that in CCS a. and _ + _ represent respectively prefix and non-deterministic choice.) The common interpretation of agents in (1) is that x and x̄ respectively represent an input and an output on port x. It is a simple observation that the system C | D where C and D run in parallel can evolve to e.g., the deadlock state a | ū where each party is waiting for the other to progress. The problem is that the choice of what communication should happen after a request is taken independently by C and D instead of letting D to take the decision and drive C “on the right” branch. This is attempted in the next version:

$$C = \bar{r}.(a + u) \quad \text{and} \quad D = r.(\bar{a} + \bar{u}) \qquad (2)$$

A key difference with the agents in (1) is that the server D in (2) decides what to reply to the client C, which becomes aware of the choice through the interaction with D after the request has been made. Let us now assume that the server D acts as a proxy to another server, say D'. When D cannot return an answer to the client it interacts with D' on port p. Answers are sent directly to the client if D' can compute them, otherwise D' returns an unknown on port u' to D which forwards it to the client. This is modelled by the agents

$$D = r.(\bar{a} + \bar{p}.u'.\bar{u}) \quad \text{and} \quad D' = p.(\bar{a} + \bar{u}') \qquad (3)$$

Note that this change is completely transparent to agent C, which in fact stays as in (2). It is now more difficult to ascertain if these choices may lead to a deadlock since the decision of D may involve also D'. Indeed, the parallel composition of agents in (3) may deadlock because, when C and D interact on port a, D' hangs on port p and, likewise, if C and D' interact on port a then D hangs on port u'.

A reason for this difficulty is that it is hard to define compositional mechanisms that preserve relevant communication properties such as deadlock or lock freedom. Recently, an approach to the composition of concurrent and distributed systems has been proposed in [2, 3] for the well-known model of systems of communicating finite-state machines (CFSMs) [11], that is sets of finite-state automata capable of exchanging messages. The compositional mechanism is based on the idea that two given systems, say S and S', are composed by transforming two CFSMs, say H in S and K in S', into “coupled forwarders”. Basically, each message that H receives from a machine in S is forwarded to K and vice versa. It has been shown that, under suitable compatibility conditions between H and K, this composition mechanism preserves deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange). The compatibility condition identified in [2, 3] consists in exhibiting essentially dual behaviours: gateway H is able to receive a message whenever gateway K is willing to send one and vice versa. As observed in [4], a remarkable feature of such an approach is that it enables the composition of systems originally designed
as closed systems. As far as two compatible machines can be found, any two systems can be composed by transforming as hinted above the compatible machines.

The results in [2, 3] are developed in the asynchronous semantics of CFSMs. These results have been transferred in [5] to a setting where CFSMs communicate synchronously much like as the communication mechanisms considered for instance in process algebras like CCS, ACP, etc. This model assumes a perfect symmetry between sender and receiver in synchronous communications. Let us again discuss this with an example. Consider the agents

$$T = \bar{a}.P + \bar{b}.Q \quad \text{and} \quad R = a.P' + b.Q' \quad (4)$$

According to the standard semantics of CCS [16], system $(T|R) \setminus \{a,b\}$ has two possible evolutions:

$$(T|R) \setminus \{a,b\} \xrightarrow{\tau} P | P' \quad \text{and} \quad (T|R) \setminus \{a,b\} \xrightarrow{\tau} Q | Q'$$

namely, either both $T$ and $R$ opt for the “leftmost” branch (synchronising on a) or they both choose the “rightmost” one (synchronising on b). (Recall that in CCS $\_\setminus X$ is the hiding of ports in the set $X$ and that $\tau$ represents an internal action.) This means that, the resolution of the choice is implicit in the communication mechanism: a branch is taken as soon as $T$ and $R$ synchronise on the corresponding port. Intuitively, no distinction is made between sender and receiver (formally they are indeed interchangeable); this implies that the communication mechanism is at the very core of choice resolution [5].

Interestingly, for synchronous communications, an alternative interpretation is actually possible where this perfect symmetry is not assumed so that sender and receiver play different roles in choice resolution while still relying on synchronous communication. Let us explain this interpretation using again CCS. Consider a variant of CCS where outputs must be enabled before being fired. One could formally specify that with the following reduction rules:

$$\bar{a}.P + P' \xrightarrow{\tau} \bar{a}.P \quad \text{and} \quad \bar{a}.P | (a.Q + Q') \xrightarrow{\tau} P|Q \quad (5)$$

whereby the leftmost rule chooses one of the possible outputs of the sender (the chosen output is marked by the double bar in our notation) and the rightmost rule actually synchronises sender and receiver. This semantics is an abstract model of asymmetric communications (used e.g., in [7, 17]), where silent steps taken using the left rule model some internal computation of the sender to decide what to communicate to the partner. In other words, now the choice is entirely resolved on “one side” while the communication is a mere interaction of complementary actions, the output and the input. This asymmetry, at the core of asynchronous communication, can therefore also carry for synchronous communication.

It is worth observing that asymmetric communications abstract a rather common programming pattern where sending components may choose the output to execute depending on some internal computation. For instance, elaborating on the proxy scenario in (3), $D$ could decide to directly send unknowns to normal clients while reserving the use of $D'$ only for “privileged” clients.

**Contributions.** This paper transfers the composition by gateway mechanism of [2, 3] to the case of asymmetric synchronous communication of CFSMs. The main technical results are that, in the asymmetric case, gateway composition

* preserves deadlock freedom (as well as a strong version of lock freedom) provided that systems are composable (the relation of compatibility – one of the requirements for systems to be composable – in the present paper is less restrictive than the one used in [5]);
* preserves lock freedom if systems are composable and gateways are sequential, namely each state has at most one outgoing transition.

Interestingly, preservation of deadlock freedom can be guaranteed under milder conditions than in the symmetric case. In fact, sequentiality of gateways is not necessary to preserve deadlock freedom in the asymmetric case, while it is in the symmetric one.

**Structure of the paper.** Section 2 introduces systems of (asymmetric synchronous) CFSMs, related notions and communication properties. Composition by gateways is introduced and discussed in Section 3 together with the compatibility relation. Section 4 discusses the issues that prevent gateway composition to preserve communication properties. Section 5 is devoted to the preservation of communication properties. Conclusions, related and future work are discussed in Section 6.

## 2 Background

Communicating Finite State Machines (CFSMs) [11] are Finite State Automata (FSAs) where transitions are labelled by communications. We recall basic notions on FSAs.

A finite state automaton (FSA) is a tuple $A = (\mathcal{S}, q_0, \mathcal{L}, \rightarrow)$ where

* $\mathcal{S}$ is a finite set of states (ranged over by lowercase italic Latin letters);

* $q_0 \in \mathcal{S}$ is the initial state;

* $\mathcal{L}$ is a finite set of labels

* $\rightarrow \subseteq \mathcal{S} \times (\mathcal{L} \cup \{\tau\}) \times \mathcal{S}$ is a set of transitions.

Hereafter, we let $\lambda$ range over $\mathcal{L} \cup \{\tau\}$ when it is immaterial to specify the set of labels or it is understood. We use the usual notation $q_1 \xrightarrow{\lambda} q_2$ for the transition $(q_1, \lambda, q_2) \in \rightarrow$, and $q_1 \rightarrow q_2$ when there exists a label $\lambda$ such that $q_1 \xrightarrow{\lambda} q_2$. Let $\lambda_1, \lambda_2, \dots, \lambda_n$ be the concatenation operation on labels and write $p \xrightarrow{\pi} q$ where $\pi = \lambda_1 \cdot \lambda_2 \cdot \dots \cdot \lambda_n$ whenever $p \xrightarrow{\lambda_1} p_1 \xrightarrow{\lambda_2} \dots \xrightarrow{\lambda_n} p_n = q$. We let $\pi, \psi, \dots$ range over $\mathcal{L}^*$ (i.e., sequences of labels) and define the set of reachable states in A from q as

$$ \mathcal{R}(A, q) = \{ p \mid \text{there is } \pi \in \mathcal{L}^* \text{ such that } q \xrightarrow{\pi} p \} $$

The set of reachable states in A is $\mathcal{R}(A) = \mathcal{R}(A, q_0)$. For succinctness, $q \xrightarrow{\lambda} q' \in A$ means that the transition belongs to (the set of transitions of) A; likewise, $q \in A$ means that $q$ belongs to the states of A. We say that $q \xrightarrow{\lambda} q'$ is an outgoing (resp. incoming) transition of $q$ (resp. $q'$). Since we use FSAs to formalise communicating systems, accepting states are disregarded (as also done in [11]).

We now define systems of CFSMs, by adapting the definitions in [11] to our context. Let $\mathfrak{P}$ be a set of participants (or roles, ranged over by A, B, etc.) and $\mathcal{M}$ a set of messages (ranged over by m, n, etc.). We take $\mathfrak{P}$ and $\mathcal{M}$ disjoint. An output label is written as $AB!m$ and represents the willingness of A to send message m to B; likewise, an input label is written as $AB?m$ and represents the willingness of B to receive message m from A. The subjects of an output label $AB!m$ and of an input label $AB?m$ are A and B, respectively.

**Definition 2.1 (CFSMs).** A communicating finite-state machine (CFSM) is an FSA M with labels in the set $\mathcal{L}_{act} \cup \{\tau\}$, where

$$ \mathcal{L}_{act} = \{AB!m, AB?m \mid A \neq B \in \mathfrak{P}, m \in \mathcal{M}\} $$

and, for any transition $p \xrightarrow{\lambda} q$,
* if $\lambda$ is an output label then $p \neq q$ and $p$ has exactly one incoming transition, and such transition is labelled by $\tau$;

* if $\lambda = \tau$ then $p \neq q$ and $q$ has exactly one outgoing transition, and such transition is labelled by an output label.

A state of M is

* terminal, if it has no outgoing transition; we define $T(M) = \{p \in M | p \text{ is terminal in } M\}$

* sending, if it is not terminal and all its outgoing transitions have output labels

* receiving, if it is not terminal and all its outgoing transitions have input labels

* mixed, if it has a silent outgoing transition and an outgoing transition with an input label.

A CFSM is A-local if all its non $\tau$ transitions have subject A.

Unlike in [5], the transitions of our CFSMs can also be labelled by the silent action $\tau$. Definition 2.1 can be looked at as the CFSM counterpart of the $\tau C$ contracts described in [6]. Imposing the no-mixed state condition on our CFSM, turns them into the communicating automata counterpart of the processes (contracts) called “session behaviours”<fnref n="1" /> in e.g., [10, 1, 7]. These processes are in turn the process counterpart of (binary) session types [13]. As we shall see below (and also shown in [3] and [5]), the absence of mixed states is necessary in order to get the preservation of properties by composition. As a matter of fact, we could drop the conditions related to $\tau$-transitions in case a transition like $p \xrightarrow{XY!z} q$ is the only outgoing transition from $p$, namely when no actual choice of output actions is possible in $p$. We however prefer to avoid this distinction for several reasons:

* firstly, our uniform treatment of transitions allows us to immediately adapt definitions in a more abstract setting;

* secondly, uniformity allows us to simplify some technicalities.

Said that, all proofs in the present paper could easily be adapted to the above mentioned alternative definition of CFSM.

**Definition 2.2 (Communicating systems).** A (communicating) system over $\mathcal{P}$ is a map $S = (M_A)_{A \in \mathcal{P}}$ assigning an A-local CFSM $M_A$ to each participant $A \in \mathcal{P}$ where $\mathcal{P} \subseteq \mathfrak{P}$ is finite and any participant occurring in a transition of $M_A$ is in $\mathcal{P}$.

Note that Definition 2.2 requires that any input or output label does refer to participants belonging to the system itself. In other words, Definition 2.2 restricts to closed systems.

We now define the synchronous semantics of communicating systems, which is itself an FSA (differently from the asynchronous case, where the set of states can be infinite). Hereafter, we write $f[x \mapsto y]$ for the update of the function $f$ in a point $x$ of its domain with the value $y$. Also, $\text{dom}(f)$ denotes the domain of the function $f$.

**Definition 2.3 (Asymmetric synchronisations).** Let $S$ be a communicating system. A configuration of $S$ is a map $s = (q_A)_{A \in \text{dom}(S)}$ assigning a local state $q_A \in S(A)$ to each $A \in \text{dom}(S)$.

The asymmetric synchronisations of $S$ is the FSA

$$[S] = \langle \mathcal{S}, s_0, \mathcal{L}_{\text{int}} \cup \{\tau\}, \rightarrow \rangle \quad \text{where}$$

* $\mathcal{S}$ is the set of synchronous configurations of $S$, as defined above;

<footnote n="1">¹Actually different variations of this name are used in the listed references.</footnote>
* $s_0 = (q_{0A})_{A \in \text{dom}(S)} \in \mathcal{S}$ is the initial configuration where, for each $A \in \text{dom}(S)$, $q_{0A}$ is the initial state of $S(A)$;

* $\mathcal{L}_{\text{int}} = \{A \to B: m \mid A \neq B \in \mathfrak{P} \text{ and } m \in \mathcal{M}\}$ is a set of interaction labels;

* $s \xrightarrow{A \to B: m} s[A \mapsto q, B \mapsto q'] \in [\mathbb{S}]$ if $s(A) \xrightarrow{AB!m} q \in S(A)$ and $s(B) \xrightarrow{AB?m} q' \in S(B)$;

* $s \xrightarrow{\tau} s[A \mapsto q] \in [\mathbb{S}]$ if $s(A) \xrightarrow{\tau} q \in S(A)$;

Configuration $s$ enables $A$ in $S$ if $s(A)$ has at least an outgoing transition.

As expected, an interaction $A \to B: m$ occurs when $A$ performs an output $AB!m$ (which has been previously chosen) and $B$ the corresponding input $AB?m$.

**Example 2.4.** Let us consider the communicating system $S = (M_X)_{X \in \{K,C,D,E\}}$, where

<figure><img src="image_2.png" /></figure>

A sequence of transitions of $[\mathbb{S}]$ out of $s_0$ is, according to Definition 2.3,

$$s_0 = (0_K, 0_C, 0_D, 0_E) \xrightarrow{\tau} (1_K, 0_C, 0_D, 0_E) \xrightarrow{K \to C: m} (3_K, 1_C, 0_D, 0_E) \\ \xrightarrow{\tau} (3_K, 2_C, 0_D, 0_E) \xrightarrow{C \to E: c} (3_K, 3_C, 0_D, 4_E) \\ \xrightarrow{\tau} (3_K, 3_C, 0_D, 5_E) \xrightarrow{E \to D: s} (3_K, 3_C, 3_D, 3_E)$$

◇

The symmetric synchronisation in [5] for systems without $\tau$-transitions can be readily obtained from the above definition by disregarding the clause for the $\tau$-transitions.

In the following, $ptp(\tau) = \emptyset$ and $ptp(A \to B: m) = ptp(AB!m) = ptp(AB?m) = \{A, B\}$ and, for a sequence $\pi = \lambda_1 \cdots \lambda_n$, we let $ptp(\pi) = \bigcup_{1 \le i \le n} ptp(\lambda_i)$.

As discussed in Section 1, we shall study the preservation of communication properties under composition. We shall consider the following relevant properties: deadlock freedom, lock freedom and strong lock freedom. The definitions below adapt the ones in [12] to a synchronous setting (as done also in [15, 18, 5]).

**Definition 2.5 (Communication properties).** Let $S$ be a communicating system on $\mathcal{P}$. We say that a participant $A \in \mathcal{P}$ is involved in a run $s \xrightarrow{\lambda_1} s_1 \dots \xrightarrow{\lambda_n} s_n$ of $S$ if there is $1 \le i \le n$ such that either $A \in ptp(\lambda_i)$ or $\lambda_i = \tau$, $s_i(A) \xrightarrow{\tau} q$ in $S(A)$, and $s_{i+1} = s_i[A \mapsto q]$.

**Deadlock freedom** A configuration $s \in \mathcal{R}([\mathbb{S}])$ is a deadlock if

* $s$ has no outgoing transitions in $[\mathbb{S}]$ and

* there exists $A \in \mathcal{P}$ such that $s(A)$ enables $A$ in $S$.

A system is deadlock-free if none of its configurations is a deadlock.

**Lock freedom** Let $A \in \mathcal{P}$. A configuration $s \in \mathcal{R}([\mathbb{S}])$ is a lock for $A$ if
* s(A) has outgoing transitions; and

* A is not involved in any run from s.

A system is lock-free if none of its configurations is a lock for any of its participants.

**Strong lock freedom** System S is strongly lock-free for A ∈ P if for each s ∈ R([S]) enabling A in S then A is involved in all maximal sequences from s.

A system is strongly lock free if it is strongly lock free for each of its participants.

**Proposition 2.6.** 1. Lock-freedom implies deadlock-freedom;

2. Strong lock freedom implies lock freedom.

**Example 2.7.** Let us consider the system S of Example 2.4. The only other maximal transition sequence in [S] out of s₀, besides the one described in Example 2.4, is

$$s_0 = (0_K, 0_C, 0_D, 0_E) \xrightarrow{\tau} (2_K, 0_C, 0_D, 0_E) \xrightarrow{\substack{K \to D: n \\ D \to E: d}} (3_K, 0_C, 1_D, 0_E) \\ \xrightarrow{\tau} (3_K, 0_C, 2_D, 0_E) \xrightarrow{\substack{K \to D: n \\ D \to E: d}} (3_K, 0_C, 3_D, 1_E) \\ \xrightarrow{\tau} (3_K, 0_C, 3_D, 2_E) \xrightarrow{\substack{K \to D: n \\ D \to E: d}} (3_K, 3_C, 3_D, 3_E)$$

These two sequences are both maximal and contain all the elements of R([S]). By the above observations it is possible to check S to be strongly lock free. ◇

# 3 Composition via Gateways

This section discusses composition of systems of CFSMs via gateways, as introduced in [2, 3], and studies its properties under asymmetric synchronisation. The main idea is that two systems of CFSMs, say S₁ and S₂, can be composed by transforming one participant in each of them into gateways connected to each other.

## 3.1 Building gateways

Let us call H the selected participant in S₁ and K the one in S₂. The gateways for H and K are connected to each other and act as forwarders: each message sent to the gateway for H by a participant from the original system S₁ is now forwarded to the gateway for K, that in turn forwards it to the same participant to which K sent it in the original system S₂. The dual will happen to messages that the gateway for K receives from S₂. A main advantage of this approach is that no extension of the CFSM model is needed to transform systems of CFSMs, which are normally closed systems, into open systems that can be composed. Another advantage is that the composition is fully transparent to all participants different from H and K.

We will now define composition via gateways on systems of CFSMs, following the intuition above.

**Definition 3.1 (Gateway).** Given a H-local CFSM M and a participant K, the gateway of M towards K is the CFSM gw(M, K) obtained by replacing in M

$$\bullet \text{ each pair of consecutive transitions } p \xrightarrow{\tau} q \xrightarrow{HA!m} r \text{ with} \\ p \xrightarrow{KH?m} p' \xrightarrow{\tau} q \xrightarrow{HA!m} r \quad \text{for some fresh state } p' \quad (6)$$

$$\bullet \text{ each transition } p \xrightarrow{AH?m} r \text{ with} \\ p \xrightarrow{AH?m} p' \xrightarrow{\tau} p'' \xrightarrow{HK!m} r \quad \text{for some fresh states } p' \text{ and } p'' \quad (7)$$
We shall call external the states like p and r and internal the states like p', p'' and q.

Note that gateways execute “segments” of the form described in (6) and (7) in the above definition. Also, by very construction, we have the following

**Fact 3.2.** Given a H-local CFSM M and a participant K, each state of gw(M, K) has at most one incoming or outgoing τ transition.

We compose systems with disjoint participants through two of them, say H and K, by taking all the participants of the original systems but H and K, whereas H and K are replaced by their respective gateways.

Given two functions f and g such that dom(f) ∩ dom(g) = θ, we let f + g denote the function behaving as function f on dom(f) and as function g on dom(g).

**Definition 3.3 (System composition).** Let S₁ and S₂ be two systems with disjoint domains. The composition of S₁ and S₂ via H ∈ dom(S₁) and K ∈ dom(S₂) is defined as

$$S_1^{H \to K} S_2 = S_1[H \mapsto gw(S_1(H), K)] + S_2[K \mapsto gw(S_2(K), H)]$$

(Note that dom(S₁$^{H \to K}$S₂) = dom(S₁) ∪ dom(S₂).)

We remark again that, by the above approach for composition, we do not actually need to formalise the notion of open system. In fact any closed system can be looked at as open by choosing (according to the current needs) two suitable participants in the “to-be-connected” systems and transforming them into two forwarders.

We also note that the notion of composition above is structural: a corresponding notion of behavioural composition has been studied in [4] in a context of multiparty session types [14], that is with symmetric synchronous interactions.

**Example 3.4.** Let us take the following two communicating systems.

<figure><img src="image_3.png" /></figure>
The system $S_1^{H \leftrightarrow K} S_2$ is

<figure><img src="image_4.png" /></figure>

Note that the CFSMs A, B, C, D, and E remain unchanged.

<figure><img src="image_5.png" /></figure>

## 3.2 Compatibility

A few simple auxiliary notions are useful. Let $\mathcal{L}_{i/o} = \{ ?m, !m \mid m \in \mathcal{M} \}$ and define the functions

$$ \text{io} : \mathcal{L}_{\text{act}} \to \mathcal{L}_{i/o} \quad \text{and} \quad (\overline{\cdot}) : \mathcal{L}_{i/o} \to \mathcal{L}_{i/o} $$

by the following clauses

$$ \text{io}(AB?m) = ?m \quad \text{io}(AB!m) = !m \quad \text{and} \quad \overline{?m} = !m \quad \overline{!m} = ?m $$

which extend to CFSMs in the obvious way: given a CFSM $M = (\mathcal{S}, q_0, \mathcal{L}_{\text{act}}, \to)$, we define $\text{io}(M) = (\mathcal{S}, q_0, \mathcal{L}_{i/o}, \to')$ where $\to' = \{ q \xrightarrow{\text{io}(\lambda)} q' \mid q \xrightarrow{\lambda} q' \in M, \lambda \in \mathcal{L}_{\text{act}} \} \cup \{ q \xrightarrow{\tau} q' \mid q \xrightarrow{\tau} q' \in M \}$ and likewise for $\overline{M}$.

Informally, two CFSMs $M_1$ and $M_2$ are compatible if each output of $M_1$ has a corresponding input in $M_2$ and vice versa once the identities of communicating partners are blurred away.

**Definition 3.5 (Compatibility).** Let $M$ and $M'$ be two FSAs on $\mathcal{L}_{i/o}$. An io-correspondence is a relation $R$ between states of $M$ and those of $M'$ such that whenever $(q, q') \in R$:

* $q \in \mathcal{T}(M)$ if, and only if, $q' \in \mathcal{T}(M')$ (cf. Definition 2.1)

* if $q \xrightarrow{!m} r \in M$ then there is $q' \xrightarrow{?m} r' \in M'$ such that $(r, r') \in R$

* if $q' \xrightarrow{!m} r' \in M'$ then there is $q \xrightarrow{?m} r \in M$ such that $(r, r') \in R$

* if $q \xrightarrow{\tau} r \in M$ then $(r, q') \in R$

* if $q' \xrightarrow{\tau} r' \in M'$ then $(q, r') \in R$

Two CFSMs $M$ and $M'$ are compatible (in symbols $M \asymp M'$) if there is an io-correspondence relating the initial states of $\text{io}(M_1)$ and $\text{io}(M')$.
**Example 3.6 (Compatibility).** The machines *H* and *K* of Example 3.4 are compatible. For a more complex example, consider the following *CFSMs*

<figure><img src="image_6.png" /></figure>

The above *H* and *K* are compatible. Apart for $\tau$ actions preceding them, *H* can only perform output actions, whereas *K* can only perform input actions. By disregarding the names of the receivers in the actions of *H*, and of the senders in those of *K*, any output action after its corresponding $\tau$ can find a matching input in *K*. The vice versa does not hold, since none of the possible output actions that can occur after a $\tau$ from 0 (i.e. the outputs from 1 and 7 in *H*) can actually match the input action $EK?z$ from 0 in *K*. Such a possibility is in fact allowed by our definition of compatibility. ◇

Definition 3.5 transfers the notion of compatibility given in [4] for processes in multiparty sessions. Also, Definition 3.5 differs from the notions of compatibility in [5] and in [2, 3] which are defined as bisimulations and do not involve $\tau$-transitions.

**Definition 3.7.** An *A*-local *CFSM M* is:

1. ?-deterministic if $p \xrightarrow{XA?m} q$ and $p \xrightarrow{YA?m} r \in M$ implies $q = r$;

2. !-deterministic if $p \xrightarrow{\tau \quad AX!m} q$ and $p \xrightarrow{\tau \quad YA!m} r \in M$ implies $q = r$;

3. ?!-deterministic if it is both ?-deterministic and !-deterministic;

A non-terminal state $q \in M$ is asymmetric sending (resp. receiving) if all its outgoing transitions have $\tau$ (resp. receiving) labels; $q$ is a asymmetric mixed state if it is neither asymmetric sending nor receiving.

**Example 3.8.** Machine *H* and *K* in Example 3.6 are, respectively non !-deterministic and non ?-deterministic. In particular, conditions (2) and (1) of Definition 3.7 fail for, respectively, state 0 of *H* and state 0 of *K*.

We require a stronger condition than compatibility for two systems to be composable.

**Definition 3.9 ((H, K)-composability).** Two systems $S_1$ and $S_2$ with disjoint domains are (H, K)-composable if $H \in \text{dom}(S_1)$ and $K \in \text{dom}(S_2)$ are two compatible ?-deterministic machines with no asymmetric mixed states.

# 4 Composition Related Issues

It is known that under symmetric synchronisation composition spoils deadlock-freedom; this is shown by the example below, borrowed from [5].

**Example 4.1 (Deadlock-freedom preservation fails under symmetric synchronisation).** Take the following systems

<figure><img src="image_7.png" /></figure>
**Example 4.3** (Asymmetric mixed-states spoil deadlock freedom preservation). Let $S_1$ and $S_2$ be

<figure><img src="image_8.png" /></figure>

Notice that the initial states are asymmetric mixed and that $H$ and $K$ are compatible. The gateways we obtain are

<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /></figure>

The composed system $S_1 \overset{H \leftrightarrow K}{\rightleftharpoons} S_2$ deadlocks when $gw(S_1(H), K)$ receives from $B$ while $gw(S_2(K), H)$ receives from $D$ since both gateways reach an output state (respectively states 10 and 7). ◇

The following examples show that, as asymmetric mixed states, !?-nondeterminism is problematic too. Let us first take two deadlock free systems.
<figure><img src="image_11.png" /><figcaption>**Example 4.4.** The two systems</figcaption></figure>

are deadlock free.

The deadlock freedom of $S_1$ follows from the fact that, from its initial configuration $(0_A, 0_B, 0_C, 0_H)$, $S_1$ can only branch over the two $\tau$-transitions of $H$ reaching either of the following configurations

$$ (0_A, 0_B, 0_C, 7_H) \quad \text{or} \quad (0_A, 0_B, 0_C, 1_H) $$

From the former (resp. latter) configuration $S_1$ can only reach configurations where $H$ synchronises with $C$ and then with $A$ (resp. $B$). In either case $S_1$ reaches the terminal configuration $(1_A, 1_B, 1_C, 6_H)$.

Let us now have a look at $S_2$. Firstly note that $E$ cannot synchronise since it is already terminated; hence, the only possible transitions of $S_2$ must involve $K$ and $D$ only. We therefore have that

$$ \begin{array}{ccc} (0_K, 0_D, 0_E) \xrightarrow{\tau} & (0_K, 1_D, 0_E) \xrightarrow{D \to K: m} & (1_K, 2_D, 0_E) \xrightarrow{\tau} (1_K, 3_D, 0_E) \xrightarrow{D \to K: x} & (2_K, 4_D, 0_E) \\ \xrightarrow{\tau} & (2_K, 5_D, 0_E) \xrightarrow{D \to K: m} & & (3_K, 6_D, 0_E) \end{array} $$

is the only possible execution from the initial configuration $(0_K, 0_D, 0_E)$ of $S_2$, leading to the terminal configuration $(3_K, 6_D, 0_E)$.

<figure><img src="image_12.png" /></figure>

The next example shows that the compositions of the systems $S_1$ and $S_2$ in Example 4.4 can deadlock.

**Example 4.5** (?!-determinism is necessary). The CFSMs $H$ and $K$ in Example 4.4 are compatible as seen
in Example 3.6. Hence, we can build the composed system $S_1 \overset{H \leftrightarrow K}{\to} S_2$ through the gateways

<figure><img src="image_13.png" /></figure>

Now, from the initial configuration $s_0 = (0_A, 0_B, 0_C, 0_{gw}(M_H, K), 0_{gw}(M_K, H), 0_D, 0_E)$ of $S_1 \overset{H \leftrightarrow K}{\to} S_2$ we have the following run

$$ \begin{array}{rcl} s_0 & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 0_{gw}(M_H, K), 0_{gw}(M_K, H), 1_D, 0_E) \\ \xrightarrow{D \to K: m} & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 0_{gw}(M_H, K), 9_{gw}(M_K, H), 2_D, 0_E) \\ \xrightarrow{K \to H: m} & \xrightarrow{\tau} & (0_A, 0_B, 0_C, 13_{gw}(M_H, K), 1_{gw}(M_K, H), 3_D, 0_E) \end{array} \quad (8) $$

$$ \begin{array}{rcl} \xrightarrow{D \to K: \times} & (0_A, 0_B, 0_C, 13_{gw}(M_H, K), 14_{gw}(M_K, H), 4_D, 0_E) & \\ \xrightarrow{\tau} \xrightarrow{\tau} \xrightarrow{\tau} & (0_A, 0_B, 0_C, 1_{gw}(M_H, K), 15_{gw}(M_K, H), 5_D, 0_E) & \end{array} $$

$$ \xrightarrow{H \to A: m} (1_A, 0_B, 0_C, 2_{gw}(M_H, K), 15_{gw}(M_K, H), 5_D, 0_E) \quad (9) $$

where the $\tau$-transition of $D$ enables the synchronisation of $gw(M_K, H)$ and $D$ with label $D \to K: m$ that leads the gateway in state 9 after its $\tau$-transition from state 8. Now, the two gateways can communicate and exchange message $m$. Due to $?!-nondeterminism$ of $S_1$, from state 0 $gw(M_H, K)$ can move either to state 12 or to state 13. Fatally, transition (8) leads to a deadlock: after $gw(M_K, H)$ and $D$ synchronise to exchange message $\times$ the system goes into a configuration from where $gw(M_H, K)$ forwards $m$ to $A$ and reaches the last configuration (9). This is a deadlock for $S_1 \overset{H \leftrightarrow K}{\to} S_2$, since none of the CFSMs can do a $\tau$-transitions, the only enabled output action is from $gw(M_K, H)$ which tries to send message $\times$ to $gw(M_H, K)$; however, $gw(M_H, K)$ can only receive message $\gamma$ from $K$ and hence these actions cannot synchronise. $\diamond$

# 5 Preserving Properties by Composition

Composition via gateways does not ensure the preservation of communication properties. We provide below sufficient conditions for this to happen. Recall that $(H, K)$-composability requires absence of asymmetric mixed states and $?!-determinism.

**Theorem 5.1** (Deadlock freedom preservation). Let $S_1$ and $S_2$ be two $(H, K)$-composable and deadlock-free systems. Then the composed system $S_1 \overset{H \leftrightarrow K}{\to} S_2$ is deadlock-free.
**Proof sketch.** The proof relies on the fact that the reachable configurations of $S_1 \overset{H \to K}{\to} S_2$ can be projected on reachable configurations of $S_1$ and $S_2$. This implies that a deadlock in $S_1 \overset{H \to K}{\to} S_2$ corresponds to a deadlock in $S_1$ or in $S_2$. See the appendix for the detailed proof. □

**Example 5.2.** We can infer deadlock-freedom of the system $S = S_1 \overset{H \to K}{\to} S_2$ of Example 3.4 by the result above, since $S_1$ and $S_1$ are $(H, K)$-composable and deadlock-free.

Somehow surprisingly, in the symmetric case preservation of deadlock freedom requires stricter conditions on gateways than in the asymmetric case. In fact, in the asymmetric case, deadlock freedom preservation requires only absence of asymmetric mixed states and ?!-determinism while the symmetric case requires the (stronger) condition of sequentiality.

**Definition 5.3 (Sequential CFSM).** A CFSM is sequential if each of its states has at most one outgoing transition. A participant A of a system S is sequential if $S(A)$ is so.

As we will see (cf. Theorem 5.5), sequentiality is necessary to preserve lock-freedom also in the asymmetric case. We note that sequentiality implies absence of asymmetric mixed states and ?!-determinism, while the converse does not hold.

As mentioned before, the property of lock freedom is not preserved in general by composition, as shown by the following example.

**Example 5.4 (Composability does not preserve lock-freedom).** Take the communicating systems

<figure><img src="image_14.png" /></figure>

Note that both $S_1$ and $S_2$ are lock-free and that H and K are compatible. The gateways are

<figure><img src="image_15.png" /></figure>

Hence, the composed system $S_1 \overset{H \to K}{\to} S_2$ is non lock-free because e.g. the configuration

$$s = (0_A, 0_{gw(M_H, K)}, 0_{gw(M_K, H)}, 0_B, 0_C)$$

is a lock for B, since the only outgoing transition from $0_B$ could be fired only in case the transition CB!stop is enabled. However, this is impossible since $gw(M_H, K)$ forwards only message m; hence, the run (which does not involve B)

$$s \xrightarrow{\tau} \underset{A \to H: m}{\overline{\hspace{1.5cm}}} (0_A, 2_{gw(M_H, K)}, 0_{gw(M_K, H)}, 0_B, 0_C) \xrightarrow{\tau} \underset{A \to H: m}{\overline{\hspace{1.5cm}}} s \dots$$

is perpetually executed.

<figure><img src="image_16.png" /></figure>
We show that the problem of Example 5.4 cannot happen in case we restrict to sequential gateways, as done for deadlock freedom in the symmetric case (cf. [5]). As usual, $f|_X$ denotes the restriction of a function $f$ on a subset $X$ of its domain.

**Theorem 5.5 (Lock-freedom preservation).** Let $S_1$ and $S_2$ be two (H, K)-composable and lock-free systems with H and K sequential. Then the composed system $S_1^{H→K}S_2$ is lock-free.

*Proof sketch.* The proof goes as the one of Theorem 5.1 noticing that we have to reconstruct “backward” the sequence of interactions. This exploits sequentiality and lock-freedom of $S_1$ and $S_2$ in order to guarantee the reconstruction when we “cross” the two composed systems through the gateways. ☐

We turn now our attention to strong lock-freedom. In this case, as for deadlock freedom, (H, K)-composability suffices for preservation by composition; we shall see that this is not the case for lock freedom preservation.

**Theorem 5.6 (Strong lock freedom preservation).** Let $S_1$ and $S_2$ be two (H, K)-composable and strongly lock free systems. Then the composed system $S_1^{H→K}S_2$ is strongly lock free.

*Proof sketch.* The proof is similar to the one of Theorem 5.5 but for the use of strong lock freedom of $S_1$ and $S_2$ instead of their deadlock freedom. ☐

# 6 Conclusions and Future Work

We introduce an asymmetric synchronous semantics of communicating systems which breaks the symmetry between senders and receivers. In fact, our semantics decouples communication from choice resolution as in standard semantics of communicating systems (and other models). We then adapted the gateway composition mechanism defined in [2, 3] to our asymmetric semantics and gave conditions for the preservation of some communication properties under this notion of composition.

An approach related to ours is the framework of [8, 9] based on *contract automata* where transitions express “requests” and “offers” among participants. The composition mechanism is based on “trimming” a product of contract automata according to relevant *agreement* properties. This yields controllers that preserve deadlocks. Contract automata do not consider asymmetric synchronous semantics. Our composition mechanism does not introduce orchestrators which, under some conditions, can be avoided also for contract automata [8, 9].

Modular approaches to the development of concurrent systems can be exploited even for systems designed using formalisms intrinsically dealing with *closed* systems. Indeed, given two systems, any two components – one per system – exhibiting *compatible* behaviours can be replaced by two coupled forwarders (gateways) connecting the systems, as investigated initially in [2, 3] for an asynchronous interaction model. The investigation on the composition-by-gateways technique was shifted in [5] towards synchronous symmetric interactions. In the present paper we pushed a step forward such an investigation, by considering *asymmetric* synchronous interactions. Interestingly, deadlock freedom preservation in the synchronous asymmetric case we consider does not require sequentiality of gateways, like in the asynchronous case, and differently from the synchronous symmetric case. Notably, sequentiality is needed here for lock-freedom preservation, but not for strong-lock freedom preservation.

While the path of investigation above is quite homogeneous, the different analyses present some methodological differences. For instance, [5] considers also another form of composition, where one single gateway (interacting with both the composed systems) is used. On the other side, [5] focused only
on deadlocks, disregarding other properties we consider. A first item of future research consist in filling
the bits missing due to the mismatches above.

A more challenging direction for future work is looking for refined composition mechanisms in order
to get preservation of relevant properties under weaker conditions.

References

[1] F. Barbanera and U. de'Liguoro. Sub-behaviour relations for session-based client/server systems. *MSCS*, 25(6):1339-1381, 2015.

[2] F. Barbanera, U. de'Liguoro, and R. Hennicker. Global types for open systems. In M. Bartoletti and S. Knight, editors, *ICE*, volume 279 of *EPTCS*, pages 4–20, 2018.

[3] F. Barbanera, U. de'Liguoro, and R. Hennicker. Connecting open systems of communicating finite state machines. *JLAMP*, 109, 2019.

[4] F. Barbanera, M. Dezani-Ciancaglini, I. Lanese, and E. Tuosto. Composition and decomposition of multiparty sessions. *JLAMP*, 2020. Submitted.

[5] F. Barbanera, I. Lanese, and E. Tuosto. Composing communicating systems, synchronously. In T. Margaria and B. Steffen, editors, *ISoLA 2020*, volume 12476 of LNCS, pages 39–59. Springer, 2020.

[6] M. Bartoletti, T. Cimoli, and R. Zunino. Compliance in behavioural contracts: A brief survey. In C. Bodei, G. L. Ferrari, and C. Priami, editors, *Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday*, volume 9465 of *Lecture Notes in Computer Science*, pages 103–121. Springer, 2015.

[7] M. Bartoletti, A. Scalas, and R. Zunino. A semantic deconstruction of session types. In P. Baldan and D. Gorla, editors, *CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings*, volume 8704 of *Lecture Notes in Computer Science*, pages 402–418. Springer, 2014.

[8] D. Basile, P. Degano, G. L. Ferrari, and E. Tuosto. Playing with our CAT and communication-centric applications. In E. Albert and I. Lanese, editors, *FORTE*, volume 9688 of LNCS, pages 62–73. Springer, 2016.

[9] D. Basile, M. H. ter Beek, and R. Pugliese. Synthesis of orchestrations and choreographies: Bridging the gap between supervisory control and coordination of services. *LMCS*, 16(2), 2020.

[10] G. Bernardi and M. Hennessy. Modelling session types using contracts. In *Proceedings of the 27th Annual ACM Symposium on Applied Computing*, SAC '12, pages 1941–1946, New York, NY, USA, 2012. ACM.

[11] D. Brand and P. Zafiropulo. On communicating finite-state machines. *J. ACM*, 30(2):323–342, 1983.

[12] G. Cécé and A. Finkel. Verification of programs with half-duplex communication. *I&C*, 202(2):166–190, 2005.

[13] K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type disciplines for structured communication-based programming. In *ESOP*, volume 1381 of LNCS, pages 22–138. Springer, 1998.

[14] H. Hüttel et al. Foundations of session types and behavioural contracts. *ACM Comput. Surv.*, 49(1):3:1–3:36, 2016.

[15] J. Lange, E. Tuosto, and N. Yoshida. From communicating machines to graphical choreographies. In *POPL*, pages 221–232. ACM, 2015.

[16] R. Milner. *A Calculus of Communicating Systems*, volume 92 of LNCS. Springer, Berlin, 1980.

[17] L. Padovani. Contract-based discovery of web services modulo simple orchestrators. *Theoretical Computer Science*, 411:3328–3347, 2010.

[18] E. Tuosto and R. Guanciale. Semantics of global view of choreographies. *JLAMP*, 95:17–40, 2018.
A Proofs for Section 3 (Composition via Gateways)

Given a configuration of the composition of systems S<sub>1</sub> and S<sub>2</sub> we can retrieve the configurations of the two subsystems by taking only the states of participants in S<sub>1</sub> and S<sub>2</sub> while avoiding, for the gateways, to take the fresh states introduced by the gateway construction. Indeed, we shall prove in Proposition B.3 that for each s ∈ ℛ([S]), we have H]s ∈ ℛ([S<sub>1</sub>]) and s|<sub>K</sub> ∈ ℛ([S<sub>2</sub>]).

**Definition A.1 (Configuration projections).** Let s be a configuration of a composed system S<sub>1</sub>H↔KS<sub>2</sub> and M = gw(S<sub>1</sub>(H), K). The left-projection of s on S<sub>1</sub> is the map H]s defined on dom(S<sub>1</sub>) by

$$
H]s : A \mapsto \begin{cases}
q, & \text{if } s(A) \notin S_1(A) \text{ and there is } q \xrightarrow{KH^?m} s(A) \in M \text{ or } q \xrightarrow{KH^?m} \tau \xrightarrow{H} s(A) \in M \\
r, & \text{if } s(A) \notin S_1(A) \text{ and there is } s(A) \xrightarrow{HK!m} r \in M \text{ or } s(A) \xrightarrow{H} r \in M \\
s(A), & \text{otherwise}
\end{cases}
$$

The definition of right-projection s|_K is analogous.

**Proposition A.2.** Left- and right-projections are well-defined.

Proof. It is enough to show that H]· and ·|_K uniquely assign a state to fresh states because on non-fresh stats both functions act as the identify map. This follows since, by construction, each state introduced by our gateway construction has unique successor and predecessor. □

Intuitively, only **H** is aware of an input from **K** when **H** is in the internal state reached after an input from **K**; hence to have a coherent configuration we take the state of **H** before the input. If instead **H** is in an internal state corresponding to an output to **K**, then other participants in S<sub>1</sub> know that the message has been sent; hence to have a coherent configuration we take the state of **H** after the send. (A similar intuition applies to s|<sub>K</sub>.)

**Example A.3.** Let $s = (2_A, 0_B, 1_H, 5_K, 0_C, 0_D, 0_E)$; and $S = S_1^{H \leftrightarrow K} S_2$ be the system of Example 3.4. Then, $s \in \mathcal{R}([S])$, namely $s$ is reachable in $S$. In fact

$$
\begin{align*}
s_0 = (0_A, 0_B, 0_H, 0_K, 0_C, 0_D, 0_E) &\xrightarrow{\tau} (1_A, 0_B, 0_H, 0_K, 0_C, 0_D, 0_E) \\
&\xrightarrow{A \to H: m} (2_A, 0_B, 2_H, 0_K, 0_C, 0_D, 0_E) \\
&\xrightarrow{\tau} (2_A, 0_B, 4_H, 0_K, 0_C, 0_D, 0_E) \\
&\xrightarrow{H \to K: m} (2_A, 0_B, 1_H, 5_K, 0_C, 0_D, 0_E)
\end{align*}
$$

The projections of s on, respectively, S<sub>1</sub> and S<sub>2</sub> are H]s = (2<sub>A</sub>, 0<sub>B</sub>, 1<sub>H</sub>) and s|<sub>K</sub> = (0<sub>K</sub>, 0<sub>C</sub>, 0<sub>D</sub>, 0<sub>E</sub>). ◇

B Proofs for Section 4 (Composition Related Issues)

Let M be an H-local CFSM and K ∈ 𝒫 \ {H} be a participant not occurring in M. Function nof maps the states of gw(M, K) to the states of M as follows:

$$
\mathrm{nof}_{H,K}(M, q) =
\begin{cases}
p, & \text{if } p \xrightarrow{\lambda} q \in \mathrm{gw}(M, K) \text{ and } \lambda \text{ input label with } K \notin \mathrm{ptp}(\lambda) \\
p, & \text{if } p \xrightarrow{\lambda} p' \xrightarrow{\tau} q \in \mathrm{gw}(M, K) \text{ and } \lambda \text{ input label with } K \in \mathrm{ptp}(\lambda) \\
r, & \text{if } q \xrightarrow{\lambda} r \in \mathrm{gw}(M, K) \text{ and } \lambda \text{ output label with } K \notin \mathrm{ptp}(\lambda) \\
r, & \text{if } q \xrightarrow{\tau} q' \xrightarrow{\lambda} r \in \mathrm{gw}(M, K) \text{ and } \lambda \text{ output label with } K \in \mathrm{ptp}(\lambda) \\
q, & \text{if } q \text{ is a state of } M
\end{cases}
$$
Note that the first four clause imply that $q$ is a fresh state of $gw(M, K)$.

**Lemma B.1.** *Function nof is well-defined.*

*Proof.* Let $M$ be an $H$-local CFSM and $K \in \mathcal{P} \setminus \{H\}$. We have to check only internal states as the restriction of nof to the states of $M$ is the identity by definition. If $q$ is an internal state of $gw(M, K)$, by definition of $gw(M, K)$, there is a unique $q'$ such that either $q' \xrightarrow{AH?m} q \in gw(M, K)$ or $q \xrightarrow{HA!m} q' \in gw(M, K)$. $\square$

**Example B.2.** For $S_1 \xrightarrow{H \to K} S_2$ of Example 3.4, $\text{nof}_{H,K}(S_1(H), 0) = 0$ and $\text{nof}_{K,H}(S_2(K), 2) = 0$. $\diamond$

Function nof is similar to configuration projection when considering CFSMs in isolation, with a main difference: when e.g., $gw(M, K)$ in state $q$ receives from a partner in its own system going to some fresh state $p'$ with a $\tau$-transition to $p''$, nof maps both $p'$ and $p''$ to $p$ (unlike configuration projection $H$]$_-$ which maps $q$ to the successor of $p''$). This represents the fact that the other system, and $K$ in particular, are oblivious of the transition. In fact, function nof is designed to establish a correspondence with the other system as shown by the next proposition.

**Proposition B.3.** Let $S = S_1 \xrightarrow{H \to K} S_2$ be the composition of two $(H, K)$-composable systems $S_1$ and $S_2$. If $s \in \mathcal{R}(\llbracket S \rrbracket)$ then $H \rfloor s \in \mathcal{R}(\llbracket S_1 \rrbracket)$, $s \lfloor_K \in \mathcal{R}(\llbracket S_2 \rrbracket)$, and $\text{nof}_{H,K}(S_1(H), s(H)) \asymp \text{nof}_{K,H}(S_2(K), s(K))$.

*Proof.* Let $s_0$ be the initial configuration of $S$ and

$$s_0 \xrightarrow{\lambda_1} s_1 \cdots s_{n-1} \xrightarrow{\lambda_n} s_n = s \qquad (10)$$

a run reaching $s$ from $s_0$. We proceed by induction on $n$.

If $n=0$ the thesis is immediate by observing that

* $H \rfloor s \in \mathcal{R}(\llbracket S_1 \rrbracket)$ and $s \lfloor_K \in \mathcal{R}(\llbracket S_2 \rrbracket)$ because left- and right-projections are the initial configurations of $S_1$ and $S_2$ respectively, and

* $\text{nof}_{H,K}(S_1(H), s(H))$ and $\text{nof}_{K,H}(S_2(K), s(K))$ are the initial states of $S_1(H)$ and $S_2(K)$ respectively which are compatible by hypothesis.

Let $n > 0$ and assume that the statement holds for all configurations reachable from $s_0$ in less the $n$ transitions. We have that either none of $H$ and $K$ are involved in $\lambda_n$ or that at least one of them is. In the former case, without loss of generality, assume that the interacting participants, say $A$ and $B$ are both in $S_1$. Then, by construction (cf. Definition A.1), $s \lfloor_K = s_{n-1} \lfloor_K$ and by inductive hypothesis $s_{n-1} \lfloor_K \in \mathcal{R}(\llbracket S_2 \rrbracket)$. Moreover, $H \rfloor s$ equals $H \rfloor s_{n-1}$ but for the local states of $A$ and $B$; hence $H \rfloor s_{n-1} \in \mathcal{R}(\llbracket S_1 \rrbracket)$ by the semantics of communicating systems (cf. Definition 2.3). Also,

$$\text{nof}_{H,K}(S_1(H), s(H)) = (H \rfloor s)(H) = (H \rfloor s_{n-1})(H) \asymp (s_{n-1} \lfloor_K)(K) = (s \lfloor_K)(K) = \text{nof}_{K,H}(S_2(K), s(K))$$

because the equalities above hold by the definition of asymmetric synchronisation (cf. Definition 2.3) and the compatibility relation holds by the inductive hypothesis. So, let us assume that at least one between $H$ and $K$ is involved in the last transition reaching $s$ and proceed by case analysis on $\lambda_n$.

$\lambda_n = \tau$ We consider only the case where $H$ is involved since the case where $K$ is involved is symmetric. By our gateway construction (cf. Definition 3.1) only one of the following two cases are possible for the transitions in $gw(S_1(H), K)$:

$$p \xrightarrow{KH?m} s_{n-1}(H) \xrightarrow{\tau} q \xrightarrow{HA!m} r \qquad (11)$$

$$q \xrightarrow{AH?m} s_{n-1}(H) \xrightarrow{\tau} p \xrightarrow{HK!m} r \qquad (12)$$
for some participant A of S<sub>1</sub> and states p, q, r of gw(S<sub>1</sub>(H), K). Cases (11) and (12) respectively correspond to have the transitions

$$p \xrightarrow{\tau} q \xrightarrow{HA!m} r \quad \text{and} \quad q \xrightarrow{AH?m} r$$

in the machine S<sub>1</sub>(H).

In case (11) the last transition in the run (10) must therefore be preceded by a transition, say the i-th one, where the machines gw(S<sub>1</sub>(H), K) and gw(S<sub>2</sub>(K), H) have exchanged message m. Hence, we have that gw(S<sub>2</sub>(K), H) has a transition $s_i(K) \xrightarrow{KH!m} s_{i+1}(K)$ with $s_{n-1}(H) \asymp s_{i+1}(K)$ since (by inductive hypothesis) $s_i(H) = p = \text{nof}_{H,K}(S_1(H), s_i(H)) \asymp \text{nof}_{K,H}(S_2(K), s_i(K))$ and both gateways are ?-deterministic. We now observe that either $s(K) = s_{i+1}(K)$ or it is a fresh state that gw(S<sub>2</sub>(K), H) reaches after having received a message from a participant of S<sub>2</sub> (possibly followed by a τ transition) between the i-th and the last interactions in (10). We have that $H \searrow s = H \searrow s_{n-1}[H \mapsto p]$, hence $H \searrow s \in \mathcal{R}(\llbracket S_1 \rrbracket)$ by inductive hypothesis; also, $s \llbracket K \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$ by the inductive hypothesis since $s \llbracket K \rrbracket = s_{n-1} \llbracket K \rrbracket$ because K is not involved in $\lambda_n$. Finally, in both cases the last part of the thesis immediately follows by observing that $\text{nof}_{K,H}(S_2(K), s(K)) = \text{nof}_{K,H}(S_2(K), s_i(K))$ by definition and $\text{nof}_{H,K}(S_1(H), s(H)) = p$.

In case (12), firstly note that by construction $A \neq H$ (cf. Definition 2.3). Then gw(S<sub>1</sub>(H), K) has the transition $s_{n-1}(H) \xrightarrow{AH?m} s(H)$ which corresponds to an input transition $s_{n-1}(H) \xrightarrow{AH?m} r$ where $r=H \searrow s(H) = \text{nof}_{H,K}(S_1(H), s_{n-1}(H)) = \text{nof}_{H,K}(S_1(H), s(H))$ in S<sub>1</sub>(H). Hence, the thesis follows since $s \llbracket K \rrbracket = s_{n-1} \llbracket K \rrbracket$ because K is not involved in $\lambda_n$ and $\text{nof}_{H,K}(S_1(H), s(H)) \asymp \text{nof}_{K,H}(S_2(K), s(K)) = \text{nof}_{K,H}(S_2(K), s_{n-1}(K))$ by inductive hypothesis.

$\lambda_n = H \to X: m$ By construction, either $X = K$ or $X \neq H$ is a participant of S<sub>1</sub>. In the former case, gw(S<sub>1</sub>(H), K) has the transition $s_{n-1}(H) \xrightarrow{HK!m} s(H)$ which corresponds to an input transition while gw(S<sub>2</sub>(K), H) has the transition $s_{n-1}(K) \xrightarrow{HK?m} s(K)$ which corresponds to a sequence of transitions $p \xrightarrow{\tau} s(K)$ in S<sub>2</sub>(K) for some participant $B \neq K$ in S<sub>2</sub>. Then the thesis follows by the fact that $H \searrow s = H \searrow s_{n-1}[H \mapsto s(H)]$ and $s \llbracket K \rrbracket = s_{n-1} \llbracket K \mapsto p \rrbracket$ by construction (cf. Definition A.1) and that, by inductive hypothesis, $\text{nof}_{H,K}(S_1(H), s_{n-1}(H)) = q \asymp s(K) = \text{nof}_{K,H}(S_2(K), s_{n-1}(K))$ and therefore, by ?-determinism and the compatibility relation $s(H) \asymp s(K)$.

Suppose now that X is a participant of S<sub>1</sub>; note that by construction $X \neq H$ (cf. Definition 2.3). Since $s \llbracket K \rrbracket = s_{n-1} \llbracket K \rrbracket$, the inductive hypothesis immediately entails that $s \llbracket K \rrbracket \in \mathcal{R}(\llbracket S_2 \rrbracket)$.

We first show the reachability of left- and right-projections. The transition $s_{n-1}(H) \xrightarrow{HX!m} s(H)$ is in gw(S<sub>1</sub>(H), K) by construction and it corresponds to a pair of transitions $p \xrightarrow{\tau} s_{n-1}(H) \xrightarrow{HX!m} s(H)$ in S<sub>1</sub>(H). We have that $H \searrow s_{n-1} \in \mathcal{R}(\llbracket S_1 \rrbracket)$ (by inductive hypothesis) and since $H \searrow s_{n-1}(H) = p$ (by Definition A.1) we have $H \searrow s_{n-1} \xrightarrow{\tau} H \xrightarrow{H \to X: m} H \searrow s$ (by Definition 2.3).

We now show the compatibility condition. The last transition in the run (10) must be preceded by a transition, say the i-th one, where the machines gw(S<sub>1</sub>(H), K) and gw(S<sub>2</sub>(K), H) have exchanged message m. Hence, we have that gw(S<sub>2</sub>(K), H) has a transition $s_i(K) \xrightarrow{KH!m} s_{i+1}(K)$ with

$$\text{nof}_{H,K}(S_1(H), s_{n-1}(H)) = s(H) = \text{nof}_{H,K}(S_1(H), s(H)) \quad (13)$$

which hold by definition of $\text{nof}(\cdot, \cdot)$. We now observe that either $s(K) = s_{i+1}(K)$ or it is a fresh state that gw(S<sub>2</sub>(K), H) reaches after having received a message from a participant of S<sub>2</sub> (possibly
followed by a $\tau$ transition) between the $i$-th and the last interactions in (10). In both cases the $\text{nof}_{K,H}(S_2(K), s(K)) = \text{nof}_{K,H}(S_2(K), s_{n-1}(K))$ and, by inductive hypothesis,

$$ \text{nof}_{K,H}(S_2(K), s_{n-1}(K)) \asymp \text{nof}_{H,K}(S_1(H), s_{n-1}(H)) $$

hence, by equalities (13), $\text{nof}_{H,K}(S_1(H), s(H)) \asymp \text{nof}_{K,H}(S_2(K), s(K))$.

$\lambda_n = X \to H: m$ The case $X = K$ is symmetric to the previous case with $\lambda_n = H \to K: m$ and therefore omitted. So, assume that $X$ is a participant of $S_1$; note that by construction $X \neq H$ (cf. Definition 2.3). Then $\text{gw}(S_1(H), K)$ has the transition $s_{n-1}(H) \xrightarrow{XH?m} s(H)$ which corresponds to an input transition $s_{n-1}(H) \xrightarrow{XH?m} r$. We have that $H \rfloor s_{n-1} \in \text{RS}[[S_1]]$ by inductive hypothesis, and so is $H \rfloor s_{n-1} \xrightarrow{X \to H: m} H \rfloor s$ since, by definition of left-projection, $H \rfloor s(H) = r$. The reachability of the right-projection of $s$ immediately follows by inductive hypothesis, since $s \lfloor_K = s_{n-1} \lfloor_K$.

We now show the compatibility condition. By definition, we have that $\text{nof}_{H,K}(S_1(H), s(H)) = \text{nof}_{H,K}(S_1(H), s_{n-1}(H))$. Moreover, we necessarily have that $s(K) = s_{n-1}(K)$. Hence by inductive hypothesis,

$$ \text{nof}_{H,K}(S_1(H), s(H)) = \text{nof}_{H,K}(S_1(H), s_{n-1}(H)) \asymp \text{nof}_{K,H}(S_2(K), s_{n-1}(K)) = \text{nof}_{K,H}(S_2(K), s(K)) $$

The cases $\lambda_n = X \to K: m$ and $\lambda_n = K \to X: m$ are similar to the last two cases above. $\square$

## C Proofs for Section 5 (Preserving Properties by Composition)

**Theorem 5.1 (Deadlock freedom preservation).** Let $S_1$ and $S_2$ be two $(H,K)$-composable and deadlock-free systems. Then the composed system $S_1^{H \leftrightarrow K} S_2$ is deadlock-free.

Given an $H$-local CFSM $M$ and a participant $K \in \mathcal{P} \setminus \{H\}$, call connecting a fresh asymmetric sending state of $\text{gw}(M, K)$ whose next outgoing transition does not have $K$ as receiver.

*Proof.* We show that if the composed system $S_1^{H \leftrightarrow K} S_2$ reaches a deadlock configuration $s$ then at least one of $H \rfloor s$ and $s \lfloor_K$ is a deadlock. Without loss of generality, we assume that the deadlock is the left-projection; the case where the deadlock is the right-projection is similar.

First, we show that if a participant $A$ from $S_1$ has an enabled transition in $s$ then some participant in $S_1$ has a transition enabled in $H \rfloor s$. Note that $H \rfloor s$ is reachable in $S_1$ by Proposition B.3.

If $A \neq H$ then any transition of $A$ enabled in $s$ is also enabled in $H \rfloor s$ since $H \rfloor s(A) = s(A)$ by Definition A.1. If $A = H$, then either of the following cases occurs

* $H$ has enabled an input

Assume that the input is from $K$. Then by construction $H \rfloor s(H)$ has a $\tau$-transition enabled in $S_1(H)$.

If the input of $H$ is from a participant $A$ of $S_1$ then by construction $H \rfloor s(H)$ has an input transition enabled in $S_1(H)$.

* $H$ has enabled an output.

Assume that the receiver of such output is $K$. Then $\text{nof}_{H,K}(S_1(H), s(H)) \asymp \text{nof}_{K,H}(S_2(K), s(K))$ by Proposition B.3. By definition of $\text{nof}$ and of gateway, $\text{nof}_{H,K}(S_1(H), s(H))$ has an input transition enabled from a participant in $S_1$, hence $\text{nof}_{K,H}(S_2(K), s(K))$ has a corresponding output transition enabled towards a participant in $S_2$ by compatibility. By construction (Definition A.1), $s \lfloor_K(K) = \text{nof}_{K,H}(S_2(K), s(K))$, hence there is a participant, in particular $K$, willing to take a transition.
If the receiver of the output from H is a participant of S₁ then, by definition of gateway and configuration projection, we get that in H is willing to perform an output from H]s(H) in S₁.

* H can perform a τ-transition.

Then, there is a sequence of transitions of the form $s(H) \xrightarrow{\tau}^{HX!m} \text{ in } S(H)$ with $X = K$ or $X \neq H$ participant of S₁. If the former case we can reason as in the previous case when H outputs to K. Otherwise, $H]s(H)$ has an enabled τ-transition in S₁(H) by Definition A.1.

If s is a deadlock, by definition of deadlock freedom (cf. Definition 2.5), $s \nrightarrow$ but there are participants in S with enabled transitions in s. Under the assumption that $s|_K$ is deadlock-free, such participants must belong to S₁. By the cases shown above, $H]s$ enables some participants in S₁; therefore, there is $H]s \xrightarrow{\lambda}$ because S₁ is deadlock free by hypothesis. It must be that H is involved in all transitions from $H]s$ of S₁ otherwise $s \xrightarrow{\lambda}$ since for all $X \in \text{ptp}(\lambda) s(X) =_H s(X)$ (by Definition A.1) contrary to our assumption that s is a deadlock. We proceed by case analysis on $\lambda$.

$\lambda = H \rightarrow X: m$ If $X \neq K$ then $H]s(X) = s(X) \xrightarrow{HA?m} $; also, H would be in a connecting state and, by Definition A.1, $H]s(H) = s(H) \xrightarrow{HA!m} $. Hence $s \xrightarrow{\lambda}$ contrary to the hypothesis that s is a deadlock configuration.

If $X = K$ then we have again a contradiction since $s \xrightarrow{\lambda}$ by Proposition B.3.

$\lambda = X \rightarrow H: m$ If $X \neq K$ then $H]s(X) = s(X) \xrightarrow{AH!m} $ and $H]s(X) \xrightarrow{AH?m} = s(H)$ Hence $s \xrightarrow{\lambda}$ contrary to the hypothesis that s is a deadlock configuration.

If $X = K$ then we have again a contradiction since $s \xrightarrow{\lambda}$ by Proposition B.3.

$\lambda = \tau$ If $s(H) = p''$ is fresh then $gw(S_1(H), K)$ must have a sequence of transitions

$$p \xrightarrow{AH?m} p' \xrightarrow{\tau} p'' \xrightarrow{HK!m} r \qquad (14)$$

with A participant of S₁ and $p'$ fresh. (Note that it cannot be $s(H) = p'$ otherwise $s(H) \xrightarrow{\tau}$ contradicting $s \nrightarrow$.) By Definition A.1, $H]s(H) = r$. Hence, by Proposition B.3 we have $s \xrightarrow{H \rightarrow K: m} $ contradicting $s \nrightarrow$.

If $s(H)$ is not fresh then H has a τ transition enabled at $s$ (because $s(H) =_H s(H)$ by Definition A.1) again contradicting $s \nrightarrow$.

**Lemma C.1.** Let $S = S_1^{H \rightarrow K} S_2$ where $S_1$ and $S_2$ are two (H,K)-composable systems with H and K sequential. Given $s \in \mathcal{R}(\llbracket S \rrbracket)$, if

(1) either $H]s \xrightarrow{\lambda} s'$ in $S_1$ and $\lambda = \tau \implies H]s(H) = s'(H)$

(2) or $H]s \xrightarrow{\tau} \hat{s}$ involving H in $S_1(H)$ and $\hat{s}$ reaching a configuration $\hat{s}'$ such that $\hat{s}' \xrightarrow{\lambda} s'$ in $S_1$ with $\lambda = H \rightarrow A: m$

then there is a run $s \xrightarrow{\lambda_1} \dots \xrightarrow{\lambda_n} \hat{s}$ in S such that $\lambda_n = \lambda$ and $H]s = s'$.

The same holds for the right-projection of S.

*Proof.* We give the proof for each case.

**Case (1)** By case analysis on $\lambda$ noticing that the case $\lambda = H \rightarrow A: m$ is not possible since $H]s$ cannot enable output transitions from H by construction (cf. Definition A.1).

$\lambda = \tau$. Then the τ-transition is executed by $A \neq H$ in $S_1$; hence there is a transition $H]s(A) \xrightarrow{\tau} q$ in $S_1(A)$. Observing that $s(A) =_H s(A)$ by Definition A.1 we have the thesis since $s \xrightarrow{\tau} s[A \mapsto q]$.
$\lambda = A \to H: m$. We have

$$ H \rfloor s(H) \xrightarrow{AH?m} p \text{ in } S_1(H) \quad \text{and} \quad H \rfloor s(A) \xrightarrow{AH!m} q \text{ in } S_1(A) $$

moreover, $s(H) =_H \rfloor s(H)$ and $s(A) =_H \rfloor s(A)$. Hence,

$$ s \xrightarrow{A \to H: m} s'' \quad \text{with} \quad s''(X) = \begin{cases} p, & \text{if } X = H \\ q, & \text{if } X = A \\ s(X), & \text{otherwise} \end{cases} $$

by Definition 2.3. Therefore $H \rfloor s'' = s'$.

**Case (2)** Note that $S_1(H)$ necessarily contains the transitions $H \rfloor s(H) \xrightarrow{\tau} s'(H) \xrightarrow{HA!m} r$. Then, by construction, in $gw(S_1(H), K)$ we have

$$ H \rfloor s(H) \xrightarrow{KH?m} p \xrightarrow{\tau} s'(H) \xrightarrow{HA!m} r \quad (15) $$

note that $p$ and $s'(H)$ are fresh, that these are the only transitions from $H \rfloor s(H)$ to $r$ by sequentiality, and that $s(H) \in \{H\} \rfloor s(H)$, $p, s'(H)$ by construction (cf. Definition A.1). If $s(H) =_H \rfloor s(H)$ then, by Proposition B.3, we have $s \xrightarrow{K \to H: m} \xrightarrow{\tau} s''$ with $s''(H) = s'(H)$. Hence $H \rfloor s'' = H \rfloor s[H \mapsto r]$ and therefore $s'' \xrightarrow{H \to A: m} s''[H \mapsto r, A \mapsto s'(A)] = s'''$ which yields the thesis noticing that $H \rfloor s''' = s'$. If $s(H) = p$ then $s \xrightarrow{\tau} s''$ with $s''(H) = s'(H)$; hence the thesis follows as in the previous case. Finally, if $s(H) = s'(H)$ then $s \xrightarrow{H \to A: m} s''$ with $s'' = s[H \mapsto r, A \mapsto s'(A)]$ and therefore $H \rfloor s'' = s'$. $\square$

**Theorem 5.5 (Lock-freedom preservation).** Let $S_1$ and $S_2$ be two $(H, K)$-composable and lock-free systems with $H$ and $K$ sequential. Then the composed system $S_1^{H \leftrightarrow K} S_2$ is lock-free.

*Proof.* By contradiction, let us assume $S = S_1^{H \leftrightarrow K} S_2$ not to be lock-free. Then there is a configuration $s \in \mathcal{R}(\llbracket S \rrbracket)$ and a participant $X$ not involved in any run from $s$. Without any loss of generality, we can assume $X \in S_1$. We have $H \rfloor s \in \mathcal{R}(\llbracket S_1 \rrbracket)$ by Proposition B.3 and, by lock-freedom of $S_1$, $H \rfloor s$ cannot be a lock of $S_1$ for $X$. Hence, there exists a run $H \rfloor s \xrightarrow{\lambda_0} s_0 \cdots s_{n-1} \xrightarrow{\lambda_n} s_n$ of $S_1$ with $X$ involved in $\lambda_n$. We show that this induces a run from $s$ in $S$ involving $X$ by induction on $n$.

* If $n = 0$, by Lemma C.1 there is a run $s \xrightarrow{\psi} \lambda$ such that $H \rfloor s' = s_0$ with $\lambda_0 = \lambda$.

* If $n > 0$, we assume that the statement holds for all runs with less than $n$ transitions. If $X$ is involved in $\lambda_i$ with $0 \le i < n$ then the thesis follows by inductive hypothesis. Let us therefore assume that $X$ is involved in $\lambda_n$ only. By repeated application of Lemma C.1, there is a run $s \xrightarrow{\psi_1 \cdot \lambda'_1} s'_1 \cdots \xrightarrow{\psi_{n-1} \cdot \lambda'_{n-1}} s'_{n-1} \xrightarrow{\psi_{n} \cdot \lambda'_{n}} s'_n$ in $S$ such that $\lambda'_i = \lambda_i$ and $H \rfloor s'_i = s_i$ for each $1 \le i \le n$.

In both cases $s$ reaches a configuration with a run involving $X$, which contradicts our assumption. $\square$

**Theorem 5.6 (Strong lock freedom preservation).** Let $S_1$ and $S_2$ be two $(H, K)$-composable and strongly lock free systems. Then the composed system $S_1^{H \leftrightarrow K} S_2$ is strongly lock free.

*Proof.* By contradiction, let us assume $S_1^{H \leftrightarrow K} S_2$ not to be strongly lock free. This means that there are a reachable configuration $s$, a participant $X$, and a maximal run $\psi$ of $S_1^{H \leftrightarrow K} S_2$ such that $s \xrightarrow{\psi} X$ and $X$ is not involved in any of those transitions. By the first part of the proof of Theorem 5.1, there exist two run $H \rfloor s \xrightarrow{\psi_1} X$ and $s \lfloor_K \psi_2$ of $S_1$ and $S_2$ respectively such that $X$ is involved neither in $\psi_1$ nor in $\psi_2$.
* In case $\psi$ is infinite, we get that either $\psi_1$ or $\psi_2$ is infinite, and hence maximal.

* In case $\psi$ is finite it is possible to use the second part of the proof of Theorem 5.1 to show that either $\psi_1$ or $\psi_2$ is maximal,

In both cases we get a contradiction of the hypothesis that $S_1$ and $S_2$ are strong lock free. $\square$