On the Send-Synchronizability Problem for Mailbox Communication

Delpy, Romain; Muscholl, Anca; Sutre, Grégoire

doi:10.4230/LIPIcs.CONCUR.2025.15

On the Send-Synchronizability Problem for Mailbox Communication

Romain Delpy

LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France Anca Muscholl

LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France Grégoire Sutre

LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France

Abstract

A system of communicating automata is send-synchronizable if its set of send sequences (i.e., the projection on send actions of its executions) is the same when communications are asynchronous and when they are rendez-vous synchronizations. Send-synchronizability was claimed to be decidable for the mailbox semantics (Basu and Bultan, 2011) and for the peer-to-peer semantics (Basu and Bultan, 2016). Finkel and Lozes showed in 2017 that the proofs of these results are flawed, and they proved that send-synchronizability is in fact undecidable for peer-to-peer systems. The send-synchronizability problem for mailbox systems was left open. A partial solution was recently proposed in (Di Giusto, Laversa and Peters, 2024). In this paper, we revisit the send-synchronizability problem for mailbox systems. Firstly, we show that send-synchronizability is undecidable for mailbox systems, thus closing the question left open in (Finkel and Lozes, 2023) and (Di Giusto, Laversa and Peters, 2024). Secondly, we show that send-synchronizability is decidable for the class of 1-schedulable mailbox systems. A system is 1-schedulable if every execution can be re-scheduled into an equivalent execution where each send is either immediately followed by its matching receive, or is never matched. Despite the apparent similarity between send-synchronizability and 1-schedulability, the proof that send-synchronizability is decidable for 1-schedulable mailbox systems is quite involved. We believe that the techniques that we develop in this proof could be used to address other problems on mailbox systems, such as the realizability problem.

Keywords and phrases:

Concurrent programming, Mailbox communication, Verification, Synchronizability

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification

Funding:

This work was (partially) supported by the grant ANR-23-CE48-0005 of the French National Research Agency ANR (project PaVeDyS).

DOI:

10.4230/LIPIcs.CONCUR.2025.15

Event:

36th International Conference on Concurrency Theory (CONCUR 2025)

Editors:

Patricia Bouyer and Jaco van de Pol

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Message-passing is a key synchronization mechanism for concurrent programming and distributed systems. In this model, processes running asynchronously synchronize by exchanging messages over unbounded channels. Typically, the communication follows a peer-to-peer model, which is particularly useful for reasoning about telecommunication protocols.

Recently, mailbox communication has attracted increased attention due to its role in multi-thread programming, as seen in languages like Rust or Erlang. In mailbox communication each process has a single incoming communication buffer, or mailbox, where messages from other processes are multiplexed.

Asynchronous communication poses significant challenges for formal verification, since it can easily emulate Turing machines. The quest for conditions that ensure decidability for automatic verification has led to various restrictions, such as constraints on channel behavior (e.g. lossiness [1, 12], or properties based on partial-orders [18, 14, 20]). More recently, research has focused on restricting the communication protocols themselves [6, 16, 17, 8].

While synchronous communication offers great simplicity, its relevance extends beyond verification. Many specification formalisms, such as choreography languages [2] and multi-party session types [24, 22, 23], are built upon synchronous communication. This raises a fundamental question, considering the inherent asynchrony of real-world systems: how different is an asynchronous system from its idealized synchronous version, where every sent message is instantaneously received?

Send-synchronizability offers one way to compare synchronous and asynchronous semantics. The work [13] defined a system as (send-)synchronizable if the sequence of sent messages is identical under both asynchronous and synchronous semantics. While [2] claimed decidability for mailbox systems and later extended the claim to peer-to-peer systems [3], the latter claim was refuted by [10, 11], showing undecidability for peer-to-peer systems. The decidability of send-synchronizability for mailbox systems, however, remained an open question (see, e.g., [9]), and this paper addresses it.

Send-synchronizability has been explored in several subsequent works [2, 4, 3, 11, 9] with variations such as final states, or requiring that the same state is reached in both the synchronous and asynchronous execution. For example, in [9], each process has a set of final states. This generalized version was shown to be undecidable in [9], with final states playing a key role in the proof. Our first contribution is to show that send-synchronizability remains undecidable even in the standard setting of communicating systems without final states.

Our second contribution shows the decidability of send-synchronizability for $1$ -schedulable systems. These systems, termed 1-synchronizable in [6] but renamed here for clarity, share similarities with the synchronous semantics. However, a key difference is that not all messages need to be received. A system is $1$ -schedulable if every execution can be reordered into an equivalent one where each send is either immediately followed by its corresponding receive, or remains unmatched. Being $1$ -schedulable is a decidable property, with PSPACE complexity [6, 16]. We show that send-synchronizability is decidable for $1$ -schedulable systems, but the proof is surprisingly intricated because of the unreceived messages. Our proof employs partial-order techniques (commutations), with the main challenge being the unmatched send events.

For convenience, technical terms and notations in the electronic version of this manuscript are hyper-linked to their definitions (cf. https://ctan.org/pkg/knowledge).

2 Definitions and Notations

2.1 Mailbox message-passing systems

We let $\mathbb{P}$ denote a finite non-empty set of processes, and $\mathbb{M}$ denote a finite non-empty set of message contents. The set of (communication) actions is $\mathit{Act}=\{p!q(m),q?p(m)\mid p,q\in\mathbb{P},p\not=q,m\in\mathbb{M}\}$ . An action $p!q(m)$ denotes a send by $p$ of message $m$ to $q$ and an action $p?q(m)$ denotes a receive by $p$ of message $m$ from $q$ . In both cases, the process performing the action is $p$ . A communicating finite-state machine [7] is a finite set of processes that exchange messages, each process being given as a finite LTS. Recall that a (finite) labeled transition system, LTS for short, is a quadruple $(L,A,\to,i)$ where $L$ is a (finite) set of states, $A$ is a finite alphabet, ${\to}\subseteq L\times A\times L$ is a set of transitions, and $i\in L$ is an initial state. In the following definition, $\mathit{Act}_{p}$ denotes the set of actions $a\in\mathit{Act}$ performed by $p$ .

A Communicating Finite-State Machine (CFM for short) is a tuple $\mathcal{A}=(\mathcal{A}_{p})_{p\in\mathbb{P}}$ , where each $\mathcal{A}_{p}$ is a finite LTS $\mathcal{A}_{p}=(L_{p},\mathit{Act}_{p},\to_{p},i_{p})$ . States in $L_{p}$ are called local states. The size of $\mathcal{A}$ is defined as $\sum_{p\in\mathbb{P}}(|L_{p}|+|\to_{p}|)$ .

The usual semantics of communication is peer-to-peer, with (at most one) fifo channel for each pair of distinct processes. In this paper we focus on the mailbox semantics. Here, every process has a receiving fifo queue in which every other process can enqueue messages. We define the semantics by an associated global transition system.

Let $\mathcal{A}=(\mathcal{A}_{p})_{p\in\mathbb{P}}$ be a CFM. The global transition system associated with $\mathcal{A}$ is the LTS $\mathcal{T}(\mathcal{A})=(C_{\mathcal{A}},\mathit{Act},\rightarrow_{\mathcal{A% }},c_{in})$ with set of configurations $C_{\mathcal{A}}=G\times\prod_{p\in\mathbb{P}}(\mathbb{P}\times\mathbb{M})^{*}$ consisting of global states $G=\prod_{p\in\mathbb{P}}L_{p}$ (i.e., products of local states) and queue contents over the alphabet $\mathbb{P}\times\mathbb{M}$ . Let $((\ell_{p})_{p\in\mathbb{P}},(w_{p})_{p\in\mathbb{P}})\xrightarrow{a}_{% \mathcal{A}}((\ell_{p}^{\prime})_{p\in\mathbb{P}},(w^{\prime}_{p})_{p\in% \mathbb{P}})$ if

$\blacksquare$

$\ell_{p}\xrightarrow{a}_{p}\ell_{p}^{\prime}$ and $\ell_{q}=\ell_{q}^{\prime}$ for $q\not=p$ , where $p$ is the process performing $a$ .
$\blacksquare$

Send actions: if $a=p!q(m)$ then $w^{\prime}_{q}=w_{q}\,(p,m)$ and $w^{\prime}_{p^{\prime}}=w_{p^{\prime}}$ for $p^{\prime}\not=q$ .
$\blacksquare$

Receive actions: if $a=p?q(m)$ then $(q,m)\,w^{\prime}_{p}=w_{p}$ and $w^{\prime}_{p^{\prime}}=w_{p^{\prime}}$ for $p^{\prime}\not=p$ .

The initial configuration is $c_{in}=((i_{p})_{p\in\mathbb{P}},\varepsilon^{\mathbb{P}})$ .

An execution of $\mathcal{T}(\mathcal{A})$ is a sequence $\rho=c_{0}\xrightarrow{a_{1}}c_{1}\cdots\xrightarrow{a_{n}}c_{n}$ with $c_{i}\in C_{\mathcal{A}}$ such that $c_{i-1}\xrightarrow{a_{i}}_{\mathcal{A}}c_{i}$ for every $i$ . The sequence $a_{1}\cdots a_{n}$ is the label of the execution. The execution is initial if $c_{0}=c_{in}$ .

$\blacktriangleright$ Remark 2.1.

Note that the queue content includes the identity of the sender. This is to exclude executions labelled by $p!q(m)\;q?r(m)$ with $p\not=r$ . Without this addition such executions would be allowed in the mailbox semantics, which is clearly not intended.

Definition 2.2 (Trace).

A trace of a CFM $\mathcal{A}$ is a sequence $u\in\mathit{Act}^{*}$ such that there exists an initial execution of $\mathcal{T}(\mathcal{A})$ labelled by $u$ . The set of all traces of $\mathcal{A}$ is denoted by $\mathit{Tr}(\mathcal{A})$ .

Definition 2.3 (Viable).

A sequence $v\in\mathit{Act}^{*}$ is called viable if for every $p\in\mathbb{P}$ :

$\blacksquare$

for every prefix $u$ of $v$ , the number of receives of $p$ in $u$ is less or equal the number of sends to $p$ in $u$ ;
$\blacksquare$

for every $k$ , if the $k$ -th receive of $p$ in $v$ has label $p?q(m)$ then the $k$ -th send to $p$ in $v$ has label $q!p(m)$ .

Definition 2.4 (Rendez-vous).

A sequence from $\mathit{Act}^{*}$ is called a rendez-vous sequence if it is of the form $p_{1}!q_{1}(m_{1})q_{1}?p_{1}(m_{1})\dots p_{n}!q_{n}(m_{n})q_{n}?p_{n}(m_{n})$ . Note that every send action is matched in a rendez-vous sequence, and that such sequences are viable. We define $\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})\subseteq\mathit{Tr}(\mathcal{A})$ as the set of traces in $\mathit{Tr}(\mathcal{A})$ that are rendez-vous.

The classical happens-before relation [21], frequently used in reasoning about distributed systems, orders the actions of each process and every (matched) send action before its matching receive. Because of mailbox semantics, an additional order arise between sends to the same process. The happens-before relation together with the mailbox order naturally associates a partial order with every trace, known as message sequence chart:

Definition 2.5 (Message Sequence Chart).

An MSC over $\mathbb{P}$ is an $\mathit{Act}$ -labeled partially ordered set $\mathcal{M}=(E,\preceq,\lambda)$ of events $E$ , with $\lambda:E\to\mathit{Act}$ and $\preceq\mathop{=}(\leq_{\mathbb{P}}\cup\mathop{\mathrm{msg}}\cup\mathop{<_{% \texttt{mb}}})^{*}$ the least partial order containing the relations $\leq_{\mathbb{P}}$ , $\mathop{\mathrm{msg}}$ and $\mathop{<_{\texttt{mb}}}$ , which are defined as:

1.

For every process $p$ , the set of events on $p$ is totally ordered by $\leq_{\mathbb{P}}$ , and $\leq_{\mathbb{P}}$ is the union of these total orders.
2.

$\mathop{\mathrm{msg}}$ is the set of matching send/receive event pairs. In particular, $(e,f)\in\mathop{\mathrm{msg}}$ implies $\lambda(e)=p!q(m)$ and $\lambda(f)=q?p(m)$ for some $p,q\in\mathbb{P}$ and $m\in\mathbb{M}$ . Moreover, $\mathop{\mathrm{msg}}$ is a partial bijection between sends and receives such that every receive is paired with a (unique) send. A send is called matched if it is in the domain of $\mathop{\mathrm{msg}}$ , and unmatched otherwise.
3.
for every process $p$ , we order two sends $e\mathop{<_{\texttt{mb}}}e^{\prime}$ with $e=q!p(m)$ and $e^{\prime}=q^{\prime}!p(m^{\prime})$ if
- $\blacksquare$
  
  either $e$ is matched and $e^{\prime}$ is unmatched,
- $\blacksquare$
  
  or $(e,f),(e^{\prime},f^{\prime})\in\mathop{\mathrm{msg}}$ and $f\mathop{<_{\mathbb{P}}}f^{\prime}$ .
We call $\mathop{<_{\texttt{mb}}}$ the mailbox order.

For two events $e,f\in E$ we write $e\parallel f$ if neither $e\preceq f$ nor $f\preceq e$ holds. For a set of events $F\subseteq E$ we write $\mathit{Past}(F)=\{f\mid f\preceq e\text{ for some $e\in F$}\}$ and $\mathit{Ftr}(F)=\{f\mid e\preceq f\text{ for some $e\in F$}\}$ for the causal past and future of $F$ , respectively.

$p_{0}!p_{1}(m_{0})\,p_{1}!p_{2}(m_{1})\,p_{2}?p_{1}(m_{1})\,p_{2}!p_{1}(m_{2})% \,p_{1}?p_{0}(m_{0})$

Figure 1: A sequence and its MSC. An unmatched send action is marked by a special arrowhead, as for

m_{2}

. We have here

s_{0}\mathop{<_{\texttt{mb}}}s_{2}

, so

s_{0}\prec s_{2}

, and

s_{1}\parallel s_{0}

, with

s_{i}

the send of message

m_{i}

.

If $u=u[1]\dots u[n]$ is a viable sequence of actions, then we can associate an MSC with $u$ by setting $\texttt{msc}(u)=(E,\preceq,\lambda)$ with $E=\{e_{1},\dots,e_{n}\}$ , $\lambda(e_{i})=u[i]$ , and the orders defined as expected:

$\blacksquare$

$e_{i}\leq_{\mathbb{P}}e_{j}$ if $u[i]$ and $u[j]$ are performed by the same process and $i\leq j$ .
$\blacksquare$

$(e_{i},e_{j})\in\mathop{\mathrm{msg}}$ if there exists $k\geq 1$ and a process $p$ such that $u[i]$ is the $k$ -th send to $p$ and $u[j]$ is the $k$ -th receive of $p$ .
$\blacksquare$

$e_{i}\mathop{<_{\texttt{mb}}}e_{j}$ if $u[i]$ and $u[j]$ are both sends to the same process $p$ , $u[i]$ is matched to some $u[k]$ , and either $u[j]$ is unmatched, or $u[j]$ is matched to some $u[\ell]$ with $k\leq\ell$ .

$\blacktriangleright$ Remark 2.6.

By definition, for any viable sequence $u$ , the associated MSC $\texttt{msc}(u)$ is well-defined. For the converse, for every MSC $\mathcal{M}$ , every (labelled) linearization of the partial order $\preceq$ of $\mathcal{M}$ is viable. Indeed, all receives of the same process are totally ordered by $\leq_{\mathbb{P}}$ , and the corresponding sends are ordered in the same way because of the mailbox order. For example, the sequence shown in Figure 1 is viable, but $p_{1}!p_{2}(m_{1})\,p_{2}?p_{1}(m_{1})\,p_{2}!p_{1}(m_{2})\,p_{0}!p_{1}(m_{0})% \,p_{1}?p_{0}(m_{0})$ is not.

The next definition introduces an equivalence relation $\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}$ on sequences of actions. Two viable sequences are equivalent up to commuting adjacent actions that are not ordered by being on the same process, being a matching send/receive pair, or being two sends to the same process that are not both unmatched.

Definition 2.7 (Equivalence $\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}$ ).

Two viable sequences $u,v\in\mathit{Act}^{*}$ are called equivalent if $\texttt{msc}(u)=\texttt{msc}(v)$ (up to isomorphism), and we write $u\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}v$ in this case.

In this paper, we define (as in [2, 10]) the observable behavior of a CFM as the set of projections on sends. We set $S=\{p!q(m)\mid p,q\in\mathbb{P},p\not=q,m\in\mathbb{M}\}$ . For a sequence $u\in\mathit{Act}^{*}$ , we denote by ${u}|_{S}$ the projection of $u$ on $S$ . For any $X\subseteq\mathit{Act}^{*}$ , we write ${X}|_{S}=\{{u}|_{S}\mid u\in X\}$ .

Definition 2.8 (Send-synchronizability).

Let $\mathcal{A}$ be a CFM. We say that $\mathcal{A}$ is send-synchronizable if ${\mathit{Tr}(\mathcal{A})}|_{S}={\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})}|_{S}$ .

The send-synchronizability problem is the question whether a CFM is send-synchronizable.

3 Undecidability of Send-Synchronizability for Mailbox Systems

We show in this section that the send-synchronizability problem is undecidable. We rely in our undecidability proof on the following decision problem, which is a variant of the well-known Post correspondence problem.

Pre-MPCP
Input:	A finite sequence of pairs $(x_{1},y_{1}),\ldots,(x_{K},y_{K})$ , with $K\geq 1$ , where $x_{i},y_{i}\in\Sigma^{*}$ for some finite alphabet $\Sigma$ .
Output:	Yes if there exists a sequence of indices $i_{1},\ldots,i_{k}\in\{1,\ldots,K\}$ , with $k\geq 1$ , such that $i_{1}=1$ , $x_{i_{1}}\cdots x_{i_{k}}=y_{i_{1}}\cdots y_{i_{k}}$ and $\|x_{i_{1}}\cdots x_{i_{j}}\|\geq\|y_{i_{1}}\cdots y_{i_{j}}\|$ for every $j\in\{1,\ldots,k\}$ .

It is well-known that Pre-MPCP is undecidable [19]. The remainder of this section provides a reduction from Pre-MPCP to send-synchronizability.

Consider an instance $\mathcal{I}=(x_{1},y_{1}),\ldots,(x_{K},y_{K})$ of Pre-MPCP over a finite alphabet $\Sigma$ . We construct a CFM $\mathcal{A}(\mathcal{I})$ such that $\mathcal{I}$ is a positive instance of Pre-MPCP if, and only if, $\mathcal{A}(\mathcal{I})$ is not send-synchronizable. The CFM $\mathcal{A}(\mathcal{I})$ comprises three processes, namely $G$ (the guesser), $R$ (the relayer), and $V$ (the verifier). So $\mathbb{P}=\{G,R,V\}$ . The set of message contents is $\mathbb{M}=\Sigma\cup\overline{\Sigma}\cup\{\$,\overline{\$},\#\}$ , where $\overline{\Sigma}=\{\overline{a}\mid a\in\Sigma\}$ is disjoint from $\Sigma$ , and the messages $\$$ , $\overline{\$}$ and $\#$ denote three distinct symbols that are not in $\Sigma\cup\overline{\Sigma}$ . We choose to introduce a copy $\overline{\Sigma}\cup\{\overline{\$}\}$ of the alphabet $\Sigma\cup\{\$\}$ in order to easily¹¹1In our global transition system $\mathcal{T}(\mathcal{A})$ , each message content stored in a buffer is decorated with the channel of the corresponding send action. So our construction would also work without the copy $\overline{\Sigma}\cup\{\overline{\$}\}$ of $\Sigma\cup\{\$\}$ , but we believe that this copy makes our construction easier to read. distinguish in the mailbox of $V$ the messages that were sent by $G$ from the messages that were sent by $R$ . The symbols $\$$ and $\overline{\$}$ are used to mark the end of the sequences $x_{i_{1}}\cdots x_{i_{k}}$ and $\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}$ guessed by $G$ . It is understood that $\overline{y_{1}},\ldots,\overline{y_{K}}$ are the words in $\overline{\Sigma}$ that are obtained from $y_{1},\ldots,y_{K}$ by replacing each letter $a$ by $\overline{a}$ . The message $\#$ is sent by $V$ when the two guessed sequences are equal. The LTSes $\mathcal{A}_{G}$ , $\mathcal{A}_{R}$ and $\mathcal{A}_{V}$ of the processes $G$ , $R$ and $V$ are defined in Figures 2, 3, and 4. To ease understanding, the resulting communication topology, along with the potential message contents in the channels, is depicted in Figure 5. In the description of the guesser process (see Figure 2), we use the shortcuts $G!R(x_{i})$ and $G!V(\overline{y_{i}})$ to reduce clutter. Let us explain what we mean by these shortcuts. A transition $\ell\xrightarrow{p!q(m_{1}\cdots m_{n})}\ell^{\prime}$ , where $m_{i}\in\mathbb{M}$ , stands for the contiguous sequence of transitions $\ell=\ell_{0}\xrightarrow{p!q(m_{1})}\ell_{1}\cdots\ell_{n-1}\xrightarrow{p!q(% m_{n})}\ell_{n}=\ell^{\prime}$ where $\ell_{1},\ldots,\ell_{n-1}$ are intermediate states. The observant reader will notice that the LTSes $\mathcal{A}_{R}$ and $\mathcal{A}_{V}$ contain silent transitions (from the initial state to the states $D$ and $N$ ), which are not allowed in our definition of CFM. This is merely a notational convenience to reduce clutter in the figures. We may safely get rid of these silent transitions since send-synchronizability of a CFM is not sensitive to such transitions.

Figure 2: LTS

\mathcal{A}_{G}

of the guesser process

G

of the CFM

\mathcal{A}(\mathcal{I})

.

Figure 3: LTS

\mathcal{A}_{R}

of the relayer process

R

of the CFM

\mathcal{A}(\mathcal{I})

.

Figure 4: LTS

\mathcal{A}_{V}

of the verifier process

V

of the CFM

\mathcal{A}(\mathcal{I})

.

Figure 5: Topology of the CFM

\mathcal{A}(\mathcal{I})

and message contents potentially exchanged along the channels. The

+

sign serves as a reminder that the channels

(G,V)

and

(R,V)

are multiplexed into a single mailbox.

The behavior of the guesser process $G$ should be quite clear. It sends the two guessed sequences and then waits for a message $\#$ from $V$ , which it relays to $R$ , signaling that the guessed sequences form a solution. The relayer process $R$ has two operating modes, a normal mode (right-hand side of Figure 3) and a dummy mode (left-hand side of Figure 3). In the normal mode, $R$ simply relays to $V$ every message that it receives from $G$ . For $V$ to process its mailbox properly (see below), the send actions $G!V(\cdot)$ and $R!V(\cdot)$ need to be interleaved in lock-step (but there may be executions in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ where this does not hold). The purpose of the dummy mode is to make $\mathcal{A}(\mathcal{I})$ send-synchronizable if $\mathcal{I}$ is a negative instance of Pre-MPCP. Notice that there is no switch between modes. Analogously, the verifier process $V$ has a normal mode and a dummy mode (right-hand and left-hand sides of Figure 4, respectively). In the normal mode, $V$ checks that the contents of its mailbox is of the form $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ . It then sends $\#$ to $G$ if that is the case (otherwise it is blocked). The purpose of the dummy mode is the same as for $R$ . Observe that the message $\#$ sent by $V$ to $G$ is relayed by $G$ to $R$ , and then relayed by $R$ back to $V$ , but $V$ never receives it.

We first show that if $\mathcal{I}$ is a positive instance of Pre-MPCP, then $\mathcal{A}(\mathcal{I})$ is not send-synchronizable.

Lemma 3.1.

If $\mathcal{I}$ is a positive instance of Pre-MPCP then there is an initial execution in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ leading to the configuration $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ .

Proof sketch..

$G$ guesses a solution $i_{1},\ldots,i_{k}$ , and sends $x_{i_{1}}\cdots x_{i_{k}}\$$ and $\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}\overline{\$}$ to $R$ and $V$ , respectively. $R$ relays $x_{i_{1}}\cdots x_{i_{k}}\$$ to $V$ with the appropriate delay so that the mailbox of $V$ is filled by $G$ and $R$ in lock-step. This is possible because our variant of PCP requires that $|x_{i_{1}}\cdots x_{i_{j}}|\geq|y_{i_{1}}\cdots y_{i_{j}}|$ for every $j\in\{1,\ldots,k\}$ . We end up with $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ in the mailbox of $V$ . Then $V$ empties its mailbox by iterating the cycle on $N$ . $\hfill\blacktriangleleft$

Corollary 3.2.

If $\mathcal{I}$ is a positive instance of Pre-MPCP then there is a trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ containing the action $R!V(\#)$ , hence, $\mathcal{A}(\mathcal{I})$ is not send-synchronizable.

Now we show that if $\mathcal{I}$ is a negative instance of Pre-MPCP, then $\mathcal{A}(\mathcal{I})$ is send-synchronizable. Some additional notations are needed. For every process $p\in\mathbb{P}$ , we let $L(\mathcal{A}_{p})$ denote the language recognized by the LTS $\mathcal{A}_{p}$ viewed as a non-deterministic automaton with every state final, and we let ${u}_{|p}$ denote the projection of a sequence $u\in\mathit{Act}^{*}$ on $\mathit{Act}_{p}$ . We also define $\mathit{match}:S^{*}\rightarrow\mathit{Act}^{*}$ as the morphism given by $\mathit{match}(p!q(m))=p!q(m)\,q?p(m)$ .

Lemma 3.3.

If there is a trace in $\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ containing the action $R!V(\#)$ then $\mathcal{I}$ is a positive instance of Pre-MPCP.

Lemma 3.4.

For every trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ , if $u$ does not contain the action $R!V(\#)$ then ${\mathit{match}({u}|_{S})}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\{G,R,V\}$ .

Proof sketch..

Either $u$ contains no send action to $G$ , or $u$ contains a single send action to $G$ , which is $V!G(\#)$ . In that case, this action is necessarily after $G!V(\overline{\$})$ and before $G!R(\#)$ . In both cases, we get that ${\mathit{match}({u}|_{S})}_{|G}\in L(\mathcal{A}_{G})$ .

All sends to $R$ are from $G$ and all sends by $R$ are to $V$ . The word sent by $G$ to $R$ in $u$ is a prefix of a word in $\Sigma^{*}\$\#$ . The word sent by $R$ to $V$ in $u$ is a prefix of a word in $\Sigma^{*}\$$ , since $u$ does not contain the action $R!V(\#)$ . It follows that ${\mathit{match}({u}|_{S})}_{|R}\in L(\mathcal{A}_{R})$ , by letting $R$ select the dummy mode.

The word sent to $V$ in $u$ is in $(\Sigma\cup\overline{\Sigma}\cup\{\$,\overline{\$}\})^{*}$ , since $u$ does not contain the action $R!V(\#)$ . If $u$ contains no send action by $V$ , then ${\mathit{match}({u}|_{S})}_{|V}\in L(\mathcal{A}_{V})$ , by letting $V$ select the dummy mode. Otherwise, $u$ contains a single send action by $V$ , which is $V!G(\#)$ . The definition of $\mathcal{A}_{V}$ (together with the mailbox semantics) entails that the word sent to $V$ in $u$ is of the form $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ . Moreover, the action $V!G(\#)$ is necessarily after $G!V(\overline{\$})$ . We derive that ${\mathit{match}({u}|_{S})}_{|V}$ coincides with the sequence of actions by $V$ in $u$ , hence, ${\mathit{match}({u}|_{S})}_{|V}\in L(\mathcal{A}_{V})$ . $\hfill\blacktriangleleft$

Corollary 3.5.

If $\mathcal{I}$ is a negative instance of Pre-MPCP then $\mathcal{A}(\mathcal{I})$ is send-synchronizable.

We then get the next theorem from Corollaries 3.2 and 3.5.

Theorem 3.6.

The send-synchronizability problem is undecidable.

4 Send-synchronizability and $1$ -schedulable Systems

In this section we show that we can decide send-synchronizability for a subclass of CFMs that we call $1$ -schedulable.²²2This decidable class of systems originates from [6] and it is the same as 1-synchronizable there. To better distinguish it from send-synchronizability we decided to rename it here into $1$ -schedulable. Comparison with other close notions can be found in Appendix A. We start by defining $1$ -schedulable systems and a commutation relation over send sequences. Then we show that if all traces of a $1$ -schedulable CFM respect a certain property (and we say the CFM is good in this case) then we can check if the CFM is send-synchronizable. Next we show that any $1$ -schedulable CFM that is not good, cannot be send-synchronizable. Finally we show that we can check if a $1$ -schedulable CFM is good.

Definition 4.1 ( $1$ -scheduling and $1$ -schedulable).

A viable sequence $u\in\mathit{Act}^{*}$ is a $1$ -scheduling if every send action in $u$ is either directly followed by its receive or it is unmatched. We also say in that case that $u$ is $1$ -scheduled. A sequence $u\in\mathit{Act}^{*}$ is $1$ -schedulable if there exists $v\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}u$ such that $v$ is a $1$ -scheduling.

A CFM $\mathcal{A}$ is $1$ -schedulable if every trace $u\in\mathit{Tr}(\mathcal{A})$ is $1$ -schedulable.

From [8] (see also [16]) we know that $1$ -schedulability is a decidable property (PSPACE-complete). To make the characterization formal, we need some notation first. Given a binary relation $\bowtie$ over some set $X$ , a $\bowtie$ -cycle is any sequence $(x_{1},\ldots,x_{k})\in X$ , with $k\geq 1$ , such that $x_{1}\bowtie x_{2}\cdots\bowtie x_{k+1}$ , where $x_{k+1}:=x_{1}$ . A viable sequence $w$ is not $1$ -schedulable if, and only if, $\texttt{msc}(w)$ contains a $(\prec\cup\mathop{\mathrm{msg}}^{-1})$ -cycle with at least two distinct sends [8]. For example, the sequence $1!2(m)\,2!1(m^{\prime})\,1?2(m^{\prime})\,2?1(m)$ is not $1$ -schedulable, as witnessed by the cycle $1!2(m)\mathop{<_{\mathbb{P}}}1?2(m^{\prime})\,\mathop{\mathrm{msg}}^{-1}\,2!1(% m^{\prime})\,\mathop{<_{\mathbb{P}}}2?1(m)\,\mathop{\mathrm{msg}}^{-1}\,1!2(m)$ .

Throughout this section we will assume that the CFM $\mathcal{A}$ is $1$ -schedulable. Our characterization of send-synchronizability will rely on partial commutations applied to the observable behaviors of rendez-vous traces.

Definition 4.2 (Commutations).

We define a commutation relation $\mathit{SI}\subseteq S\times S$ on the alphabet $S$ of sends as follows. Let $a=p!q(m)$ and $b=p^{\prime}!q^{\prime}(m^{\prime})$ be two send actions. Then $(a,b)\in\mathit{SI}$ if $p\not=p^{\prime}$ , $q\not=q^{\prime}$ and $q\not=p^{\prime}$ .

If $(a,b)\in\mathit{SI}$ and $w,w^{\prime}\in S^{*}$ then we write $wabw^{\prime}\Rightarrow_{\mathit{SI}}wbaw^{\prime}$ , and we consider the reflexive-transitive closure $\stackrel{{\scriptstyle*}}{{\Rightarrow}}_{\mathit{SI}}$ of this relation. We denote the commutative closure of a send sequence $v\in S^{*}$ as $\mathit{Cl}_{\mathit{SI}}(v)=\{v^{\prime}\in S^{*}\mid v\stackrel{{% \scriptstyle*}}{{\Rightarrow}}_{\mathit{SI}}v^{\prime}\}$ . We define $\mathit{Cl}_{\mathit{SI}}(E)$ , for $E\subseteq S^{*}$ , as $\bigcup_{v\in E}\mathit{Cl}_{\mathit{SI}}(v)$ .

The example in Figure 6 gives a first intuition about the role of commutations for send-synchronizability. As seen there, if a CFM has an execution $w$ as depicted on the left, and is send-synchronizable, then it has to include also an execution as depicted on the right. This entails that if $1!0(m)2!1(m^{\prime})$ is an observable behavior, then so is $2!1(m^{\prime})1!0(m)$ .

$\blacktriangleright$ Remark 4.3.

It is readily seen that one can check if a regular language $L$ satisfies $L=\mathit{Cl}_{\mathit{SI}}(L)$ . For this it is enough to check that $wabw^{\prime}\in L$ entails $wbaw^{\prime}\in L$ , for all words $w,w^{\prime}$ and $(a,b)\in\mathit{SI}$ . Such a test can be done in Pspace, if $L$ is described by an automaton.

Figure 6: In the left scenario, the two send events

s

and

s^{\prime}

satisfy

s\parallel s^{\prime}

. Note that

(1!0(m),2!1(m^{\prime}))\in\mathit{SI}

, so

1!0(m)\,2!1(m^{\prime})\Rightarrow_{\mathit{SI}}2!1(m^{\prime})\,1!0(m)

. To be send-synchronizable, a CFM must also allow the scenario on the right, where

s^{\prime}\prec s

.

4.1 From $1$ -schedulings to arbitrary traces via commutations

In this subsection we start with a sufficient condition that ensures that the send projections of traces of $\mathcal{A}$ can be obtained via commutations from the send projections of $1$ -schedulings of $\mathcal{A}$ (see Proposition 4.5). The definitions that follow are used in Lemma 4.4, that states the relation between commutations and projections for a single trace.

Consider a viable sequence $w$ . We introduce two binary relations $\dashrightarrow$ and $\ll^{w}_{\mathrm{us}}$ over the set of events $E$ of $\texttt{msc}(w)$ , defined as follows:

$\blacksquare$

$f\dashrightarrow e$ if there exists $p\in\mathbb{P}$ such that $e$ is an unmatched send to $p$ , $f$ is a send from $p$ , and $e\parallel f$ .
$\blacksquare$

$e\ll^{w}_{\mathrm{us}}f$ if there exists $p\in\mathbb{P}$ such that $e$ and $f$ are unmatched sends to $p$ , $e$ is before $f$ in $w$ , and $e\parallel f$ .

We say that $w$ has a backward $\dashrightarrow$ arc if there exists two events $e, f$ such that $f\dashrightarrow e$ and $e$ occurs before $f$ in $w$ . Consider for example the trace $w_{1}$ in Figure 7(a) left: we have $s_{0}\dashrightarrow s_{1}\dashrightarrow s_{2}\dashrightarrow s_{0}$ , so $w_{1}$ has a backward $\dashrightarrow$ arc.

The objective of the $\ll^{w}_{\mathrm{us}}$ relation is to enforce the order of unmatched sends to the same process. Given two viable sequences $w$ and $w^{\prime}$ , we write $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}$ if $w\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}w^{\prime}$ and for every process $p$ , the order of unmatched sends to $p$ is the same in $w$ and $w^{\prime}$ . Notice that for every viable sequences $w,w^{\prime}$ such that $w\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}w^{\prime}$ , we have $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}$ if, and only if, the binary relations $\ll^{w}_{\mathrm{us}}$ and $\ll^{w^{\prime}}_{\mathrm{us}}$ coincide.

Lemma 4.4.

Let $w$ be a $1$ -scheduling and suppose that $w$ has no backward $\dashrightarrow$ arc. Then $\mathit{Cl}_{\mathit{SI}}({w}|_{S})=\{{w^{\prime}}|_{S}\mid w^{\prime}\text{ % is a {\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% viable} sequence and }w^{\prime}\mathop{\mathop{\boldsymbol{{\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us% }}}w\}$ .

Proof.

We write $\mathcal{W}=\{{w^{\prime}}|_{S}\mid w^{\prime}\mathop{\mathop{\boldsymbol{{% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}% _{\mathrm{us}}}w\}$ .

We first show $\mathit{Cl}_{\mathit{SI}}({w}|_{S})\subseteq\mathcal{W}$ recursively on the number of commutation steps. Initially ${w}|_{S}\in\mathcal{W}$ . Now we take $u\in\mathit{Cl}_{\mathit{SI}}({w}|_{S})\cap\mathcal{W}$ , and let $u=u_{0}\,x\,y\,u_{1}$ with $x,y\in S$ , $u_{0},u_{1}\in S^{*}$ and $(x,y)\in\mathit{SI}$ . Let $u^{\prime}=u_{0}\,y\,x\,u_{1}$ be the sequence of sends obtained by commuting $x$ and $y$ . As $u\in\mathcal{W}$ , there is some $v\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w$ such that ${v}|_{S}=u$ . We suppose w.l.o.g. that $v=v_{0}\,x\,y\,v_{1}$ : if there were receives between $x$ and $y$ , each one could either swap with $x$ to the left, or with $y$ to the right, since $x, y$ cannot be on the same process, and the sequence obtained would be $\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}$ equivalent to $v$ . As $(x,y)\in\mathit{SI}$ we know that they are not on the same process, and they do not send to the same process, so $x\parallel y$ and $v\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}v_{0}\,y\,x\,v_{1}$ , hence $u^{\prime}\in\mathcal{W}$ .

Now we show that $\mathit{Cl}_{\mathit{SI}}({w}|_{S})\supseteq\mathcal{W}$ by induction on the size of $w$ . Initially, ${\varepsilon}|_{S}=\varepsilon$ . Let $w=u\,s\,r$ be a $1$ -scheduling without $\dashleftarrow$ arc. Consider some $w^{\prime}\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w$ such that $w^{\prime}=x\,s\,y\,r\,z$ , with $x,y,z\in\mathit{Act}^{*}$ . We have ${w}|_{S}={u}|_{S}\,s$ and ${w^{\prime}}|_{S}={x}|_{S}\,s\,{(yz)}|_{S}$ . We know that $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}xyz\,sr$ so $u\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}xyz$ . The case where $w=u\,s$ is dealt with similarly.

By induction, ${x}|_{S}{(yz)}|_{S}\in\mathit{Cl}_{\mathit{SI}}(u)$ , so ${x}|_{S}{(yz)}|_{S}\,s\in\mathit{Cl}_{\mathit{SI}}(w)$ . Now, we know that $s$ is concurrent with every event of $y z$ . Moreover, there is no $\dashleftarrow$ arc. So for every $s^{\prime}$ occurring in ${(yz)}|_{S}$ : if $s=p!q(m)$ , then $s^{\prime}$ is not on $p$ , and it is neither a send to $p$ (matched or not) nor to $q$ (matched or not), so $(s^{\prime},s)\in\mathit{SI}$ , and ${w^{\prime}}|_{S}\in\mathit{Cl}_{\mathit{SI}}(w)$ . $\hfill\blacktriangleleft$

A viable sequence $w$ is called good if there exists a $1$ -scheduled sequence $w^{\prime}$ such that $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}$ and $w^{\prime}$ has no backward $\dashrightarrow$ arc. Otherwise $w$ is called bad. Note that every good viable sequence is necessarily $1$ -schedulable. A CFM $\mathcal{A}$ is good if every trace in $\mathit{Tr}(\mathcal{A})$ is good, and $\mathcal{A}$ is called bad otherwise.

Proposition 4.5.

For every good CFM $\mathcal{A}$ , it holds that ${\mathit{Tr}(\mathcal{A})}|_{S}$ is the closure under $\mathit{SI}$ of ${\{w\in\mathit{Tr}(\mathcal{A})\mid w\text{ is a {\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}$1$-scheduling}}\}}|_{S}$ .

Proof.

Let $K$ and $L$ be defined as $K={K^{\prime}}|_{S}$ and $L={L^{\prime}}|_{S}$ , where

	$\displaystyle K^{\prime}$	$\displaystyle=\{w\in\mathit{Tr}(\mathcal{A})\mid w\text{ is a {\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}$1$-scheduling} and % has no backward $\dashrightarrow$ arc}\}$
	$\displaystyle L^{\prime}$	$\displaystyle=\{w\in\mathit{Tr}(\mathcal{A})\mid w\text{ is a {\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}$1$-scheduling}}\}$

Note that $K\subseteq L\subseteq{\mathit{Tr}(\mathcal{A})}|_{S}$ . We first show that ${\mathit{Tr}(\mathcal{A})}|_{S}=\mathit{Cl}_{\mathit{SI}}(K)$ . Consider a trace $w\in\mathit{Tr}(\mathcal{A})$ . As $w$ is good, there exists a trace $w^{\prime}\in\mathit{Tr}(\mathcal{A})$ such that $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}$ , $w^{\prime}$ is a $1$ -scheduling and $w^{\prime}$ has no backward $\dashrightarrow$ arc. It holds that $\mathit{Cl}_{\mathit{SI}}({w^{\prime}}|_{S})=\{{u}|_{S}\mid u\mathop{\mathop{% \boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}\}$ according to Lemma 4.4. As ${w^{\prime}}|_{S}\in K$ and $w\mathop{\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}_{\mathrm{us}}}w^{\prime}$ , we get that ${w}|_{S}\in\mathit{Cl}_{\mathit{SI}}(K)$ . The converse inclusion $\mathit{Cl}_{\mathit{SI}}(K)\subseteq{\mathit{Tr}(\mathcal{A})}|_{S}$ immediately follows from Lemma 4.4. Since $K\subseteq L\subseteq{\mathit{Tr}(\mathcal{A})}|_{S}$ and ${\mathit{Tr}(\mathcal{A})}|_{S}=\mathit{Cl}_{\mathit{SI}}(K)$ , we derive that $\mathit{Cl}_{\mathit{SI}}(K)\subseteq\mathit{Cl}_{\mathit{SI}}(L)\subseteq% \mathit{Cl}_{\mathit{SI}}(\mathit{Cl}_{\mathit{SI}}(K))=\mathit{Cl}_{\mathit{% SI}}(K)$ , hence, ${\mathit{Tr}(\mathcal{A})}|_{S}=\mathit{Cl}_{\mathit{SI}}(K)=\mathit{Cl}_{% \mathit{SI}}(L)$ . $\hfill\blacktriangleleft$

The above proposition provides our first ingredient to decide the send-synchronizability problem for $1$ -schedulable CFMs. Two additional ingredients are needed to complete our decidability proof. First, we will show that every bad CFM is not $1$ -schedulable or not send-synchronizable. Second, badness of a CFM will be shown to be decidable. We start with a characterization of bad viable sequences. For a viable sequence $w$ , a $(\prec\cup\mathop{\mathrm{msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us% }})$ -cycle in $\texttt{msc}(w)$ is called trivial if it is of the form $(e,f,\ldots,e,f)$ with $(e,f)\in(\mathop{\mathrm{msg}}\cup\mathop{\mathrm{msg}}^{-1})$ , or equivalently, if it does not contain two distinct sends.

Lemma 4.6.

For every viable sequence $w$ , it holds that $w$ is bad if, and only if, there exists a $(\prec\cup\mathop{\mathrm{msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us% }})$ -cycle in $\texttt{msc}(w)$ that is not trivial.

Proof sketch..

Consider a viable sequence $w$ . For short, let us write $\mathit{TrvCyc}$ the condition that every $(\prec\cup\mathop{\mathrm{msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us% }})$ -cycle in $\texttt{msc}(w)$ is trivial. To prove the lemma, we show that $w$ is good if, and only if, $\mathit{TrvCyc}$ holds. We consider the directed graph $G$ whose nodes are the events of $\texttt{msc}(w)$ and whose edges are given by the relations $<_{\mathbb{P}}$ , $\mathop{\mathrm{msg}}$ , $<_{\texttt{mb}}$ , $\mathop{\mathrm{msg}}^{-1}$ , $\dashrightarrow$ and $\ll^{w}_{\mathrm{us}}$ . Let $H$ denote the directed graph obtained from $G$ by, firstly, merging events that are connected by an $\mathop{\mathrm{msg}}$ -arc, and secondly, removing all $\mathop{\mathrm{msg}}$ -arcs. It is readily seen that $\mathit{TrvCyc}$ is equivalent to the condition that $H$ is acyclic. If $\mathit{TrvCyc}$ holds, then the partial order induced by $H$ admits a linearization $x_{1}\cdots x_{n}$ . By “unmerging” events in $x_{1}\cdots x_{n}$ , we get a linearization $w^{\prime}$ of $\texttt{msc}(w)$ such that $w^{\prime}$ is $1$ -scheduled and $w^{\prime}$ has no backward $\dashrightarrow$ -arc nor backward $\ll^{w}_{\mathrm{us}}$ -arc, hence, $w$ is good. Conversely, if $w$ is good then the sequence $x_{1}\cdots x_{n}$ of nodes of $H$ that is induced by $w$ contains every node of $H$ and has no backward edge, so $H$ is acyclic, hence, $\mathit{TrvCyc}$ holds. $\hfill\blacktriangleleft$

We now focus our attention to CFMs that are $1$ -schedulable. For this class of CFMs, we obtain a characterization of badness of a CFM in terms of cycles that are simpler than those of Lemma 4.6 in the sense that they contain no $\mathop{\mathrm{msg}}^{-1}$ -arc.

Lemma 4.7.

For every $1$ -schedulable CFM $\mathcal{A}$ , if $\mathcal{A}$ is bad then there exists a (bad) trace $w\in\mathit{Tr}(\mathcal{A})$ such that $\texttt{msc}(w)$ contains a $(\prec\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycle.

Proof.

Consider a bad trace $w\in\mathit{Tr}(\mathcal{A})$ of minimal length. Let $\Xi$ denote the set of non-trivial $(<_{\mathbb{P}}\cup\mathop{\mathrm{msg}}\cup<_{\texttt{mb}}\cup\mathop{\mathrm% {msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycles in $\texttt{msc}(w)$ . We lexicographically order cycles $\xi$ in $\Xi$ first by number of $\mathop{\mathrm{msg}}^{-1}$ -arcs (accounting for the arc from the last event of $\xi$ to the first event of $\xi$ ), second by length of the cycle. By Lemma 4.6, the set $\Xi$ is non-empty. Pick a cycle $\xi$ in $\Xi$ of minimal length, and let us show that $\xi$ contains no $\mathop{\mathrm{msg}}^{-1}$ -arc.

We first observe that every event of $\texttt{msc}(w)$ is in $\mathit{Past}(C)$ , where $C$ denotes the set of events of $\xi$ . By contradiction, assume that this is not the case. There necessarily exists an event $e$ in $\texttt{msc}(w)$ such that $e\not\in\mathit{Past}(C)$ , $e$ is maximal for $\leq_{\mathbb{P}}$ and $e$ is a receive or an unmatched send. Consider the sequence $w^{\prime}$ corresponding to $w$ with $e$ removed. It is readily seen that $w^{\prime}$ is viable, hence, $w^{\prime}\in\mathit{Tr}(\mathcal{A})$ . Moreover, the cycle $\xi$ is still a non-trivial $(\prec\cup\mathop{\mathrm{msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us% }})$ -cycle in $\texttt{msc}(w^{\prime})$ . So by Lemma 4.6, $w^{\prime}$ is a bad trace in $\mathit{Tr}(\mathcal{A})$ , which contradicts the minimality of $w$ .

By contradiction, assume that $\xi$ contains an $\mathop{\mathrm{msg}}^{-1}$ -arc. Up to a rotation of the cycle, we may assume that $\xi$ is of the form $(e_{1},\ldots,e_{k})$ with $(e_{k},e_{1})\in\mathop{\mathrm{msg}}^{-1}$ . Note that $k>2$ since $\xi$ is non-trivial. For readability, let us write $s:=e_{1}$ and $r:=e_{k}$ . We make three observations.

1.

The event $r$ is maximal for $\leq_{\mathbb{P}}$ . By contradiction, suppose that $r<_{\mathbb{P}}f$ for some event $f$ . Since $f\in\mathit{Past}(C)$ , we get that $f\preceq e_{i}$ for some $1\leq i\leq k$ . Pick a $(<_{\mathbb{P}}\cup\mathop{\mathrm{msg}}\cup<_{\texttt{mb}})$ -path $(f_{1},\ldots,f_{\ell})$ with $f_{1}=f$ and $f_{\ell}=e_{i}$ . We get that $(e_{i},\ldots,e_{k},f_{1},\ldots,f_{\ell-1})$ is in $\Xi$ and has one less $\mathop{\mathrm{msg}}^{-1}$ -arc than $\xi$ , which contradicts the minimality of $\xi$ .
2.

The event $s^{\prime}:=e_{k-1}$ is a send and $s^{\prime}<_{\mathbb{P}}r=e_{k}$ . Indeed, as $e_{k}$ is a receive, $e_{k-1}$ verifies $e_{k-1}<_{\mathbb{P}}r$ or $(e_{k-1},r)\in\mathop{\mathrm{msg}}$ . If $(e_{k-1},r)\in\mathop{\mathrm{msg}}$ then $e_{k-1}=s=e_{1}$ , hence, $(e_{1},\ldots,e_{k-2})$ is in $\Xi$ , which contradicts the minimality of $\xi$ . So $e_{k-1}<_{\mathbb{P}}r$ . It remains to show that $e_{k-1}$ is a send. Suppose by contradiction that $e_{k-1}$ is a receive. We either have $e_{k-2}<_{\mathbb{P}}e_{k-1}$ or $(e_{k-2},e_{k-1})\in\mathop{\mathrm{msg}}$ . In the first case, $e_{k-2}<_{\mathbb{P}}r=e_{k}$ , hence, $(e_{1},\ldots,e_{k-2},e_{k})$ is in $\Xi$ , which is impossible by minimality of $\xi$ . In the second case, $(e_{k-2},e_{k-1})\in\mathop{\mathrm{msg}}$ , hence, $e_{k-2}<_{\texttt{mb}}s=e_{1}$ . This entails that $(e_{1},\ldots,e_{k-2})$ is in $\Xi$ , which is impossible by minimality of $\xi$ .
3.

It holds that $s\parallel s^{\prime}$ . Let us prove this claim. We have $s^{\prime}<_{\mathbb{P}}r$ and $(r,s)\in\mathop{\mathrm{msg}}^{-1}$ . Note that $s\neq s^{\prime}$ since $s$ and $s^{\prime}$ are sends by distinct processes. If $s\prec s^{\prime}$ then $(s,s^{\prime},r,s)$ would be a $(\prec\cup\mathop{\mathrm{msg}}^{-1})$ -cycle with at least two distinct sends in $\texttt{msc}(w)$ , which is impossible since $w$ is $1$ -schedulable. If $s^{\prime}\prec s$ then $e_{k-1}=s^{\prime}\prec s=e_{1}$ , hence, $(e_{1},\ldots,e_{k-1})$ is in $\Xi$ , which contradicts the minimality of $\xi$ .

We now derive a contradiction, which will conclude the proof that $\xi$ contains no $\mathop{\mathrm{msg}}^{-1}$ -arc. Consider the sequence $w^{\prime\prime}$ corresponding to $w$ with $r$ removed. We have $w^{\prime\prime}\in\mathit{Tr}(\mathcal{A})$ since $r$ is a receive and is maximal for $\leq_{\mathbb{P}}$ , by our first observation above. The event $r=e_{k}$ is the matching receive of $s=e_{1}$ in $\texttt{msc}(w)$ , so $s$ becomes an unmatched send in $\texttt{msc}(w^{\prime\prime})$ . In $\texttt{msc}(w^{\prime\prime})$ , the event $s^{\prime}=e_{k-1}$ is a send and $s$ is a send to the process performing $s^{\prime}$ , by our second observation above. Moreover, as $s\parallel s^{\prime}$ in $\texttt{msc}(w)$ , by our third observation above, we still have $s\parallel s^{\prime}$ in $\texttt{msc}(w^{\prime\prime})$ . It follows that $s^{\prime}\dashrightarrow s$ in $\texttt{msc}(w^{\prime\prime})$ , hence, $e_{k-1}\dashrightarrow e_{1}$ . We derive that $(e_{1},\ldots,e_{k-1})$ is a non-trivial $(\prec\cup\mathop{\mathrm{msg}}^{-1}\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us% }})$ -cycle in $\texttt{msc}(w^{\prime\prime})$ . This entails, by Lemma 4.6, that $w^{\prime\prime}$ is bad, which contradicts the minimality of $w$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 4.8.

Given a viable sequence $w$ , a $(\prec\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycle $(e_{1},\ldots,e_{k})$ in $\texttt{msc}(w)$ is called genuine if $e_{1},\ldots,e_{k}$ are pairwise-distinct and, for every $1\leq i<j\leq k$ , we have $e_{i}\prec e_{j}$ implies $j=i+1$ and $e_{j}\prec e_{i}$ implies $i=1$ and $j=k$ . Informally, a genuine cycle is a simple cycle such that for every events $e, f$ on the cycle, if $e\prec f$ then the subpath of the cycle from $e$ to $f$ is a single $\prec$ -arc. It is routinely checked that if $\texttt{msc}(w)$ contains a $(\prec\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycle then it contains a genuine $(\prec\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycle.

4.2 Bad CFMs

Our goal in this section is to analyze bad, $1$ -schedulable CFMs. We will show a necessary condition for badness in terms of patterns (Proposition 4.10), and we will show that the presence of a pattern prevents a CFM to be send-synchronizable (Proposition 4.11).

We focus on $1$ -scheduled traces, as they can be effectively constructed from the CFM using automata. The binary relation $\ll^{w}_{\mathrm{us}}$ needs to be relaxed as we might need to re-order unmatched sends of a $1$ -scheduling in $\mathit{Tr}(\mathcal{A})$ in order to exhibit a bad $1$ -schedulable trace in $\mathit{Tr}(\mathcal{A})$ . Given a viable sequence $w$ , we introduce the binary relation $\parallel_{\mathrm{us}}$ over the set of events $E$ of $\texttt{msc}(w)$ , defined by $e\parallel_{\mathrm{us}}f$ if there exists $p\in\mathbb{P}$ such that $e$ and $f$ are unmatched sends to $p$ and $e\parallel f$ . Note that $\parallel_{\mathrm{us}}$ is symmetric and contains $\ll^{w}_{\mathrm{us}}$ .

A pattern for a viable sequence $w$ is an alternating sequence of send events $(x_{1},\!y_{1},\!\ldots,\!x_{k},\!y_{k})$ of $\texttt{msc}(w)$ satisfying, with the convention that $x_{k+1}:=x_{1}$ , the following conditions:

1.

$x_{i}\preceq y_{i}$ , for every $1\leq i\leq k$ ,
2.

$y_{i}\dashrightarrow x_{i+1}$ or $y_{i}\parallel_{\mathrm{us}}x_{i+1}$ , for every $1\leq i\leq k$ ,
3.

$y_{i}\dashrightarrow x_{i+1}$ for some $1\leq i\leq k$ ,
4.

$x_{i}\parallel x_{j}$ and $y_{i}\parallel y_{j}$ and $x_{i}\parallel y_{j}$ , for every $1\leq i,j\leq k$ with $i\neq j$ .

Example 4.9.

Figure 7 shows two examples of patterns. In Figure 7(a) the sequence $w_{1}$ has the pattern $(s_{0},s_{0},s_{1},s_{1},s_{2},s_{2})$ , with $s_{0}\dashrightarrow s_{1}$ , $s_{1}\dashrightarrow s_{2}$ and $s_{2}\dashrightarrow s_{0}$ .

The pattern in Figure 7(b) is $(s_{0},s_{0},s_{1},s_{3})$ , with $s_{0}\dashrightarrow s_{1}$ , $s_{1}\prec s_{3}$ , and $s_{3}\parallel_{\mathrm{us}}s_{0}$ .

Proposition 4.10.

Let $\mathcal{A}$ be $1$ -schedulable CFM. If $\mathcal{A}$ is bad then there exists a trace $w\in\mathit{Tr}(\mathcal{A})$ that admits a pattern $(x_{1},y_{1},\ldots,x_{k},y_{k})$ .

Proof.

By Lemmas 4.7 and 4.8, there exists a trace $w\in\mathit{Tr}(\mathcal{A})$ such that $\texttt{msc}(w)$ contains a genuine $(\prec\cup\dashrightarrow\cup\ll^{w}_{\mathrm{us}})$ -cycle $\xi$ . Observe that $\xi$ necessarily contains a $\dashrightarrow$ arc. The reason is that $\prec$ and $\ll^{w}_{\mathrm{us}}$ are both contained in the total order over positions of $w$ , hence, there is no $(\prec\cup\ll^{w}_{\mathrm{us}})$ -cycle in $\texttt{msc}(w)$ . In order to transform $\xi=(e_{1},\ldots,e_{k})$ into a pattern, we insert “identity” arcs of the form $(e_{i},e_{i})$ as needed to get an alternating sequence $(x_{1},y_{1},\ldots,x_{k},y_{k})$ satisfying the first three conditions of the definition of patterns (recall that $\ll^{w}_{\mathrm{us}}$ is contained in $\parallel_{\mathrm{us}}$ ). The fourth (and last) condition holds because $\xi$ is genuine. $\hfill\blacktriangleleft$

(a) MSC of sequence

w_{1}=3!1(m_{0})\,2!3(m_{1})\,1!2(m_{2})

.

(b) MSC of sequence

w_{2}=4!1(m_{0})\,3!4(m_{1})\,3!2(m_{2})\,2?3(m_{2})\,2!1(m_{3})

.

Figure 7: Sequences with pattern, and their MSC.

Proposition 4.11.

Let $\mathcal{A}$ be $1$ -schedulable. If some $1$ -scheduling $w\in\mathit{Tr}(\mathcal{A})$ contains a pattern, then $\mathcal{A}$ is not send-synchronizable.

For the proof of Proposition 4.11 we first provide two technical lemmas. Recall that patterns are cycles. Proposition 4.11 will show a contradiction to send-synchronizability by listing the cycle in two ways. Lemma 4.12 identifies traces corresponding to different listings of the cycle in a such way that the part before the cycle is the same. Lemma 4.13 relates arcs of two equivalent traces with the same send-projection, one of which is rendez-vous.

Lemma 4.12.

Let $w\in\mathit{Tr}(\mathcal{A})$ contain some pattern $(x_{1},y_{1},\dots,x_{k},y_{k})$ . Let also $Z=\{x_{1},y_{1},\dots,x_{k},y_{k}\}$ . Then for every $1\leq i\leq k$ there exist $u,v,u^{\prime}\in\mathit{Act}^{*}$ with $uvu^{\prime}\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}w$ satisfying the following:

$\blacksquare$

$u$ is a linearization of $\mathit{Past}(Z)\setminus\mathit{Ftr}(Z)$
$\blacksquare$

$u v$ is a linearization of $\mathit{Past}(Z)$
$\blacksquare$

$v$ contains $x_{i},y_{i},\dots,x_{k},y_{k},x_{1},y_{1},\dots x_{i-1},y_{i-1}$ as subsequence.

Proof.

As in Lemma 4.7 we start with a prefix containing all events that are ordered causally before the events of the pattern: $u$ is a linearization of $\mathit{Past}(Z)\setminus\mathit{Ftr}(Z)$ .

Consider some $j,\ell\in\{1,\dots,k\}$ , $j\not=\ell$ . For readability we write $Z_{i}$ for the infix $\mathit{Past}(y_{i})\cap\mathit{Ftr}(x_{i})$ of $\texttt{msc}(w)$ , for every $i$ .

Let also $e\in Z_{j}$ and $f\in Z_{\ell}$ . If $e\preceq f$ would hold true then, using $f\preceq y_{\ell}$ and $x_{j}\preceq e$ , we would also get $x_{j}\preceq y_{\ell}$ , contradicting the definition of pattern. By symmetry, we conclude that $e\parallel f$ for all such $e, f$ .

Therefore, for $1\leq i\leq k$ we can define $v$ as linearization of $Z_{i},Z_{i+1},\dots Z_{k},Z_{1},\dots Z_{i-1}$ . By definition, $v$ contains the subsequence $x_{i},y_{i},\dots,x_{k},y_{k},x_{1},y_{1},\dots x_{i-1},y_{i-1}$ . $\hfill\blacktriangleleft$

Lemma 4.13.

Consider $w\in\mathit{Tr}(\mathcal{A})$ and $w^{\prime}\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ with ${w}|_{S}={w^{\prime}}|_{S}$ . Then for every send events $x\not=y$ in $w$ , with $x$ before $y$ in $w$ :

$\blacksquare$

If $x\dashrightarrow y$ in $w$ , then $x\mathop{<_{\mathbb{P}}}z$ , where $z$ is the matching receive of $y$ in $w^{\prime}$ : $(y,z)\in\mathop{\mathrm{msg}}$ .
$\blacksquare$

If $x\parallel_{\mathrm{us}}y$ in $w$ , then $x\mathop{<_{\texttt{mb}}}y$ in $w^{\prime}$ .
$\blacksquare$

If $x\prec y$ in $w$ then $x\prec y$ in $w^{\prime}$ by the same causal path.

Proof.

If $x\dashrightarrow y$ in $w$ , we know that $x$ is a send on some process $p$ and $y$ is an unmatched send to process $p$ . Because $w^{\prime}$ is a rendez-vous execution, with $x$ before $y$ , we get $x\mathop{<_{\mathbb{P}}}z$ .

Now suppose that $x\parallel_{\mathrm{us}}y$ in $w$ . Then $x$ and $y$ are two unmatched sends to the same process. The two sends are matched in $w^{\prime}$ , with $x^{\prime}\mathop{<_{\mathbb{P}}}y^{\prime}$ , where $(x,x^{\prime})\in\mathop{\mathrm{msg}},(y,y^{\prime})\in\mathop{\mathrm{msg}}$ . Thus $x\prec y$ in $w^{\prime}$ because of $\mathop{<_{\texttt{mb}}}$ .

Finally, if $x\prec y$ in $w$ , then $x\prec y$ holds also in $w^{\prime}$ because every arc of type $\mathop{<_{\mathbb{P}}},\mathop{\mathrm{msg}},\mathop{<_{\texttt{mb}}}$ on the causal path from $x$ to $y$ is preserved in $w^{\prime}$ . $\hfill\blacktriangleleft$

Proof of Proposition 4.11.

We assume that $\mathcal{A}$ is send-synchronizable, and consider some $w\in\mathit{Tr}(\mathcal{A})$ with pattern $(x_{1},y_{1},\dots,x_{k},y_{k})$ . We will assume that the pattern is minimal w.r.t. the following parameter: the size of the pattern is the sum of the lengths of the shortest paths from $x_{j}$ to $y_{j}$ , over all $j$ .

By Lemma 4.12 we can assume that $w=uv$ is a linearization of $\mathit{Past}(Z)$ , with $Z=\{x_{1},y_{1},\dots,x_{k},y_{k}\}$ , and $x_{1},y_{1},\dots,x_{k},y_{k}$ occurs as subsequence of $v$ . In addition, $u$ is linearization of $\mathit{Past}(Z)\setminus\mathit{Ftr}(Z)$ .

We know that $(x_{1},y_{1},\dots,x_{k},y_{k})$ is a pattern in $v$ , and we can assume w.l.o.g. that $y_{k}\dashrightarrow x_{1}$ . Note that $k>1$ since $x_{1}\preceq y_{1}$ (by definition of patterns) and $x_{1}\parallel y_{k}$ (by definition of $\dashrightarrow$ ). By Lemma 4.12, for every $1\leq i\leq k$ there exists some $v^{\prime}\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\equiv}}}v$ such that $x_{i+1},y_{i+1},\dots,x_{k},y_{k},x_{1},y_{1},\dots,x_{i},y_{i}$ is a subsequence of $v^{\prime}$ . Chose for example $i=1$ .

As $\mathcal{A}$ is send-synchronizable, there exist $z,z^{\prime}\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ such that ${(uv)}|_{S}={z}|_{S}$ and ${(uv^{\prime})}|_{S}={z^{\prime}}|_{S}$ . From Lemma 4.13, we get that there exists a $(\prec\cup\mathop{\mathrm{msg}}^{-1})^{*}$ -path from $x_{1}$ to $y_{k}$ in $z$ not going through $\mathit{rcv}(x_{1})$ , the receive matching $x_{1}$ . Indeed, for each $1\leq i\leq k$ , we have $x_{i}\prec y_{i}$ in $w$ , so we still have it in $z$ and it does not go through $\mathit{rcv}(x_{1})$ . We also have $y_{i}\dashrightarrow x_{i+1}$ or $y_{i}\parallel_{\mathrm{us}}x_{i+1}$ in $w$ , for every $i$ . If $y_{i}\dashrightarrow x_{i+1}$ then $y_{i}\mathop{<_{\mathbb{P}}}\mathit{rcv}(x_{i+1})\mathop{\mathrm{msg}}^{-1}x_{% i+1}$ in $z$ . If $y_{i}\parallel_{\mathrm{us}}x_{i+1}$ , then $y_{i}\mathop{<_{\texttt{mb}}}x_{i+1}$ in $z$ . In both cases the arcs do not use $\mathit{rcv}(x_{1})$ .

We inspect now $M:=\texttt{msc}(z)$ . Let $p$ be the process of the send $y_{k}$ (recall that it is also the process of $\mathit{rcv}(x_{1}$ ), because $y_{k}\dashrightarrow x_{1}$ ). Because of pattern minimality, we can show that the only send event on $p$ in $v$ is $y_{k}$ . Suppose that some $s\not=y_{k}$ is a send on process $p$ with $s$ in $v$ . By definition of $u, v$ , we have $x_{k}\preceq s\prec y_{k}$ . But then the pattern $(x_{1},y_{1},\dots,x_{k},s)$ would be smaller, contradiction. Again by minimality, we can show that the only send to $p$ in $v$ is $x_{1}$ . First there is no matched send to $p$ in $v$ , because such a send $s$ would satisfy $s\prec x_{1}$ as $x_{1}$ is an unmatched send to $p$ , hence, if $x_{j}\preceq s\preceq y_{j}$ with $1\leq j\leq k$ , then $x_{j}\prec x_{1}$ , which is forbidden by the definition of patterns. Now if we had some $s\not=x_{1}$ unmatched send event to $p$ , with say $x_{j}\preceq s\preceq y_{j}$ and $1\leq j<k$ , then the pattern $(s,y_{j},\dots,x_{k},y_{k})$ would be smaller. Finally, if $j=k$ , so $x_{k}\preceq s\prec y_{k}$ , then the predecessor of $s$ on the causal path from $x_{k}$ to $s$ is an event on $p$ , and we can shorten path from $x_{k}$ to $y_{k}$ , obtaining a smaller pattern.

Let us construct $z^{\sharp}$ from $z$ by moving $\mathit{rcv}(x_{1})$ at the end of the sequence. Observe that $z=\mathit{match}({z}|_{S})=\mathit{match}({u}|_{S})\mathit{match}({v}|_{S})$ and similarly $z^{\prime}=\mathit{match}({u}|_{S})\mathit{match}({v^{\prime}}|_{S})$ , where $\mathit{match}:S^{*}\rightarrow\mathit{Act}^{*}$ is the morphism defined by $\mathit{match}(p!q(m))=p!q(m)\,q?p(m)$ . We derive from the previous paragraph that the sequence of actions by $p$ is $\mathit{rcv}(x_{1})y_{k}$ in $\mathit{match}({v}|_{S})$ and $y_{k}\mathit{rcv}(x_{1})$ in $\mathit{match}({v^{\prime}}|_{S})$ . As $\mathit{rcv}(x_{1})$ is the last receive by $p$ in $z$ , moving it at the end of the sequence preserves viability, so $z^{\sharp}$ is viable. Moreover, the sequence of actions by $p$ in $z^{\sharp}$ coincides with that of $z^{\prime}$ , and the sequence of actions by $q\neq p$ in $z^{\sharp}$ coincides with that of $z$ . Since $z\in\mathit{Tr}(\mathcal{A})$ and $z^{\prime}\in\mathit{Tr}(\mathcal{A})$ , we get that $z^{\sharp}\in\mathit{Tr}(\mathcal{A})$ .

However, note that now there is a $(\prec\cup\mathop{\mathrm{msg}}^{-1})$ -cycle with at least two distinct sends in $M^{\sharp}:=\texttt{msc}(z^{\sharp})$ . Indeed, we still have in $M^{\sharp}$ the $(\prec\cup\mathop{\mathrm{msg}}^{-1})^{+}$ -path of $M$ from $x_{1}$ to $y_{k}$ , as this path does not go through $\mathit{rcv}(x_{1})$ , and $y_{k}\mathop{<_{\mathbb{P}}}\mathit{rcv}(x_{1})$ in $M^{\sharp}$ , finishing the cycle with $(\mathit{rcv}(x_{1}),x_{1})\in\mathop{\mathrm{msg}}^{-1}$ . So $z^{\sharp}$ is not $1$ -schedulable because it contains a non-trivial $(\prec\cup\mathop{\mathrm{msg}}^{-1})^{+}$ -cycle with at least two sends, which contradicts our assumption that $\mathcal{A}$ is $1$ -schedulable. $\hfill\blacktriangleleft$

4.3 Wrap-Up

In this section, we prove that send-synchronizability is decidable for $1$ -schedulable CFMs, by assembling the results from the previous subsections. We start with the following observation, which is an immediate consequence of Propositions 4.5, 4.10, and 4.11.

Proposition 4.14.

For every $1$ -schedulable CFM $\mathcal{A}$ , it holds that $\mathcal{A}$ is send-synchronizable if, and only if, (1) $\mathcal{A}$ is good, (2) ${\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})}|_{S}={\{w\in\mathit{Tr}(\mathcal{A})% \mid w\text{ is a {\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb% }{0,0,0.7}$1$-scheduling}}\}}|_{S}$ and (3) ${\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})}|_{S}$ is closed under $\mathit{SI}$ .

Proposition 4.15.

It is decidable to check if a $1$ -schedulable CFM is good.

Proof sketch..

Let $\mathcal{A}$ be a $1$ -schedulable CFM. From Proposition 4.10, we know that $\mathcal{A}$ is bad if there exists a trace with a pattern. The existence of a pattern can be checked on a $1$ -scheduling, as by construction two equivalent traces have the same patterns, and $\mathcal{A}$ is $1$ -schedulable. Moreover the set of $1$ -scheduling of $\mathcal{A}$ is regular.

We guess a bad $1$ -scheduling on-the-fly, together with the sends that form the pattern. We can assume that the pattern occurs in the order of the sequence. If there exists some bad trace in $\mathit{Tr}(\mathcal{A})$ , then there is one with a pattern of size at most $2\times|\mathbb{P}|$ , as otherwise there would be at least three sends of the pattern on the same process, and we would have a shortcut.

Let $(x_{1},y_{1},\dots,x_{k},y_{k})$ be the pattern we read. We need to check that

$\blacksquare$

for each $0\leq i\leq k$ , $x_{i}\preceq y_{i}$ and $y_{i}\parallel x_{i+1}$ with either $\dashrightarrow$ or $\parallel_{\mathrm{us}}$ , and at least one $\dashrightarrow$ -arc.
$\blacksquare$

and for each $0\leq i,j\leq k$ with $i\not=j$ , $x_{i}\parallel x_{j}$ and $y_{i}\parallel y_{j}$ and $x_{i}\parallel y_{j}$ .

To do so, we will keep for each send $s$ of the pattern the set of processes with actions causally ordered after $s$ , and we will update these sets while reading the bad $1$ -scheduling. So we need a memory of size $O(|\mathbb{P}|^{2})$ . $\hfill\blacktriangleleft$

From the two previous propositions, we get the following theorem.

Theorem 4.16.

The question whether a $1$ -schedulable CFM is send-synchronizable is Pspace-complete.

Proof.

Let $\mathcal{A}$ be a $1$ -schedulable CFM. From Proposition 4.15, we know that we can check in polynomial space if $\mathcal{A}$ is good. The two sets $\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ and $\{w\in\mathit{Tr}(\mathcal{A})\mid w\text{ is a {\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}$1$-scheduling}}\}$ are regular, so we can check in Pspace if they are equal. And from Remark 4.3, we know that we can check if ${\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})}|_{S}$ is closed under $\mathit{SI}$ in Pspace.

For Pspace-hardness, we reduce from the automata intersection problem as in [8], with a send that cannot be received if the intersection of the automata is not empty. $\hfill\blacktriangleleft$

5 Conclusion

We showed that send-synchronizability for mailbox CFMs is undecidable, thus closing the question left open in [11, 9]. We also showed that we can decide in Pspace if a $1$ -schedulable CFM (which is a property that can be checked in Pspace) is send-synchronizable. We think that the techniques developed for the proof could be used to answer others problems for mailbox CFMs, like the realizability problem. Moreover, even if the class of $1$ -schedulable systems is decidable, it is quite restrictive. It can be interesting to see if our techniques can be used for $k$ -schedulable CFMs and the more general class of CFMs studied in [8].

References

[1] Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996. doi:10.1006/INCO.1996.0053.
[2] Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Sadagopan Srinivasan, Krithi Ramamritham, Arun Kumar, M. P. Ravindra, Elisa Bertino, and Ravi Kumar, editors, Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, pages 795–804. ACM, 2011. doi:10.1145/1963405.1963516.
[3] Samik Basu and Tevfik Bultan. On deciding synchronizability for asynchronously communicating systems. Theoretical Computer Science, 656:60–75, 2016. doi:10.1016/J.TCS.2016.09.023.
[4] Samik Basu, Tevfik Bultan, and Meriem Ouederni. Synchronizability for verification of asynchronously communicating systems. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 56–71. Springer, 2012. doi:10.1007/978-3-642-27940-9_5.
[5] Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Étienne Lozes, and Amrita Suresh. A unifying framework for deciding synchronizability. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 14:1–14:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.14.
[6] Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 372–391. Springer, 2018. doi:10.1007/978-3-319-96142-2_23.
[7] Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983. doi:10.1145/322374.322380.
[8] Romain Delpy, Anca Muscholl, and Grégoire Sutre. An automata-based approach for synchronizable mailbox communication. In 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada, volume 311 of LIPIcs, pages 22:1–22:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CONCUR.2024.22.
[9] Cinzia Di Giusto, Laetitia Laversa, and Kirstin Peters. Synchronisability in mailbox communication. In Proceedings Combined 31st International Workshop onTheoretical Computer Science Expressiveness in Concurrencyand 21st Workshop on Structural Operational Semantics, Calgary, Canada, 9th September 2024, volume 412 of Electronic Proceedings in Theoretical Computer Science, pages 19–34. Open Publishing Association, 2024. doi:10.4204/EPTCS.412.3.
[10] Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 122:1–122:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPICS.ICALP.2017.122.
[11] Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. Logical Methods in Computer Science, 19(4), 2023. doi:10.46298/LMCS-19(4:33)2023.
[12] Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63–92, 2001. doi:10.1016/S0304-3975(00)00102-X.
[13] Xiang Fu, Tevfik Bultan, and Jianwen Su. Synchronizability of conversations among web services. IEEE Transactions on Software Engineering, 31(12):1042–1055, 2005. doi:10.1109/TSE.2005.141.
[14] Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147–167, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
[15] Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Étienne Lozes. A partial order view of message-passing communication models. Proceedings of the ACM on Programming Languages, 7(POPL):1601–1627, 2023. doi:10.1145/3571248.
[16] Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. On the k-synchronizability of systems. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 157–176. Springer, 2020. doi:10.1007/978-3-030-45231-5_9.
[17] Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. International Journal of Foundations of Computer Science, 34(8):1051–1076, 2023. doi:10.1142/S0129054122430018.
[18] Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1–38, 2005. doi:10.1016/J.IC.2004.08.004.
[19] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
[20] Dietrich Kuske and Anca Muscholl. Communicating automata. In Handbook of Automata Theory, pages 1147–1188. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. doi:10.4171/AUTOMATA-2/9.
[21] Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, 1978. doi:10.1145/359545.359563.
[22] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 350–373. Springer, 2023. doi:10.1007/978-3-031-37709-9_17.
[23] Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 35:1–35:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.35.
[24] Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 32:1–32:31. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ECOOP.2023.32.

Appendix A $1$ -schedulability and related notions

Similar notions to $1$ -schedulability can be found in several papers [5, 17]. The way unmatched sends are treated in the literature may differ in a significant way. Our notion of $1$ -schedulable is the same as strongly $1$ -synchronisable in [5]. The notion of RSC in [15] is more restrictive than $1$ -schedulable, as it does not allow to permute two unmatched sends to the same process.

Take as an example the trace 0!2(a) 0!1(b) 2!1(c) 2?0(a). It is $1$ -schedulable since it is equivalent to 2!1(c) 0!2(a) 2?0(a) 0!1(b). But it is not RSC according to [15], since RSC disallows permuting 0!1(b), 2!1(c). Note however that every $1$ -scheduling is an RSC execution.

Appendix B A necessary and sufficient condition for send-synchronizability

Let $\mathcal{A}$ be a CFM. Recall that $\mathcal{A}$ is send-synchronizable if, and only if, for every trace $u\in\mathit{Tr}(\mathcal{A})$ , there exists a trace $v\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ with ${u}|_{S}={v}|_{S}$ . In fact, the trace $v$ is unique if it exists. Indeed, the only candidate for $v$ is $\mathit{match}({u}|_{S})$ . Recall that $\mathit{match}:S^{*}\rightarrow\mathit{Act}^{*}$ is the morphism defined by $\mathit{match}(p!q(m))=p!q(m)\,q?p(m)$ . Observe that ${\mathit{match}(u)}|_{S}=u$ for all $u\in S^{*}$ . This leads us to the characterization of send-synchronizability in Lemma B.1 below. The following notations are used in this lemma. For every process $p\in\mathbb{P}$ , $L(\mathcal{A}_{p})$ is the language of the LTS $\mathcal{A}_{p}$ (viewed as a non-deterministic automaton with every state final) and ${u}_{|p}$ is the projection of $u\in\mathit{Act}^{*}$ on $\mathit{Act}_{p}$ .

Lemma B.1.

A CFM $\mathcal{A}$ is send-synchronizable if, and only if, for every trace $u\in\mathit{Tr}(\mathcal{A})$ , the sequence $v=\mathit{match}({u}|_{S})$ satisfies ${v}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\mathbb{P}$ .

Proof.

Assume that $\mathcal{A}$ is send-synchronizable. Let $u\in\mathit{Tr}(\mathcal{A})$ and define $v=\mathit{match}({u}|_{S})$ . Since $\mathcal{A}$ is send-synchronizable, there exists $u^{\prime}\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ such that ${u}|_{S}={u^{\prime}}|_{S}$ . We have $\mathit{match}({u^{\prime}}|_{S})=u^{\prime}$ since $u^{\prime}\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ . It follows that $u^{\prime}=v$ , hence, $v\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ . This entails that ${v}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\mathbb{P}$ .

Conversely, let $u\in\mathit{Tr}(\mathcal{A})$ and assume that $v=\mathit{match}({u}|_{S})$ satisfies ${v}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\mathbb{P}$ . The sequence $v$ is clearly rendez-vous, according to the definition of $\mathit{match}$ . We derive that $v\in\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})$ , since ${v}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\mathbb{P}$ . The observation that ${v}|_{S}={\mathit{match}({u}|_{S})}|_{S}={u}|_{S}$ entails that ${u}|_{S}\in{\mathit{Tr}_{\texttt{rdv}}(\mathcal{A})}|_{S}$ , which concludes the proof. $\hfill\blacktriangleleft$

Appendix C Proofs of Section 3

Lemma 3.1. [Restated, see original statement.]

If $\mathcal{I}$ is a positive instance of Pre-MPCP then there is an initial execution in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ leading to the configuration $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ .

Proof.

Consider a sequence of indices $i_{1},\ldots,i_{k}\in\{1,\ldots,K\}$ , with $k\geq 1$ , such that $i_{1}=1$ , $x_{i_{1}}\cdots x_{i_{k}}=y_{i_{1}}\cdots y_{i_{k}}$ and $|x_{i_{1}}\cdots x_{i_{j}}|\geq|y_{i_{1}}\cdots y_{i_{j}}|$ for every $j\in\{1,\ldots,k\}$ . Let us write $a_{1}\cdots a_{n}$ , with $a_{i}\in\Sigma$ , the word $x_{i_{1}}\cdots x_{i_{k}}$ (or, equivalently, the word $y_{i_{1}}\cdots y_{i_{k}}$ ). Define $e_{j}=|x_{i_{1}}\cdots x_{i_{j}}|$ and $f_{j}=|y_{i_{1}}\cdots y_{i_{j}}|$ , for every $j\in\{1,\ldots,k\}$ . We also put $e_{0}=f_{0}=0$ . Our assumptions on $i_{1},\ldots,i_{k}$ entail, firstly, that $e_{k}=f_{k}=n$ , and, secondly, that $e_{j}\geq f_{j}$ , $x_{i_{j}}=a_{e_{j-1}+1}\cdots a_{e_{j}}$ and $y_{i_{j}}=a_{f_{j-1}+1}\cdots a_{f_{j}}$ , for all $j\in\{1,\ldots,k\}$ .

We show that for every $j\in\{1,\ldots,k\}$ , there is an execution $\rho_{j}$ in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ from the configuration $(N,N,N;\varepsilon,v^{R}_{j},v^{V}_{j})$ , with $v^{R}_{j}=a_{f_{j-1}+1}\cdots a_{e_{j-1}}$ and $v^{V}_{j}=a_{1}\overline{a_{1}}\cdots a_{f_{j-1}}\overline{a_{f_{j-1}}}$ , to the configuration $(N,N,N;\varepsilon,w^{R}_{j},w^{V}_{j})$ , with $w^{R}_{j}=a_{f_{j}+1}\cdots a_{e_{j}}$ and $w^{V}_{j}=a_{1}\overline{a_{1}}\cdots a_{f_{j}}\overline{a_{f_{j}}}$ . In the execution $\rho_{j}$ , the sequence of actions performed by $G$ is $G!R(x_{i_{j}})\,G!V(\overline{y_{i_{j}}})$ , the sequences of receive and send actions performed by $R$ are $R?G(y_{i_{j}})$ and $R!V(y_{i_{j}})$ , respectively, and $V$ does not move. These sequences of actions are permitted by the LTSes $\mathcal{A}_{G}$ and $\mathcal{A}_{R}$ (see Figures 2 and 3). To make it clear that such an execution $\rho_{j}$ exists, we need to show that these actions can be interleaved in a way that produces an viable sequence (that is, in addition, permitted by the LTS $\mathcal{A}_{R}$ ). To reduce clutter, we define $b_{1}=a_{f_{j-1}+1},\ldots,b_{m}=a_{f_{j}}$ , where $m=f_{j}-f_{j-1}$ . Note that $y_{i_{j}}=b_{1}\cdots b_{m}$ . Formally, the viable sequence labeling the execution $\rho_{j}$ is

G!R(x_{i_{j}})\,\cdot\,R?G(b_{1})\,R!V(b_{1})\,G!V(\overline{b_{1}})\,\cdots\,% R?G(b_{m})\,R!V(b_{m})\,G!V(\overline{b_{m}})

This sequence is viable because the contents $z$ of $R$ ’s mailbox after $G!R(x_{i_{j}})$ verifies $z=v^{R}_{j}\cdot x_{i_{j}}=a_{f_{j-1}+1}\cdots a_{e_{j}}$ , hence, $z$ admits $b_{1}\cdots b_{m}$ as prefix, since $b_{1}\cdots b_{m}=a_{f_{j-1}+1}\cdots a_{f_{j}}$ and $e_{j}\geq f_{j}$ . It is readily seen that the configuration $(N,N,N;\varepsilon,w^{R}_{j},w^{V}_{j})$ obtained after $\rho_{j}$ verifies $w^{R}_{j}=a_{f_{j}+1}\cdots a_{e_{j}}$ and $w^{V}_{j}=a_{1}\overline{a_{1}}\cdots a_{f_{j}}\overline{a_{f_{j}}}$ .

We also observe that there is an execution $\rho_{k+1}$ in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ from the configuration $(N,N,N;\varepsilon,\varepsilon,v^{V}_{k})$ , with $v^{V}_{k}=a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}$ , to the configuration $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ . The trace of $\rho_{k+1}$ is the viable sequence $V?R(a_{1})\,V?G(\overline{a_{1}})\,\cdots\,V?R(a_{n})\,V?G(\overline{a_{n}})$ . This sequence of actions is permitted by the LTS $\mathcal{A}_{V}$ (see Figure 4).

By concatenating the executions $\rho_{1},\ldots,\rho_{k+1}$ , we get an execution from $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ to $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ . But this execution does not start from the initial configuration of $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ . Along the execution $\rho_{1}$ , $G$ does $G!R(x_{1})G!V(\overline{y_{1}})$ , since $i_{1}=1$ . So $G$ could as well have started from its initial state. Obviously, the same goes for $R$ and $V$ , since they can move silently from their initial state to the state $N$ . Hence, there exists an execution $\rho^{\prime}_{1}$ from the initial configuration of $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ to the configuration obtained after $\rho_{1}$ . The concatenation $\rho^{\prime}_{1}\rho_{2}\cdots\rho_{K}$ provides an initial execution leading to the configuration $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ . $\hfill\blacktriangleleft$

Corollary 3.2. [Restated, see original statement.]

If $\mathcal{I}$ is a positive instance of Pre-MPCP then there is a trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ containing the action $R!V(\#)$ , hence, $\mathcal{A}(\mathcal{I})$ is not send-synchronizable.

Proof.

Starting from the configuration $(N,N,N;\varepsilon,\varepsilon,\varepsilon)$ , there is an execution in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ labelled by

G!R(\$)\,R?G(\$)\,R!V(\$)\,G!V(\overline{\$})\,V?R(\$)\,V?G(\overline{\$})\,V!% G(\#)\,G?V(\#)\,G!R(\#)\,R?G(\#)\,R!V(\#)\>.

If $\mathcal{I}$ is a positive instance of Pre-MPCP then, according to Lemma 3.1 and the above observation, there is a trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ ending with $R!V(\#)$ . Obviously, it holds that ${u}|_{S}\in{\mathit{Tr}(\mathcal{A}(\mathcal{I}))}|_{S}$ . But, as $V$ contains no $V?R(\#)$ transition, no trace in $\mathit{Tr}_{\texttt{rdv}}(\mathcal{A}(\mathcal{I}))$ contains the action $R!V(\#)$ . Hence, ${u}|_{S}\not\in{\mathit{Tr}_{\texttt{rdv}}(\mathcal{A}(\mathcal{I}))}|_{S}$ , which entails that $\mathcal{A}(\mathcal{I})$ is not send-synchronizable. $\hfill\blacktriangleleft$

Lemma 3.3. [Restated, see original statement.]

If there is a trace in $\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ containing the action $R!V(\#)$ then $\mathcal{I}$ is a positive instance of Pre-MPCP.

Proof.

Consider an initial execution $\rho$ in $\mathcal{T}(\mathcal{A}(\mathcal{I}))$ ending with the action $R!V(\#)$ . By construction, $\rho$ also necessarily contains $R?G(\#)$ , hence, it also contains $G!R(\#)$ and $G?V(\#)$ , which entails that it contains $V!G(\#)$ . Therefore, in the execution $\rho$ , the processes $R$ and $V$ have each selected the normal mode, since there is no $R!V(\#)$ transition nor $V!G(\#)$ transition in the dummy modes. Let $\pi$ denote the prefix of $\rho$ that ends just before the $V!G(\#)$ action, and let $u$ denote the trace labelling $\pi$ . According to the definition of the LTSes $\mathcal{A}_{G}$ , $\mathcal{A}_{R}$ and $\mathcal{A}_{V}$ (see Figures 2, 3, and 4), the projections ${u}_{|G}$ , ${u}_{|R}$ and ${u}_{|V}$ are as follows:

	$\displaystyle{u}_{\|G}$	$\displaystyle\ =\ G!R(x_{i_{1}})\,G!V(\overline{y_{i_{1}}})\,\cdots\,G!R(x_{i_% {k}})\,G!V(\overline{y_{i_{k}}})\,\cdot\,G!R(\$)\,G!V(\overline{\$})$
	$\displaystyle{u}_{\|R}$	$\displaystyle\ =\ R?G(b_{1})\,R!V(b_{1})\,\cdots\,R?G(b_{m})\,R!V(b_{m})\,% \cdot\,\alpha$
	$\displaystyle{u}_{\|V}$	$\displaystyle\ =\ V?R(a_{1})\,V?G(\overline{a_{1}})\,\cdots\,V?R(a_{n})\,V?G(% \overline{a_{n}})\,\cdot\,V?R(\$)\,V?G(\overline{\$})$

for some $i_{1},\ldots,i_{k}\in\{1,\ldots,K\}$ with $k\geq 1$ and $i_{1}=1$ , some $a_{1},\ldots,a_{n}\in\Sigma$ with $n\geq 0$ , some $b_{1},\ldots,b_{m}\in(\Sigma\cup\{\$,\#\})$ with $m\geq 0$ , and some $\alpha$ that is either $\varepsilon$ or a receive action $R?G(\cdot)$ . The word $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ received by $V$ is a prefix of a shuffle of the word $b_{1}\cdots b_{m}$ sent by $R$ to $V$ and of the word $\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}\overline{\$}$ sent by $G$ to $V$ . So $a_{1}\cdots a_{n}\$$ is a prefix of $b_{1}\cdots b_{m}$ and $\overline{a_{1}}\cdots\overline{a_{n}}\overline{\$}$ is a prefix of $\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}\overline{\$}$ . Since $\overline{\$}$ does not occur in $\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}$ , we get that $a_{1}\cdots a_{n}=y_{i_{1}}\cdots y_{i_{k}}$ . Similarly, the word $b_{1}\cdots b_{m}$ received by $R$ is a prefix of the word $x_{i_{1}}\cdots x_{i_{k}}\$$ sent by $G$ to $R$ . We derive that $a_{1}\cdots a_{n}\$$ is a prefix of $x_{i_{1}}\cdots x_{i_{k}}\$$ . Since $\$$ does not occur in $x_{i_{1}}\cdots x_{i_{k}}$ , this entails that $a_{1}\cdots a_{n}\$=b_{1}\cdots b_{m}=x_{i_{1}}\cdots x_{i_{k}}\$$ . We have shown that $x_{i_{1}}\cdots x_{i_{k}}=y_{i_{1}}\cdots y_{i_{k}}$ . It remains to prove that $|x_{i_{1}}\cdots x_{i_{j}}|\geq|y_{i_{1}}\cdots y_{i_{j}}|$ for all $j\in\{1,\ldots,k\}$ . Before that, we observe that every send action to $V$ is matched in $u$ . Indeed, the length of the word $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ received by $V$ is $2(n+1)$ , and the length of the word sent to $V$ is $|b_{1}\cdots b_{m}|+|\overline{y_{i_{1}}}\cdots\overline{y_{i_{k}}}\overline{% \$}|=2m=2(n+1)$ . This means that the sequence of send actions to $V$ in $u$ is $R!V(b_{1})\,G!V(\overline{b_{1}})\,\cdots\,R!V(b_{m})\,G!V(\overline{b_{m}})$ .

We now show that $|x_{i_{1}}\cdots x_{i_{j}}|\geq|y_{i_{1}}\cdots y_{i_{j}}|$ for all $j\in\{1,\ldots,k\}$ . Let $j\in\{1,\ldots,k\}$ and consider a prefix $u_{j}$ of $u$ such that ${u_{j}}_{|G}=G!R(x_{i_{1}})\,G!V(\overline{y_{i_{1}}})\,\cdots\,G!R(x_{i_{j}})% \,G!V(\overline{y_{i_{j}}})$ . The projection of $u_{j}$ on $\mathit{Act}_{R}$ may be written as ${u_{j}}_{|R}=R?G(b_{1})\,R!V(b_{1})\,\cdots\,R?G(b_{h})\,R!V(b_{h})\,\cdot\,\beta$ for some $h\in\{0,\ldots,m\}$ and some $\beta$ that is either $\varepsilon$ or a receive action $R?G(\cdot)$ . The word $b_{1}\cdots b_{h}$ received by $R$ is a prefix of the word $x_{i_{1}}\cdots x_{i_{j}}$ sent by $G$ to $R$ , so $|x_{i_{1}}\cdots x_{i_{j}}|\geq h$ . Now, the word sent to $V$ in $u_{j}$ , say $z$ , is a shuffle of the word $b_{1}\cdots b_{h}$ sent by $R$ to $V$ and of the word $\overline{y_{i_{1}}}\cdots\overline{y_{i_{j}}}$ sent by $G$ to $V$ . The word $z$ is also a prefix of the word $b_{1}\overline{b_{1}}\cdots b_{m}\overline{b_{m}}$ sent to $V$ in $u$ . This entails that $|b_{1}\cdots b_{h}|=|\overline{y_{i_{1}}}\cdots\overline{y_{i_{j}}}|$ or $|b_{1}\cdots b_{h}|=|\overline{y_{i_{1}}}\cdots\overline{y_{i_{j}}}|+1$ . It follows that $h\geq|y_{i_{1}}\cdots y_{i_{j}}|$ and we conclude that $|x_{i_{1}}\cdots x_{i_{j}}|\geq h\geq|y_{i_{1}}\cdots y_{i_{j}}|$ . $\hfill\blacktriangleleft$

Lemma 3.4. [Restated, see original statement.]

For every trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ , if $u$ does not contain the action $R!V(\#)$ then ${\mathit{match}({u}|_{S})}_{|p}\in L(\mathcal{A}_{p})$ for every process $p\in\{G,R,V\}$ .

Proof.

Let $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ such that $u$ does not contain the action $R!V(\#)$ . We consider each process in $\mathbb{P}=\{G,R,V\}$ separately. Recall that the LTSes $\mathcal{A}_{G}$ , $\mathcal{A}_{R}$ and $\mathcal{A}_{V}$ of the processes $G$ , $R$ and $V$ are defined in Figures 2, 3, and 4.

Let us start with the guesser process. According to the definition of $\mathcal{A}_{G}$ , there exists a sequence of indices $i_{1},\ldots,i_{k}\in\{1,\ldots,K\}$ , with $k\geq 1$ and $i_{1}=1$ , such that the sequence of send actions performed by $G$ in $u$ is a prefix of $v\cdot G!R(\$)\,G!V(\overline{\$})\,G!R(\#)$ , where $v=G!R(x_{i_{1}})\,G!V(\overline{y_{i_{1}}})\,\cdots\,G!R(x_{i_{k}})\,G!V(% \overline{y_{i_{k}}})$ . According to the definition of $\mathcal{A}_{R}$ and $\mathcal{A}_{V}$ , the sequence of send actions to $G$ in $u$ is either empty or the single action $V!G(\#)$ . Moreover, if $u$ contains $V!G(\#)$ then this action is necessarily after $G!V(\overline{\$})$ and before $G!R(\#)$ . This is due to the receive actions $V?G(\overline{\$})$ and $G?V(\#)$ . We derive that ${\mathit{match}({u}|_{S})}_{|G}$ is a prefix of $v\cdot G!R(\$)\,G!V(\overline{\$})\,G?V(\#)\,G!R(\#)$ and conclude that ${\mathit{match}({u}|_{S})}_{|G}\in L(\mathcal{A}_{G})$ .

We now proceed to the relayer process. According to the definition of $\mathcal{A}_{G}$ and $\mathcal{A}_{V}$ , the sequence of send actions to $R$ in $u$ is a prefix of a sequence of the form $G!R(a_{1})\,\cdots\,G!R(a_{n})\,\cdot\,G!R(\$)\,G!R(\#)$ , with $n\geq 0$ and $a_{i}\in\Sigma$ . So the word sent to $R$ in $u$ is a prefix of $a_{1}\cdots a_{n}\$\#$ . This entails that the sequence of send actions performed by $R$ in $u$ is in the language $\{R!V(a)\mid a\in\Sigma\}^{*}\cdot\{\varepsilon,R!V(\$)\}$ , according to the definition of $\mathcal{A}_{R}$ . Indeed, either $R$ selects the normal mode, in which case the word sent by $R$ to $V$ is a prefix of the word $a_{1}\cdots a_{n}\$$ (recall that $u$ does not contain the action $R!V(\#)$ by assumption), or $R$ selects the dummy mode, in which case the word sent by $R$ to $V$ is in the language $\Sigma^{*}\cdot\{\varepsilon,\$\}$ . We derive that the projection of $u$ on sends by $R$ , or to $R$ , is in the shuffle of the language $\{R!V(a)\mid a\in\Sigma\}^{*}\cdot\{\varepsilon,R!V(\$)\}$ and the language $\{G!R(m)\mid m\in\Sigma\cup\{\$,\#\}\}^{*}$ . It follows that ${\mathit{match}({u}|_{S})}_{|R}$ is in the shuffle of the language $\{R!V(a)\mid a\in\Sigma\}^{*}\cdot\{\varepsilon,R!V(\$)\}$ and the language $\{R?G(m)\mid m\in\Sigma\cup\{\$,\#\}\}^{*}$ . We conclude that ${\mathit{match}({u}|_{S})}_{|R}\in L(\mathcal{A}_{R})$ , by letting $R$ select the dummy mode.

Let us finally address the verifier process. We consider two cases, depending on whether $u$ contains the action $V!G(\#)$ or not. If $u$ does not contain the action $V!G(\#)$ , then $V$ does not perform any send action in $u$ , according to the definition of $\mathcal{A}_{V}$ . The projection of $u$ on sends to $V$ is in the language $\left(\{G!V(\overline{m})\mid m\in\Sigma\cup\{\$\}\}\cup\{R!V(m)\mid m\in% \Sigma\cup\{\$\}\}\right)^{*}$ , according to the definition of $\mathcal{A}_{G}$ and $\mathcal{A}_{R}$ (recall that $u$ does not contain the action $R!V(\#)$ by assumption). It follows that ${\mathit{match}({u}|_{S})}_{|V}$ is in the language $\left(\{V?G(\overline{m})\mid m\in\Sigma\cup\{\$\}\}\cup\{V?R(m)\mid m\in% \Sigma\cup\{\$\}\}\right)^{*}$ . We conclude that ${\mathit{match}({u}|_{S})}_{|V}\in L(\mathcal{A}_{V})$ , by letting $V$ select the dummy mode.

Assume now that $u$ contains the action $V!G(\#)$ . According to the definition of $\mathcal{A}_{V}$ , this means that ${u}_{|V}$ is equal to $V?R(a_{1})\,V?G(\overline{a_{1}})\,\cdots\,V?R(a_{n})\,V?G(\overline{a_{n}})\,% \cdot\,V?R(\$)\,V?G(\overline{\$})\,V!G(\#)$ for some $a_{1},\ldots,a_{n}\in\Sigma$ with $n\geq 0$ . The mailbox semantics entails that the word sent to $V$ in $u$ admits $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ as a prefix. When we dealt about the relayer process, we showed that the word sent by $R$ to $V$ is in the language $\Sigma^{*}\cdot\{\varepsilon,\$\}$ . Moreover, according to the definition of $\mathcal{A}_{G}$ , the word sent by $G$ to $V$ is in the language $\overline{\Sigma}^{*}\cdot\{\varepsilon,\overline{\$}\}$ . So the word sent to $V$ in $u$ is exactly $a_{1}\overline{a_{1}}\cdots a_{n}\overline{a_{n}}\$\overline{\$}$ . We derive that the sequence of send actions to $V$ in $u$ is $v=R!V(a_{1})\,G!V(\overline{a_{1}})\,\cdots\,R!V(a_{n})\,G!V(\overline{a_{n}})% \,\cdot\,R!V(\$)\,G!V(\overline{\$})$ . Moreover, the single send action performed by $V$ , namely $V!G(\#)$ , is necessarily after $G!V(\overline{\$})$ . This is due to the receive action $V?G(\overline{\$})$ . It follows that ${\mathit{match}({u}|_{S})}_{|V}$ is equal to $V?R(a_{1})\,V?G(\overline{a_{1}})\,\cdots\,V?R(a_{n})\,V?G(\overline{a_{n}})\,% \cdot\,V?R(\$)\,V?G(\overline{\$})\,V!G(\#)$ , hence, ${\mathit{match}({u}|_{S})}_{|V}={u}_{|V}$ . We conclude that ${\mathit{match}({u}|_{S})}_{|V}\in L(\mathcal{A}_{V})$ . $\hfill\blacktriangleleft$

Corollary 3.5. [Restated, see original statement.]

If $\mathcal{I}$ is a negative instance of Pre-MPCP then $\mathcal{A}(\mathcal{I})$ is send-synchronizable.

Proof.

If $\mathcal{I}$ is a negative instance of Pre-MPCP then we derive from Lemma 3.3 that no trace in $\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ contains the action $R!V(\#)$ . It follows from Lemma 3.4 that ${\mathit{match}({u}|_{S})}_{|p}\in L(\mathcal{A}_{p})$ for every trace $u\in\mathit{Tr}(\mathcal{A}(\mathcal{I}))$ and every process $p\in\{G,R,V\}$ . We conclude thanks to Lemma B.1 that $\mathcal{A}(\mathcal{I})$ is send-synchronizable. $\hfill\blacktriangleleft$

[bib.bib1] [1] Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91–101, 1996. doi:10.1006/INCO.1996.0053.

[bib.bib2] [2] Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Sadagopan Srinivasan, Krithi Ramamritham, Arun Kumar, M. P. Ravindra, Elisa Bertino, and Ravi Kumar, editors, Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, pages 795–804. ACM, 2011. doi:10.1145/1963405.1963516.

[bib.bib3] [3] Samik Basu and Tevfik Bultan. On deciding synchronizability for asynchronously communicating systems. Theoretical Computer Science, 656:60–75, 2016. doi:10.1016/J.TCS.2016.09.023.

[bib.bib4] [4] Samik Basu, Tevfik Bultan, and Meriem Ouederni. Synchronizability for verification of asynchronously communicating systems. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 56–71. Springer, 2012. doi:10.1007/978-3-642-27940-9_5.

[bib.bib5] [5] Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Étienne Lozes, and Amrita Suresh. A unifying framework for deciding synchronizability. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 14:1–14:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.14.

[bib.bib6] [6] Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 372–391. Springer, 2018. doi:10.1007/978-3-319-96142-2_23.

[bib.bib7] [7] Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323–342, 1983. doi:10.1145/322374.322380.

[bib.bib8] [8] Romain Delpy, Anca Muscholl, and Grégoire Sutre. An automata-based approach for synchronizable mailbox communication. In 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada, volume 311 of LIPIcs, pages 22:1–22:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPICS.CONCUR.2024.22.

[bib.bib9] [9] Cinzia Di Giusto, Laetitia Laversa, and Kirstin Peters. Synchronisability in mailbox communication. In Proceedings Combined 31st International Workshop onTheoretical Computer Science Expressiveness in Concurrencyand 21st Workshop on Structural Operational Semantics, Calgary, Canada, 9th September 2024, volume 412 of Electronic Proceedings in Theoretical Computer Science, pages 19–34. Open Publishing Association, 2024. doi:10.4204/EPTCS.412.3.

[bib.bib10] [10] Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 122:1–122:14. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPICS.ICALP.2017.122.

[bib.bib11] [11] Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. Logical Methods in Computer Science, 19(4), 2023. doi:10.46298/LMCS-19(4:33)2023.

[bib.bib12] [12] Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63–92, 2001. doi:10.1016/S0304-3975(00)00102-X.

[bib.bib13] [13] Xiang Fu, Tevfik Bultan, and Jianwen Su. Synchronizability of conversations among web services. IEEE Transactions on Software Engineering, 31(12):1042–1055, 2005. doi:10.1109/TSE.2005.141.

[bib.bib14] [14] Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147–167, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.

[bib.bib15] [15] Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Étienne Lozes. A partial order view of message-passing communication models. Proceedings of the ACM on Programming Languages, 7(POPL):1601–1627, 2023. doi:10.1145/3571248.

[bib.bib16] [16] Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. On the k-synchronizability of systems. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 157–176. Springer, 2020. doi:10.1007/978-3-030-45231-5_9.

[bib.bib17] [17] Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. International Journal of Foundations of Computer Science, 34(8):1051–1076, 2023. doi:10.1142/S0129054122430018.

[bib.bib18] [18] Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1–38, 2005. doi:10.1016/J.IC.2004.08.004.

[bib.bib19] [19] John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

[bib.bib20] [20] Dietrich Kuske and Anca Muscholl. Communicating automata. In Handbook of Automata Theory, pages 1147–1188. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. doi:10.4171/AUTOMATA-2/9.

[bib.bib21] [21] Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, 1978. doi:10.1145/359545.359563.

[bib.bib22] [22] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 350–373. Springer, 2023. doi:10.1007/978-3-031-37709-9_17.

[bib.bib23] [23] Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 35:1–35:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CONCUR.2021.35.

[bib.bib24] [24] Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 32:1–32:31. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ECOOP.2023.32.

On the Send-Synchronizability Problem for Mailbox Communication

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Definitions and Notations

2.1 Mailbox message-passing systems

▶ Remark 2.1.

Definition 2.2 (Trace).

Definition 2.3 (Viable).

Definition 2.4 (Rendez-vous).

Definition 2.5 (Message Sequence Chart).

▶ Remark 2.6.

Definition 2.7 (Equivalence ≡).

Definition 2.8 (Send-synchronizability).

3 Undecidability of Send-Synchronizability for Mailbox Systems

Lemma 3.1.

Proof sketch..

Corollary 3.2.

Lemma 3.3.

Lemma 3.4.

Proof sketch..

Corollary 3.5.

Theorem 3.6.

4 Send-synchronizability and 𝟏-schedulable Systems

Definition 4.1 (1-scheduling and 1-schedulable).

Definition 4.2 (Commutations).

▶ Remark 4.3.

4.1 From 𝟏-schedulings to arbitrary traces via commutations

Lemma 4.4.

Proof.

Proposition 4.5.

Proof.

Lemma 4.6.

Proof sketch..

Lemma 4.7.

Proof.

▶ Remark 4.8.

4.2 Bad CFMs

Example 4.9.

Proposition 4.10.

Proof.

Proposition 4.11.

Lemma 4.12.

Proof.

Lemma 4.13.

Proof.

Proof of Proposition 4.11.

4.3 Wrap-Up

Proposition 4.14.

Proposition 4.15.

Proof sketch..

Theorem 4.16.

Proof.

5 Conclusion

References

Appendix A 𝟏-schedulability and related notions

Appendix B A necessary and sufficient condition for send-synchronizability

Lemma B.1.

Proof.

Appendix C Proofs of Section 3

Lemma 3.1. [Restated, see original statement.]

Proof.

Corollary 3.2. [Restated, see original statement.]

Proof.

Lemma 3.3. [Restated, see original statement.]

Proof.

Lemma 3.4. [Restated, see original statement.]

Proof.

Corollary 3.5. [Restated, see original statement.]

Proof.

$\blacktriangleright$ Remark 2.1.

$\blacktriangleright$ Remark 2.6.

Definition 2.7 (Equivalence $\mathop{\boldsymbol{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\equiv}}}$ ).

4 Send-synchronizability and $1$ -schedulable Systems

Definition 4.1 ( $1$ -scheduling and $1$ -schedulable).

$\blacktriangleright$ Remark 4.3.

4.1 From $1$ -schedulings to arbitrary traces via commutations

$\blacktriangleright$ Remark 4.8.

Appendix A $1$ -schedulability and related notions