Causal Consistency for Reversible Multiparty Protocols

TL;DR

This paper extends reversible semantics to multiparty communication protocols with asynchronous features, ensuring causal consistency and supporting complex rollback mechanisms in process languages.

Contribution

It introduces a reversible semantics for multiparty protocols with asynchronous communication, expanding prior binary-focused work and proving causal consistency.

Findings

Reversible semantics for multiparty protocols with asynchronous communication.

Causal consistency of the proposed reversible semantics.

Characterization of decoupled rollbacks with atomic semantics.

Abstract

In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with synchronous communication. The applicability and expressiveness of the binary setting, however, is limited. Here we extend our approach, and use it to define reversible semantics for an expressive process model that accounts for multiparty (n-party) protocols, asynchronous communication, decoupled rollbacks, and abstraction passing. As main result, we prove that our reversible semantics for multiparty protocols is causally-consistent. A key technical ingredient in our developments is an alternative reversible semantics with atomic rollbacks, which is conceptually simple and is shown to characterize decoupled rollbacks.

Equations

$$G,G^{\prime }::=$$

$$U,U^{\prime }::=$$

$$T,T^{\prime }::=$$

$$(\mathtt{p}\to \mathtt{q}:⟨U⟩.G){\downarrow }_{\mathtt{r}}$$

$$(\mathtt{p}\to \mathtt{q}:\{l_i:G_i{\}}_{i\in I}){\downarrow }_{\mathtt{r}}$$

$$(\mu X.G){\downarrow }_{\mathtt{r}}$$

$$X{\downarrow }_{\mathtt{r}}$$

$$G=$$

$$\mathtt{B}\to \{\mathtt{A},\mathtt{V}\}:⟨\mathsf{OK}⟩.$$

$$\mathtt{B}\to \mathtt{C}:⟨\mathsf{share}⟩.\mathtt{B}\to \mathtt{C}:⟨\{\{\diamond \}\}⟩.$$

$$\mathtt{B}\to \mathtt{V}:⟨\mathsf{address}⟩.\mathtt{V}\to \mathtt{B}:⟨\mathsf{date}⟩.\mathtt{end}$$

$$G{\downarrow }_{\mathtt{V}}$$

$$G{\downarrow }_{\mathtt{A}}$$

$$G{\downarrow }_{\mathtt{B}}$$

$$G{\downarrow }_{\mathtt{C}}$$

$$\displaystyle\displaystyle{\mathbb{G}[\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}\mathtt{p}\to\mathtt{q}:\langle U\rangle.G]{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\displaystyle\looparrowright$}}}\,}\mathbb{G}[\mathtt{p}\to\mathtt{\!\!\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}q}:\langle U\rangle.G]}$$

$$\mathbb{G}\;\;::=\;\;\bullet\;\mbox{\Large{$\mid$}}\;\mathbb{G}[\mathtt{p}\to\mathtt{q}:\langle U\rangle.\mathbb{G}]\;\mbox{\Large{$\mid$}}\;\mathbb{G}[\mathtt{p}\to\mathtt{q}:\{l_{i}:G_{i}\,;\,l_{j}:\mathbb{G}\}_{i\in I\setminus j}]$$

$$\mathsf{H},{\mathsf{H}}^{\prime }::=$$

$$\mid$$

$$u,w::=$$

$$V,W::=$$

$$P,Q::=$$

$$\displaystyle\;\mbox{\Large{$\mid$}}\;P\;|\;Q\;\mbox{\Large{$\mid$}}\;{X\;\mbox{\Large{$\mid$}}\;\mu X.P}\;\mbox{\Large{$\mid$}}\;{V\,{u}}\;\mbox{\Large{$\mid$}}\;(\nu\,n)P\;\mbox{\Large{$\mid$}}\;\mathbf{0}$$

$$♠::=$$

$$M,N::=$$

$$\mid$$

$$\mathtt{C},{\mathtt{C}}^{\prime }::=$$

$$\alpha ::=$$

$$T,S::=$$

$$H,K::=$$

$$=d!⟨x:G{\downarrow }_{\mathtt{V}}⟩.x?(t).x!⟨price(t)⟩.x!⟨price(t)⟩.x?(ok).x?(a).x!⟨date⟩.0$$

$$=d?(y:G{\downarrow }_{\mathtt{A}}).y!⟨\text{‘Logicomix’}⟩.y?(p).y?(s).y?(ok).0$$

$$\displaystyle=d?(z:G\!\downarrow_{\mathtt{B}}).z?(p).z?(s).z!\langle ok\rangle.z!\langle ok\rangle.z!\langle s\rangle.z!\big{\langle}\{\!\{z!\langle\text{`Urbino, 61029'}\rangle.z?(d).\mathbf{0}\}\!\}\big{\rangle}.\mathbf{0}$$

$$=d?(w:G{\downarrow }_{\mathtt{C}}).w?(s).w?(code).(code\ast )$$

$$M={\ell }_1\left\{\text{Seller}\right\}|{\ell }_2\left\{\text{Alice}\right\}|{\ell }_3\left\{\text{Betty}\right\}|{\ell }_4\left\{\text{Carol}\right\}$$

$$\mathbb{E}\;\;::=\;\;\bullet\;\mbox{\Large{$\mid$}}\;M\;|\;\mathbb{E}\;\mbox{\Large{$\mid$}}\;(\nu\,n)\,\mathbb{E}$$

$$h\circ ({\mathtt{p}}_1,{\mathtt{q}}_1,m_1)\circ ({\mathtt{p}}_2,{\mathtt{q}}_2,m_2)\circ h^{\prime }{\equiv }_{\mathsf{q}}h\circ ({\mathtt{p}}_2,{\mathtt{q}}_2,m_2)\circ ({\mathtt{p}}_1,{\mathtt{q}}_1,m_1)\circ h^{\prime }$$

$$\frac{\text{vbox}M\Re N\text{vbox}}{\text{vbox}\text{vbox}\mathbb{E}[M]\Re \mathbb{E}[N]}$$

$$\begin{array}[]{c}A\;|\;\mathbf{0}\equiv A\quad A\;|\;B\equiv B\;|\;A\quad A\;|\;(B\;|\;C)\equiv(A\;|\;B)\;|\;C\\[2.84526pt] A\;|\;(\nu\,n)B\equiv(\nu\,n)(A\;|\;B)\ (n\notin\mathtt{fn}(A))\quad(\nu\,n)\mathbf{0}\equiv\mathbf{0}\\[2.84526pt] \mu X.P\equiv P\{\raisebox{2.15277pt}{\small$\mu X.P$}\!/\mbox{\small$X$}\}\quad A\equiv B\textrm{ if }A\equiv_{\alpha}B\end{array}$$

$$\sigma [x\mapsto V]$$

$$\sigma \setminus x$$

$$\sigma (V)=\{\begin{array}{ll}W& \text{if V=x and σ=σ′∪{(x,W)}}\\ V& \text{otherwise}\end{array}$$

$$\mathbb{T},\mathbb{S}::=$$

Full text

1. Introduction

This paper is about reversible computation in the context of models of concurrency for communication-centric software systems, i.e., collections of distributed software components in which concurrent interactions are governed by reciprocal dialogues or protocols.

Building upon process calculi techniques, these models provide a rigorous footing for message-passing concurrency; on top of them, many analysis techniques based on behavioral types and contracts have been put forward to enforce key safety and liveness properties (see, e.g., the survey [HLV*+*16]). Reversibility is an appealing notion in concurrency at large [LMT14], but especially so in communication-centric scenarios: it may elegantly abstract fault-tolerant communicating systems that react to unforeseen circumstances (say, local failures) by “undoing” computational steps so as to reach a previous consistent state.

In communication-centric software systems, protocols specify the intended communication structures among interacting components. We focus on process calculi equipped with behavioral types, which use those protocols as types to enforce communication correctness. The interest is in protocol conformance, the property that ensures that each component respects its ascribed protocol. The integration of reversibility in models of communication-centric systems has been addressed from various angles (cf. [TY15, TY16, BDd16, MP16]). Focusing on session types [HVK98, HYC08]—a well established class of behavioral types—, Tiezzi and Yoshida [TY15] were the first to integrate reversibility into a session-typed $\pi$-calculus, following the seminal approach of Danos and Krivine [DK04]; in their approach, however, session types are not used in the definition of reversible communicating systems, nor play a rôle in establishing their properties.

Triggered by this observation, our prior work [MP16, MP17b] develops a monitors-as-memories approach. The idea is to use monitors (i.e., run-time entities that enact protocol actions) as the memories needed to record and eventually undo communication steps. There is a monitor for each protocol participant, which includes a session type that describes the intended protocol. We use a so-called cursor to “mark” the current protocol state in the type; the cursor can move to the future (enacting protocol actions) but also to the past (reversing protocol actions).

The monitors-as-memories approach induces a streamlined process framework in which the key properties of a reversible semantics can be established with simple proofs, because session types narrow down the spectrum of possible process behaviors, allowing only those forward and backward actions that adhere to the declared protocols. The most significant of such properties is causal consistency [DK04], considered as the “right” criterion for reversing concurrent processes in distributed systems [MSG*+*20]. Intuitively, causal consistency ensures that reversible steps lead to system states that could have been reached by performing forward steps only. That is, causally consistent reversibility does not lead to extraneous states, not reachable through ordinary computations.

The reversible framework in [MP16, MP17b], however, accounts only for $\pi$-calculus processes implementing binary sessions, which represent protocols between exactly two partners. Also, it considers synchronous communication instead of the more general asynchronous (queue-based) communication. Hence, our prior work rules out an important class of real-life protocols, namely those that describe interaction scenarios among multiple parties without a single point of control. In multiparty session types [HYC08], these protocols are represented by a global type that can be projected as local types to obtain each participant’s contribution to the entire interaction. Moving from binary to multiparty sessions is a significant jump in expressiveness; global types offer a convenient declarative description of the entire communication scenario. However, the multiparty case also entails added challenges, as two levels of abstraction, global and local, should be considered for (reversible) protocols and their implementations. Hence, it is far from obvious that our monitors-as-memories approach to (causal consistent) reversibility extends to the multiparty case.

Contributions

Given this context, in this paper we make the following contributions:

1. (1)

We introduce a process model for reversible, multiparty sessions with asynchrony (as in [KYHH16]), abstraction passing (i.e., functions from names to processes)  [San92, KPY16, KPY19], and decoupled rollbacks (§ 2). We define forward and backward semantics for multiparty processes by extending the monitors-as-memories approach to both global types and their implementations. 2. (2)

We prove that reversibility in our model is causally consistent (Theorem 11). The proof is challenging as we must appeal to an alternative reversible semantics with atomic rollbacks, which we show to coincide with the semantics with decoupled rollbacks (Theorem 6). 3. (3)

We formally connect reversibility at two distinct levels: the (declarative) level of global types and the (operational) level of processes monitored by local types with cursors (Theorem 13).

We stress that asynchrony, abstraction passing, and decoupled rollbacks are not considered in prior works [TY16, DG16, MP16, MP17b]. Asynchrony and decoupled rollbacks are delicate issues in a reversible multiparty setting—we do not know of other asynchronous calculi with reversible semantics, nor featuring the same combination of constructs. The formal connection between global and local levels of abstraction (Theorem 13) is also unique to our multiparty setting.

Organization

In Section 2, we introduce our process model of reversible multiparty protocols, and illustrate it with examples. In Section 3 we establish causal consistency by relating decoupled and atomic semantics, and connect reversibility at global and local levels. Section 4 discusses an alternative decoupled semantics and related works. Section 5 collects some concluding remarks.

This paper is a revised and extended version of the conference paper [MP17a]. In this presentation we consider a language with labeled choices (not treated in [MP17a]), provide additional examples, streamline the presentation of the decoupled and atomic semantics, extend comparisons with related works, and include technical details (definitions and proofs).

2. Reversible Multiparty Protocols

Fig. 1 depicts the ingredients of our two-level model of protocols and configurations/processes. Multiparty protocols are defined in terms of global types, which declaratively describe a protocol among two or more participants. A global type can be projected onto each participant so as to obtain its corresponding local type, i.e., a session type that abstracts a participant’s contribution to the global protocol.

The semantics of global types is given in terms of forward and backward transition systems (Fig. 3). There is a configuration for each protocol participant: it includes a located process that specifies asynchronous communication behavior, subject to a monitor that enables forward/backward steps at run-time based on the local type. The semantics of configurations is given in terms of forward and backward reduction relations (Figs. 6, 7, 8, 9, and 10). Figure 11 in § 3 summarizes our notations for semantics of global types and configurations.

We illustrate our model of reversible protocols with two examples. As a running example, we develop a reversible variant of the Three-Buyer protocol (see, e.g., [CDCPY15]) with abstraction passing (code mobility), one of the distinctive traits of our framework. This example comes in three parts—cf. § 2.1.2,  § 2.2.2, and § 2.3.3. As second example, in § 2.4 we present a protocol with labeled choices.

Remark \thethm (Colors).

Throughout the paper, we use colors to improve readability. In particular, elements in blue belong to a forward semantics; elements in red belong to a backward semantics. Also, we use orange to highlight the cursor and other syntactic entities.

2.1. Global and Local Types

2.1.1. Syntax

Let us write $\mathtt{p},\mathtt{q},\mathtt{r},\mathtt{A},\mathtt{B}\ldots$ to denote protocol participants. The syntax of global types ($G,G^{\prime},\ldots$) and local types ($T,T^{\prime},\ldots$) is standard [HYC08] and defined as follows:

[TABLE]

The global type $\mathtt{p}\to\mathtt{q}:\langle U\rangle.G$ says that $\mathtt{p}$ may send a value of type $U$ to $\mathtt{q}$, and then continue as $G$. Given a finite index set $I$ and pairwise different labels $l_{i}$, the global type $\mathtt{p}\to\mathtt{q}:\{l_{i}:G_{i}\}_{i\in I}$ specifies a labeled choice: $\mathtt{p}$ may choose label $l_{i}$, communicate this selection to $\mathtt{q}$, and then continue as $G_{i}$. In these two types we assume that $\mathtt{p}\neq\mathtt{q}$. Global recursive and terminated protocols are denoted $\mu X.G$ and $\mathtt{end}$, respectively. We write $\mathtt{\mathtt{pa}}(G)$ to denote the set of participants in $G$.

Value types $U$ include basic first-order values (constants), but also higher-order values: abstractions from names to processes. (We write $\diamond$ to denote the type of processes.) Local types $\mathtt{p}!\langle U\rangle.T$ and $\mathtt{p}?\langle U\rangle.T$ denote, respectively, an output and input of value of type $U$ by $\mathtt{p}$. Type $\mathtt{p}\&\{l_{i}:T_{i}\}_{i\in I}$ says that $\mathtt{p}$ offers different behaviors, available as labeled alternatives; conversely, type $\mathtt{\mathtt{p}}\!\oplus\!\{l_{i}:T_{i}\}_{i\in I}$ says that $\mathtt{p}$ may select one of such alternatives. Terminated and recursive local types are denoted $\mathsf{end}$ and $\mu X.T$, respectively. We use $\alpha$ to denote type prefixes $\mathtt{p}?(U)$, $\mathtt{p}!\langle U\rangle$.

As usual, we consider only recursive types $\mu X.G$ (and $\mu X.T$) in which $X$ occurs guarded in $G$ (and $T$). We shall take an equi-recursive view of (global and local) types, and so we consider two types with the same regular tree as equal.

Global and local types are connected by projection: following [HYC08], the projection of $G$ onto participant $\mathtt{p}$, written $G\!\downarrow_{\mathtt{p}}$, is defined in Fig. 2. Projection for $\mathtt{p}\to\mathtt{q}:\{l_{i}:G_{i}\}_{i\in I}$ is noteworthy: the projections of the participants not involved in the choice (different from $\mathtt{p},\mathtt{q}$) should correspond to the same identical local type.

2.1.2. Example: The Three-Buyer Seller Protocol (I)

The Three-Buyer Seller Protocol involves three buyers—Alice ($\mathtt{A}$), Betty ($\mathtt{B}$), and Carol ($\mathtt{C}$)—who interact with a Seller ($\mathtt{V}$) as follows:

1. (1)

Alice sends a book title to Seller, which replies back to Alice and Betty with a quote. Alice tells Betty how much she can contribute. 2. (2)

Betty notifies Seller and Alice that she agrees with the price, and asks Carol to assist her in completing the protocol. To delegate her remaining interactions with Alice and Seller to Carol, Betty sends her the code she must execute. 3. (3)

Carol continues the rest of the protocol with Seller and Alice as if she were Betty. She sends Betty’s address (contained in the mobile code she received) to Seller. 4. (4)

Seller answers to Alice and Carol (who represents Betty) with the delivery date.

We formalize this protocol as a global type denoted $G$ (see below). We first define some convenient notation.

• •

We write $\mathtt{\mathtt{p}}\to\mathtt{\{\mathtt{q}_{1},\mathtt{q}_{2}\}}:\langle U\rangle.G$ as a shorthand notation for $\mathtt{\mathtt{p}}\to\mathtt{\mathtt{q}_{1}}:\langle U\rangle.\mathtt{\mathtt{p}}\to\mathtt{\mathtt{q}_{2}}:\langle U\rangle.G$ (and similarly for local types).

• •

We write $\{\!\{\diamond\}\!\}$ to denote the type $\mathsf{end}\!\rightarrow\!\diamond$. As we will see, this is the type of a thunk process $\lambda x.\,P$ with $x\not\in\mathtt{fn}(P)$, written $\{\!\{P\}\!\}$. A thunk is an inactive process; it can be activated by applying to it a dummy name of type $\mathsf{end}$ (which we will denote $\ast$).

The global type $G$ between $\mathtt{A}$, $\mathtt{B}$, and $\mathtt{C}$ is as follows:

[TABLE]

where $\mathsf{{price}}$ and $\mathsf{share}$ are base types treated as integers; also, $\mathsf{title}$, $\mathsf{OK}$, $\mathsf{address}$, and $\mathsf{date}$ are base types treated as strings.

Then, following the function defined in Fig. 2, we have the projections of $G$ onto local types:

[TABLE]

2.1.3. Semantics of Protocols

The semantics of global types comprises forward and backward transition relations, denoted {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}, respectively (Fig. 3).

To formalize backward steps, we require some auxiliary notions. We use global contexts, ranged over by $\mathbb{G},\mathbb{G}^{\prime},\ldots$ with holes ‘$\bullet$’, to record previous actions, including the choices discarded and committed:

[TABLE]

We also use global types with history, ranged over by $\mathsf{H},\mathsf{H}^{\prime},\ldots$, to record the current protocol state. This state is denoted by the cursor  ^​​^, which we introduced in [MP16].

{defi}

[Global Types with History]

The syntax of global types with history is defined as follows:

[TABLE]

We write $\mathtt{\mathtt{pa}}(\mathsf{H})$ to denote the set of participants in a global type with history $\mathsf{H}$.

The syntax of global types with history follows some basic intuitions. A directed exchange such as $\mathtt{p}\to\mathtt{q}:\langle U\rangle.G$ has three intermediate states, characterized by the decoupled involvement of $\mathtt{p}$ and $\mathtt{q}$ in the intended asynchronous model:

1. (1)

The first state, denoted \,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}\mathtt{p}\to\mathtt{q}:\langle U\rangle.G, describes the situation prior to the exchange. 2. (2)

The second state represents the point in which $\mathtt{p}$ has sent a value of type $U$ but this message has not yet reached $\mathtt{q}$; this is denoted as \mathtt{p}\to\mathtt{\!\!\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}q}:\langle U\rangle.G. 3. (3)

The third state represents the point in which $\mathtt{q}$ has received the message from $\mathtt{p}$ and the continuation $G$ is ready to execute; this is denoted as \mathtt{p}\to\mathtt{q}:\langle U\rangle.\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}G.

These intuitions extend similarly to $\mathtt{p}\to\mathtt{q}:\{l_{i}:G_{i}\}_{i\in I}$, with the following caveat: the second state should distinguish the choice made by $\mathtt{p}$ from the discarded alternatives; we write \mathtt{p}\to\!\!\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}\mathtt{q}:\{l_{i}:G_{i}\,;\,l_{j}:G_{j}\}_{i\in I\setminus j} to denote that $\mathtt{p}$ has selected $l_{j}$ and that this choice is still to be received by $\mathtt{q}$. Once this occurs, a state \mathtt{p}\to\mathtt{q}:\{l_{i}:G_{i}\,;\,l_{j}:\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}G_{j}\}_{i\in I\setminus j} is reached.

We may now describe the forward and backward transition rules for global types, given in Fig. 3. For a forward directed exchange of a value, Rule (FVal1) formalizes the transition from the first to the second state; Rule (FVal2) denotes the transition from the second to the third state. Rules (FCho1) and (FCho2) are their analogues for the forward directed communication of a label. Rules (BVal1) and (BVal2) undo the step performed by Rules (FVal1) and (FVal2), respectively. Also, Rules (BCho1) and (BCho2) undo the step performed by Rules (FCho1) and (FCho2), respectively.

2.2. Processes and Configurations

2.2.1. Syntax

The syntax of processes and configurations is given in Fig. 4. For processes $P,Q,\ldots$ we follow the syntax of $\mathsf{HO}\pi$, the core higher-order session $\pi$-calculus studied in [KPY16, KPY19]. (Actually, our syntax of processes is related to $\mathsf{HO}$, the sub-language of $\mathsf{HO}\pi$ without name-passing.) The syntax of configurations builds upon that of processes.

Names $a,b,c$ (resp. $s,s^{\prime}$) range over shared (resp. session) names. We use session names indexed by participants, denoted $s_{[\mathtt{p}]},s_{[\mathtt{q}]}$. Names $n,n^{\prime}$ are session or shared names. First-order values $v,v^{\prime}$ include base values and constants. Variables are denoted by $x,y$ and recursion variables are denoted by $X,Y$. We write $\widetilde{x}$ to denote a sequence of variables, sometimes treated as a set. To define configurations, we use fresh name identifiers (keys), denoted $\kappa,\kappa^{\prime},\ldots$, and also identifiers $\ell,\ell^{\prime},\ldots$, which denote a process location or site (as in, e.g., the distributed $\pi$-calculus [Hen07]).

The syntax of values $V$ includes shared names, first-order values, but also abstractions $\lambda x.\,P$, where $P$ is a process. Abstractions are higher-order values, as they denote functions from names to processes. As shown in [KPY16, KPY19], abstraction passing suffices to express name passing (delegation).

Process terms include prefixes for sending and receiving values $V$, written $u!\langle V\rangle.P$ and $u?(x).P$, respectively. Given a finite index set $I$, processes $u\triangleleft\{l_{i}.P_{i}\}_{i\in I}$ and $u\triangleright\{l_{i}:P_{i}\}_{i\in I}$ implement selection and branching (internal and external labeled choices, respectively). The selection $u\triangleleft\{l_{i}.P_{i}\}_{i\in I}$ is actually a non-deterministic choice over $I$. In an improvement with respect to [MP16, MP17b], here we consider parallel composition of processes $P\;|\;Q$ and recursion $\mu X.P$ (which binds $X$ in process $P$). Process $V\,{u}$ is the application which leads to substitute name $u$ on the abstraction $V$. Constructs for restriction $(\nu\,n)P$ and inaction $\mathbf{0}$ are standard.

Session restriction $(\nu\,s)P$ simultaneously binds all the participant endpoints in $P$. We write $\mathtt{fv}(P)$ and $\mathtt{fn}(P)$ to denote the sets of free variables and names in $P$. We assume $V$ in $u!\langle V\rangle.{P}$ does not include free recursion variables $X$. If $\mathtt{fv}(P)=\emptyset$, we call $P$ closed.

The syntax of configurations $M,N,\ldots$, includes inaction $\mathbf{0}$, the parallel composition $M\;|\;N$, and name restriction $(\nu\,n)M$. Also, it includes constructs for session initiation: configuration $\ell\left\{a!\langle x\rangle.{P}\right\}$ denotes the request of a service identified with $a$ implemented in $P$ as $x$; conversely, configuration $\ell\left\{a?(x).{P}\right\}$ denotes service acceptance.

Configurations also include the following run-time elements:

1. (1)

Running processes are of the form \ell:\lbag\mathtt{C}\;{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\textbf{;}}\;P\rbag, where $\ell$ is a location that hosts a process $P$ and a (process) stack $\mathtt{C}$. A stack is simply a list of processes, useful to record/reinstate the discarded alternatives in a labeled choice. 2. (2)

Monitors are of the form {s\mbox{{\Large\lfloor}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}H}\cdot\widetilde{x}\cdot\sigma\mbox{{\Large\rfloor}}^{\spadesuit}}, where $s$ is the session being monitored, $H$ is a local type with history (i.e. in which the cursor  ^​​^ acts as a “memory”), $\widetilde{x}$ is a set of free variables, the store $\sigma$ records the value of such variables (see Def. 5), and $\spadesuit$ is the monitor’s tag (see next).

These five elements allow us to track the current protocol and state of the monitored process. The tag $\spadesuit$ can be either empty (denoted ‘$\lozenge$’) or full (denoted ‘{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}’). When first created, all monitors have an empty tag; a full tag indicates that the running process associated to the monitor is currently involved in a decoupled reversible step. We often omit the empty tag (so we write {s\mbox{{\Large\lfloor}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}H}\cdot\widetilde{x}\cdot\sigma\mbox{{\Large\rfloor}}} instead of {s\mbox{{\Large\lfloor}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}H}\cdot\widetilde{x}\cdot\sigma\mbox{{\Large\rfloor}}^{\lozenge}}) and write {s\mbox{{\Large\lfloor}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}H}\cdot\widetilde{x}\cdot\sigma\mbox{{\Large\rfloor}}^{{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}}}} to emphasize the reversible (red) nature of a monitor with full tag. 3. (3)

Following [KYHH16], we have message queues s:(h\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k), where $s$ is a session, $h$ is the input part of the queue, $k$ is the output part of the queue, and ‘{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}’ acts as a delimiter between the two.

Each queue contains messages of the form $(\mathtt{p}\,,\,\mathtt{q}\,,\,m)$, which is read: “message $m$ is sent from $\mathtt{p}$ to $\mathtt{q}$”. As we will see, an output prefix in a process places the message in its corresponding output queue; conversely, an input prefix retrieves the first message from its input queue. Messages in the queue are never consumed: a process reads a message $(\mathtt{p}\,,\,\mathtt{q}\,,\,m)$ by moving it from the (tail of) queue $k$ to the (top of) queue $h$. This way, the delimiter {\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}} distinguishes the past of the queue from its future. 4. (4)

We use running functions \kappa\mbox{{\Large\lfloor}}(V\,{u})\,,\,\ell\mbox{{\Large\rfloor}} to reverse an application $V\,{u}$. While $\kappa$ is a fresh identifier (key) for this term, $\ell$ is the location of the running process that contains the application.

As customary, we write $\prod_{i\in\{1..n\}}P_{i}$ to stand for the process $P_{1}\;|\;P_{2}\;|\;\cdots\;|\;P_{n}$ (and similarly for configurations). We shall write $\mathcal{P}$ and $\mathcal{M}$ to indicate the set of processes and configurations, respectively. We call agent an element of the set $\mathcal{A}=\mathcal{M}\cup\mathcal{P}$. We let $P,Q$ to range over $\mathcal{P}$; also, we use $L,M,N$ to range over $\mathcal{M}$ and $A,B,C$ to range over $\mathcal{A}$.

2.2.2. Example: The Three-Buyer Seller Protocol (II)

Continuing with the example in §2.1.2, we now give processes for each participant:

[TABLE]

where we assume $\mathit{price}(\cdot)$ returns a value of type $\mathsf{{price}}$ given a $\mathsf{title}$. Observe how Betty’s implementation sends part of its protocol to Carol in the form of a thunk containing her session name $z$ and address. This is how abstraction passing implements session delegation.

The whole system, given by configuration $M$ below, is obtained by placing these process implementations in appropriate locations:

[TABLE]

2.3. A Decoupled Semantics for Configurations

We define a reduction relation on configurations, coupled with a structural congruence on processes and configurations. Our reduction semantics defines a decoupled treatment for reversing communication actions within a protocol. Reduction is thus defined as $\longrightarrow\subset\mathcal{M}\times\mathcal{M}$, whereas structural congruence is defined as $\equiv\,\subset\mathcal{P}^{2}\cup\mathcal{M}^{2}$.

2.3.1. Preliminaries

We require auxiliary definitions for contexts, stores, and type contexts.

Evaluation contexts are configurations with one hole ‘$\bullet$’, as defined by the following grammar:

[TABLE]

General contexts $\mathbb{C}$ are processes or configurations with one hole $\bullet$: they are obtained by replacing one occurrence of $\mathbf{0}$ (either as a process or as a configuration) with $\bullet$. A congruence on processes and configurations is an equivalence relation $\Re$ that is closed under general contexts: $P\,\Re\,Q\Longrightarrow\mathbb{C}[P]\,\Re\,\mathbb{C}[Q]$ and $M\Re N\Longrightarrow\mathbb{C}[M]\,\Re\,\mathbb{C}[N]$.

We define $\equiv$ as the smallest congruence on processes and configurations that satisfies the rules in Fig. 5 and is closed under the equivalence on queues defined below. {defi}[Equivalence on message queues] We define the structural equivalence on queues, denoted $\equiv_{\mathsf{q}}$, as follows:

[TABLE]

whenever $\mathtt{p}_{1}\neq\mathtt{p}_{2}\land\mathtt{q}_{1}\neq\mathtt{q}_{2}$. The equivalence $\equiv_{\mathsf{q}}$ extends to configurations as expected.

A relation $\Re$ on configurations is evaluation-closed if it satisfies the following rules:

[TABLE]

The state of monitored processes is formalized as follows:

{defi}

[Store] The store $\sigma$ is a mapping from variables to values. Given a store $\sigma$, a variable $x$, and a value $V$, the update $\sigma[x\mapsto V]$ and the reverse update $\sigma\setminus x$ are defined as follows:

[TABLE]

The evaluation of value $V$ under store $\sigma$, written $\sigma(V)$, is defined as follows:

[TABLE]

Together with local types with history, the following notion of type context allows us to record the current protocol state: {defi} We define type contexts as (local) types with one hole, denoted ‘$\bullet$’:

[TABLE]

Type contexts $\kappa.\mathbb{T}$ and $(\ell,\ell_{1},\ell_{2}).\mathbb{T}$ will be instrumental in formalizing reversibility of name applications and thread spawning, respectively, which are not described by local types.

As already mentioned, abstraction passing can represent name passing in a fully abstract way (cf. [KPY16, KPY19]). Such a representation suffices to implement a form of session delegation, by including free session names (indexed by participant identities) in the body of an abstraction (cf. Betty’s implementation, discussed above). The following definition identifies those names:

{defi}

Let $h$ and $\mathtt{p}$ be a queue and a participant, respectively. Also, let $\{(\mathtt{q}_{1}\,,\,\mathtt{p}\,,\,\lambda x_{1}.\,P_{1}),$ $\ldots,(\mathtt{q}_{k}\,,\,\mathtt{p}\,,\,\lambda x_{k}.\,P_{k})\}$ denote the (possibly empty) set of messages in $h$ containing abstractions sent to $\mathtt{p}$. We write $\mathtt{\mathsf{roles}}(\mathtt{p},h)$ to denote the set of participant identities occurring in $P_{1},\ldots,P_{k}$.

2.3.2. Reduction

We define $\longrightarrow$ as the union of two relations: the forward and backward reduction relations, denoted {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}, respectively. That is, \longrightarrow={\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}\cup{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}. Relations {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,} are the smallest evaluation-closed relations satisfying the rules in Figs. 6 – 9. We indicate with $\longrightarrow^{*}$, {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}, and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,} the reflexive and transitive closure of $\longrightarrow$, {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}, and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}, respectively.

We now discuss the forward reduction rules (Fig. 6 and Fig. 7), omitting empty tags $\lozenge$:

• •

Rule (Init) initiates a given protocol $G$ with $n$ participants. Given the composition of one service request and $n-1$ service accepts (all along $a$, available in different locations $\ell_{i}$), this rule establishes the session by setting up the run-time elements: running processes and monitors—one for each participant, with empty tag (omitted)—and the empty session queue. A unique session identifier ($s$ in the rule) is also created. The processes are inserted in their respective running structures, and instantiated with an appropriate session name. The local types for each participant are inserted in their respective monitor, with the cursor ‘ ^​​^’ at the beginning.

• •

Rule (Out) starts the output of value $V$ from $\mathtt{p}$ to $\mathtt{q}$. Given an output-prefixed process as running process, and a monitor with a local type supporting an output action, reduction adds the message $(\mathtt{p}\,,\,\mathtt{q}\,,\,\sigma(V))$ to the output part of the session queue (where $\sigma$ is the current store). Also, the cursor within the local type is moved accordingly. In this rule (but also in several other rules), the premise $\mathtt{p}=\mathtt{r}\,\vee\,\mathtt{p}\in\mathtt{\mathsf{roles}}(\mathtt{r},h)$ allows performing actions on names previously received via abstraction passing.

• •

Rule (In) allows a participant $\mathtt{p}$ to receive a value $V$ from $\mathtt{q}$: it takes the first element of the output part of the queue and places it in the input part. The cursor of the local type and the state in the monitor for $\mathtt{p}$ are adjusted accordingly.

• •

Rule (Sel) is the forward rule for labeled selection, which in our case entails a non-deterministic choice between pairwise different labels indexed by $I$. We require that $I$ (the set that indexes the choice in the process) is contained in $J$ (the set that indexes the choice in the protocol). After reduction, the selected label ($l_{w}$ in the rule) is added to the output part of the queue, and the continuation $P_{w}$ is kept in the running process; to support reversibility, alternatives different from $l_{w}$ are stored in the stack $\mathtt{C}$ with their continuations. The cursor is also adjusted in the monitor accordingly.

• •

Rule (Bra) is similar to Rule (Sel): it takes a message containing a label $l_{w}$ as the first element in the output part of the queue, and places it into the input part. This entails a selection between the options indexed by $I$; the continuation $P_{w}$ is kept in the running process, and all those options different from $l_{w}$ are kept in the stack. Also, the local type in the monitor is adjusted accordingly.

• •

Rule (Beta) handles applications, which in our setting are always name applications. Reduction creates a fresh identifier ($\kappa$ in the rule) for the running function, which keeps (i) the structure of the process prior to application, and (ii) the identifier of the running process that “invokes” the application. Notice that $\kappa$ is recorded also in the monitor: this is needed to undo applications in the right order. We use the store $\sigma$ to determine the actual abstraction and the name applied.

• •

Rule (Spawn) handles parallel composition. Location $\ell$ is “split” into running processes with fresh identifiers ($\ell_{1},\ell_{2}$ in the rule). This split is recorded in the monitor.

Now we comment on the backward rules (Fig. 8, Fig. 9, and Fig. 10) which, in most cases, change the monitor tags ($\lozenge$ and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}}):

• •

Rule (RInit) reverses session establishment. It requires that local types for every participant are at the beginning of the protocol, and that session queue and process stacks are empty. Run-time elements are discarded; located service accept/requests are reinstated.

• •

Rule (RollS) starts to reverse an input-output synchronization between $\mathtt{p}$ and $\mathtt{q}$. Enabled when there are complementary session types in the two monitors, this rule changes the monitor tags from $\lozenge$ to {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}}. This way, the undoing of input and output actions occurs in a decoupled way. Rule (RollC) is the analog of (RollS) but for synchronizations originated in labeled choices.

• •

Rule (ROut) reverses an output. This is only possible for a monitor tagged with {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}}, exploiting the first message in the input queue. After reduction, the process prefix is reinstated, the cursor is adjusted, the message is removed from the queue, and the monitor is tagged with $\lozenge$. Rule (RIn) is the analog of Rule (ROut). In this case, we also need to update the state of the store $\sigma$.

• •

Rule (RBra) reverses the input part of a labeled choice: the choice context is reinstated; the cursor is moved; the last message in the input part of the queue is moved to the output part. Rule (RSel) is the analog of (RBra), but for the output part of the labeled choice. The non-deterministic selection is reinstated.

• •

Rule (RBeta) undoes $\beta$-reduction, reinstating the application. The running function disappears, using the information in the monitor ($k$ in the rule). Rule (RSpawn) undoes the spawn of a parallel thread, using the identifiers in the monitor.

2.3.3. Example: The Three-Buyer Seller Protocol (III)

We conclude the example in § 2.1.2 and § 2.2.2 by illustrating the semantics of configurations ({\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}).

Consider configuration $M$ as in (1). The session starts with an application of Rule (Init):

[TABLE]

where $S_{1}$, $A_{1}$, $B_{1}$, and $C_{1}$ stand for the continuation of processes Seller, Alice, Betty, and Carol after the service request/declaration. This way, e.g., $A_{1}=y!\langle\text{`Logicomix'}\rangle.y?(p).y?(s).y?(ok).\mathbf{0}$. We use configuration $M_{1}$ to illustrate some forward and backward reductions.

From $M_{1}$ we could either undo the reduction (using Rule (RInit)) or execute the communication from Alice to Seller (using Rules (Out) and  (In)). This latter option would proceed as follows:

[TABLE]

where $N_{2}$ stands for the running processes and monitors for Seller, Betty, and Carol, not involved in the reduction. We now have:

[TABLE]

where $N_{3}$ stands for the participants not involved in the reduction, $\sigma_{3}$ stands for the resulting store $[x\mapsto d],[t\mapsto\text{`Logicomix'}]$, and $T_{\mathtt{V}}=\mathtt{B}?\langle\mathsf{OK}\rangle.\mathtt{B}?\langle\mathsf{address}\rangle.\mathtt{B}!\langle\mathsf{date}\rangle.\mathsf{end}$. Observe that the cursors in monitors $s_{\mathtt{V}}$ and $s_{\mathtt{A}}$ have evolved, and that the message from $\mathtt{A}$ to $\mathtt{V}$ has now been moved to the input queue.

We illustrate reversibility by showing how to return to $M_{1}$ starting from $M_{3}$. We need to apply three rules: (RollS), (RIn), and (ROut). Reversibility is decoupled in the sense that there is no fixed order in which the latter two rules should be applied; below we just illustrate a possible sequence. First, Rule (RollS) modifies the tags of monitors $s_{\mathtt{V}}$ and $s_{\mathtt{A}}$, leaving the rest unchanged:

[TABLE]

where, as before, $N_{4}$ represents participants not involved in the reduction. $M_{4}$ has several possible forward and backward reductions. One particular reduction uses Rule (RIn) to undo the input at $\mathtt{V}$:

[TABLE]

Just as an application of Rule (RollS) need not be immediately followed by an application of Rule (RIn), an application of Rule (RIn) need not be immediately followed by an application of Rule (ROut). A particular reduction from $M_{5}$ undoes the output at $\mathtt{A}$:

[TABLE]

Clearly, $M_{6}=M_{1}$. Summing up, the synchronization realized by the (forward) reduction sequence M_{1}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{2}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{3} can be reversed by the (backward) reduction sequence M_{3}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}M_{4}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}M_{5}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}M_{1}.

To illustrate abstraction passing, let us assume that $M_{3}$ above follows a sequence of forward reductions until the configuration:

[TABLE]

where $120<\mathit{price}(\text{`Logicomix'})$ is the amount $\mathtt{B}$ may contribute and {\mathbb{T}_{7}\left[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\bullet}\right]}, $\sigma_{7}$, {\mathbb{T}_{8}\left[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\bullet}\right]}, $\sigma_{8}$, and $h_{7}$ capture past interactions as follows:

[TABLE]

If M_{7}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{8} by using Rules (Out) and  (In) then we would have:

[TABLE]

where $\sigma_{9}=\sigma_{8}[code\mapsto\{\!\{s_{[\mathtt{B}]}!\langle\text{`Urbino, 61029'}\rangle.s_{[\mathtt{B}]}?(d).\mathbf{0}\}\!\}]$.

We now may apply Rule (Beta) so as to obtain:

[TABLE]

where $N_{6}$ stands for the rest of the system. Notice that this reduction has added a running function on a fresh $\kappa$, which is also used within the type stored in the monitor $s_{\mathtt{C}}$.

The reduction M_{8}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{9} completes the code mobility from $\mathtt{B}$ to $\mathtt{C}$: the now active thunk will execute $\mathtt{B}$’s implementation from $\mathtt{C}$’s location. This justifies the premise $\mathtt{p}=\mathtt{r}\,\vee\,\mathtt{p}\in\mathtt{\mathsf{roles}}(\mathtt{r},h)$ present in Rules (Out), (In), (Sel), and  (Bra) (and in their backward counterparts): when executing previously received mobile code, the participant mentioned in the location (i.e., $\mathtt{C}$) and that mentioned in the located process (i.e., $\mathtt{B}$) may differ. Further forward reductions from $M_{9}$ will modify the cursor in the type stored in monitor $s_{\mathtt{B}}$ based on the process behavior located at ${\ell_{4}}_{[\mathtt{C}]}$.

2.4. A Protocol with Choices

We close this section by showcasing reversibility of labeled choices. Consider the following global type, specifying a simple binary (two-party) protocol between a Buyer ($\mathtt{B}$) and a Seller ($\mathtt{V}$):

[TABLE]

This way, after receiving a title from Buyer, Seller replies with the price of the requested item; subsequently, a choice indicated by labels $\mathit{ok}$ and $\mathit{quit}$ takes place: Buyer can select whether to continue with the transaction or to conclude it. The projection of $G$ onto local types are:

[TABLE]

Possible implementations for the participants are as follows:

[TABLE]

The whole system, given by configuration $M$ below, is obtained by placing these process implementations in appropriate locations:

[TABLE]

We may then have:

[TABLE]

where $M_{1}$ is the configuration obtained from $M$ once the two participants have initiated the session and exchanged the title and the corresponding price. Above, $x_{1}$ and $x_{2}$ are the free variables of $\mathtt{V}$ and $\mathtt{B}$ after the first three interactions; also, $\sigma_{1}$ and $\sigma_{2}$ represent their respective stores. Queue $h_{1}$ contains the two messages related to $title$ and $\mathit{price}$. The context types are:

[TABLE]

In $M_{1}$, Buyer can decide either (a) to accept the suggested price and continue with the prescribed protocol or (b) to refuse it and exit. The first possibility may proceed using Rule (Sel) as follows:

[TABLE]

where $N_{1}$ contains the rest of the Seller process and monitor of $M_{1}$. As we can see, in $M_{2}$ the cursor  ^​​^ of the Buyer monitor has been moved into the choice. Moreover, the process stack of Buyer is updated in order to register the discarded branch of the choice (i.e., the branch involving label quit). From $M_{2}$, Seller can consume the message on top of the queue (which details the choice by $\mathtt{B}$), or Buyer can revert its choice. In the first case we have the following, using Rule (Bra):

[TABLE]

In the second case, we can revert the labeled choice by using Rule (RollC) from $M_{3}$ first, and then using Rules (RBra) and (RSel) in a decoupled fashion.

Having introduced and illustrated our process model and its reversible semantics, we now move on to establish its key properties.

3. Main Results

We now establish our main result: we prove that reversibility in our model of multiparty asynchronous communication is causally consistent. We proceed in three steps:

1. (1)

First, we introduce an alternative atomic semantics and show that it corresponds, in a tight technical sense, to the decoupled semantics in § 2.3 (Theorems 5 and 6). 2. (2)

Second, in the light of this correspondence, we establish causal consistency for the atomic semantics, following the approach of Danos and Krivine [DK04] (Theorem 11). 3. (3)

Finally, we state a fine-grained, bidirectional connection between the semantics of (high-level) global types with the decoupled semantics of (low-level) configurations (Theorem 13).

These steps allow us to transfer causal consistency to protocols expressed as global types.

3.1. An Atomic Semantics

Our main insight is that causal consistency for asynchronous communication can be established by considering a coarser synchronous reduction relation.

{defi}

[Atomic Reduction] We define atomic versions of the forward and backward reduction relations, relying on the rules in Fig. 12 and 13.

• •

The forward atomic reduction, denoted {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}, is the smallest evaluation-closed relation that satisfies Rules (AC) and (AS) (Fig. 12), together with Rules (Init), (Beta), and (Spawn) (Fig. 6 and 7).

• •

Similarly, the backward atomic reduction, denoted {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}, is the smallest evaluation-closed relation that satisfies Rules (RAC) and (RAS) (Fig. 13), together with Rules (RInit), (RBeta), and (RSpawn) (Fig. 8 and 10).

We then define the atomic reduction relation $\rightarrowtail$ as {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}\cup{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}.

Figure 11 summarizes our notations for reductions. We start by introducing reachable configurations:

{defi}

A configuration $M$ is initial if $M\equiv(\nu\,\tilde{n})\prod_{i\in I}\ell_{i}\left\{P_{i}\right\}$, for some $I$. A configuration is reachable, if it is derived from an initial configuration by using $\longrightarrow$ (cf. § 2.3). A configuration is atomically reachable, if it is derived from an initial configuration by using $\rightarrowtail$.

To relate the decoupled semantics $\longrightarrow$ with the atomic reduction $\rightarrowtail$ (just defined), we introduce the concept of stable configuration. Roughly speaking, in a stable configuration there are no “ongoing” reduction steps. In the forward case, an ongoing step is witnessed by non-empty output queues (which should eventually become empty to complete a synchronization); in the backward case, an ongoing step is witnessed by a marked monitor (which should be eventually unmarked when a synchronization is undone). This way, e.g., in the example of § 2.3.3 configurations $M_{3}$ and $M_{7}$ are stable, whereas $M_{2}$ and $M_{4}$ are not. Reduction $\rightarrowtail$ will move between stable configurations only. We therefore have: {defi} A configuration $M$ is stable, written $\mathtt{sb}(M)$, if

[TABLE]

Reduction $\longrightarrow$ does not preserve stability, but it can be recovered:

Lemma 1**.**

Given a stable configuration $M$ then

• •

if M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N with $\lnot\mathtt{sb}(N)$ then there exists an $N^{\prime}$ such that N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime} and $\mathtt{sb}(N^{\prime})$;

• •

if M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N with $\lnot\mathtt{sb}(N)$ then there exists an $N^{\prime}$ such that N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N^{\prime} and $\mathtt{sb}(N^{\prime})$.

We may then have:

Corollary 2**.**

If $\mathtt{sb}(M)$ and $M\longrightarrow^{*}N$ with $\lnot\mathtt{sb}(N)$, then there exists an $N^{\prime}$ such that $N\longrightarrow^{*}N^{\prime}$ with $\mathtt{sb}(N^{\prime})$.

Proof 3.1**.**

By induction on the reduction sequence $M\longrightarrow^{*}N$.

We now show the Loop lemma [DK04], which offers a local consistency guarantee for the interplay of forward and backward reductions: it ensures that every reduction step can be reverted. This lemma will be crucial both in proving a correspondence between atomic and decoupled semantics, but also in showing causal consistency of the atomic semantics.

Lemma 3** (Loop).**

Let $M,N$ be stable and atomic reachable configurations. Then M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}N if and only if N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}M.

Proof 3.2**.**

By induction on the derivation of M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}N for the if direction, and on the derivation of N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}M for the converse.

The following lemma allow us to “reorder” decoupled reduction steps so to have the generation of a message (e.g., an application of Rules (Out) or (Bra)) followed by its consumption (e.g., an application of Rules (In) or (Sel)). This way, the two consecutive decoupled reductions can be mimicked by one atomic step, which will be in turn instrumental to relate the atomic and decoupled semantics. Below we write {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{i}\,} (and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{i}\,}) to denote a specific step in a reduction sequence.

Lemma 4** (Swap).**

Let $M$ be a reachable configuration.

• •

If M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{1}\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}N_{1} and N_{1}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{2}\,}N_{2}, where {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{1}\,} denotes the use of Rule (Out) or  (Sel) and {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{2}\,} denotes the respective use of Rule (In) or  (Bra), then M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{1}\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright_{2}\,}N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}N_{2}, for some $N$.

• •

If M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{1}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,}N_{1} and N_{1}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{2}\,}N_{2}, where {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{1}\,} denotes the use of Rule (ROut) or (RSel) and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{2}\,} denotes the respective use of Rule (RIn) or (RBra), then M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{1}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}_{2}\,}N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,}N_{2}, for some $N$.

Example 3.3**.**

To better understand Lemma 4, let us consider the following configurations:

[TABLE]

Define the configuration $\mathtt{Sys}$ as:

[TABLE]

From this configuration, by applying Rule (Out) twice, we obtain:

[TABLE]

From $\mathtt{Sys}_{\mathtt{o}}$ we can apply twice Rule {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}(\textsc{In})} and obtain:

[TABLE]

where

[TABLE]

Now, Lemma 4 captures the following observation: starting from $\mathtt{Sys}$, the configuration $\mathtt{Sys}_{\mathtt{end}}$ can also be reached if after the first application of Rule (Out) the produced message is immediately consumed, by applying Rule (In):

[TABLE]

where

[TABLE]

The following theorem provides a first connection between decoupled and atomic reductions; its proof is immediate from their definitions:

Theorem 5** (Relating $\longrightarrow$ and $\rightarrowtail$).**

Let $M$ and $N$ be stable configurations. We have:

• •

M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}N if and only if either M{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}}N or M{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}}N;

• •

M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}N if and only if either M{{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}}N or M{{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}}N.

We now embark ourselves in providing a tighter formal connection between $\longrightarrow$ and $\rightarrowtail$, using back-and-forth bisimulations [LMS16]. We shall work with binary relations on configurations, written $\Re\subseteq\mathcal{M}\times\mathcal{M}$. We now adapt the usual notion of barbs [SW01] to our setting: rather than communication subjects (which are hidden/unobservable names in intra-session communications), it suffices to use participant identities as observables: {defi}[Barbs] A reachable configuration $M$ has a barb $\mathtt{p}$, written $M\downharpoonright_{\mathtt{p}}$, if

• •

M\equiv(\nu\,\tilde{n})(N\;|\;{\ell}_{[\mathtt{r}]}:\lbag\mathtt{C}\;{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\textbf{;}}\;P\rbag\;|\;{s_{\mathtt{p}}\mbox{{\Large\lfloor}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathbb{S}[\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}T]}\cdot\widetilde{x}\cdot\sigma\mbox{{\Large\rfloor}}^{\lozenge}}) where either:

(i) $P\equiv s_{[\mathtt{p}]}!\langle V\rangle.{Q}\;|\;R$ and $T=\mathtt{\mathtt{q}}!\langle U\rangle.T_{1}$ or

(ii) $P\equiv s_{[\mathtt{p}]}\triangleleft\{l_{i}.P_{i}\}_{i\in I}\;|\;R$ and $T=\mathtt{\mathtt{q}}\!\oplus\!\{l_{j}:T_{j}\}_{j\in J}$.

Notice that our definition of barbs is connected to the notion of stability: since in $M\downharpoonright_{\mathtt{p}}$ we require a monitor with empty tag, this ensures that $\mathtt{p}$ is not involved in an ongoing backward step. In a way, this allows us to consider just forward barbs (as in [AC17]).

We now adapt the definition of weak barbed back-and-forth (bf) bisimulation and congruence [LMS16] in order to work with decoupled and atomic reduction semantics: {defi} A relation $\Re$ is a (weak) barbed bf simulation if whenever $M\Re N$

• •

$M\downharpoonright_{\mathtt{p}}$ implies $N\longrightarrow^{*}\downharpoonright_{\mathtt{p}}$;

• •

M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}M_{1} implies N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}N_{1}, with $M_{1}\Re N_{1}$;

• •

M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}M_{1} implies N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{*}\,}N_{1}, with $M_{1}\Re N_{1}$.

A relation $\Re$ is a (weak) barbed bisimulation if $\Re$ and $\Re^{-1}$ are weak bf barbed simulations. The largest weak barbed bisimulation is (weak) barbed bisimilarity, noted $\approx$. We say that $M$ and $N$ are (weakly) barbed congruent, written $\stackrel{{\scriptstyle\cdot}}{{\approx}}$, if for each context $\mathbb{C}$ such that $\mathbb{C}[M]$ and $\mathbb{C}[N]$ are atomic reachable configurations, then $\mathbb{C}[M]\approx\mathbb{C}[N]$.

This way, in establishing $M\stackrel{{\scriptstyle\cdot}}{{\approx}}N$ we should consider that atomic reduction steps from $M$ are matched by $N$ with decoupled reduction steps. This is how $\stackrel{{\scriptstyle\cdot}}{{\approx}}$ enables us to state our second connection between decoupled and atomic reductions. To prove the correspondence between the two semantics, we shall relate the same configuration $M$ under the two different semantics. Hence:

Theorem 6**.**

For any atomic reachable configuration $M$, we have that $M\stackrel{{\scriptstyle\cdot}}{{\approx}}M$.

Proof 3.4**.**

First, notice that showing $\mathbb{C}[M]\approx\mathbb{C}[M]$ is similar to show $M_{1}\approx M_{1}$ with $M_{1}=\mathbb{C}[M]$. This allows us to just focus on the “hole” of the context. It is then sufficient to show that the following relation is a bf weak bisimulation.

[TABLE]

Clearly, $(M,M)\in\Re$. We consider the requirements in Def. 3.1. Let us first consider barbs.

• •

Suppose that $M$ challenges $N$ with a barb. We distinguish two cases: $N$ is stable or not. If $\mathtt{sb}(N)$ then $N$ has the same barb. Otherwise, if $\lnot\mathtt{sb}(N)$, by Corollary 2 there exists an $N_{1}$ such that $N\longrightarrow^{*}N_{1}$ and $\mathtt{sb}(N_{1})$. Since $M\longrightarrow^{*}N$ we may derive $M\longrightarrow^{*}N_{1}$ with both stable configurations. By applying Theorem 5 on $M\longrightarrow^{*}N_{1}$ we infer $M\rightarrowtail^{*}N_{1}$; then, by applying the Loop Lemma (Lemma 3) we further infer $N_{1}\rightarrowtail^{*}M$. Using again Theorem 5 we infer that $N_{1}\longrightarrow^{*}M$; since we have deduced that $N\longrightarrow^{*}N^{\prime}\longrightarrow^{*}M$, we know that $N$ weakly matches all the barbs of $M$, as desired.

• •

Suppose now that $N$ challenges $M$ with a barb. We proceed similarly as above: if $\mathtt{sb}(M)$ then $M$ has the same barb; otherwise, if $\lnot\mathtt{sb}(M)$, since $M\longrightarrow^{*}N$, by Corollary 2 we have that $M\longrightarrow^{*}N\longrightarrow^{*}N_{1}$, with $\mathtt{sb}(N_{1})$. Let us note that the reductions in $N\longrightarrow^{*}N_{1}$ do not add barbs to $N_{1}$: they only finalize ongoing synchronizations; by definition of barbs (Def. 5) parties involved in ongoing rollbacks do not contribute to barbs. We can conclude by applying Theorem 5 and deriving $M\rightarrowtail^{*}N_{1}$, which has the same barbs of $N$, as desired.

Let us now consider reductions. We will just focus on synchronizations due to input/output and branching/selection reduction steps, since these are the cases in which $\longrightarrow$ and $\rightarrowtail$ differ; indeed, reductions due to Rules Spawn and Beta can be trivially matched.

Let us consider challenges from $M$. There are two cases: M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}M_{1} and M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}M_{1}. In the first case, as we distinguish two sub-cases: either $N$ has already started the synchronization or not. In the first sub-case, $N$ can conclude the step: N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime}. Now we have that M{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}}N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime}. Thanks to Lemma 4 we can rearrange such a reduction sequence as follows: M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{1}{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}}N^{\prime}. We then have that the pair $(M_{1},N^{\prime})\in\Re$, as desired. In the second sub-case, $N$ can match the step with 2 reductions: N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime}. Also in this case we can rearrange the reduction sequence so as to obtain M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M_{1}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}N^{\prime}, with $(M_{1},N^{\prime})\in\Re$, as desired. The case M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}M_{1} (i.e., the challenge is a backward move) is handled similarly.

We now consider challenges from $N$, focusing only on synchronizations, just as before. If N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime}, we distinguish two cases: whether the reduction ends an ongoing input/output and branching/selection, or it opens a new one. In the second case $M$ matches the move with an idle move, i.e., $(M,N^{\prime})\in\Re$. In the other case we can rearrange the reduction M{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}}N{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N^{\prime} into a similar reduction sequence M\longrightarrow^{*}N_{1}{{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}}N^{\prime} with $\mathtt{sb}(N_{1})$, and all reductions in N_{1}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}N^{\prime} just start new synchronizations. Thanks to Theorem 5, $M$ can mimick the same reduction to $N_{1}$, i.e., M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow^{*}}N_{1}, and we have that $(N_{1},N^{\prime})\in\Re$, as desired. The case in which N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N^{\prime} (i.e., the challenge is a backward move) is similar. This concludes the proof.

By observing that the set of atomic configurations is a subset of reachable configurations, this result can also be formulated as full abstraction. Let $f$ be the (injective, identity) mapping from atomic reachable configurations to reachable configurations. We then have:

Corollary 7** (Full Abstraction).**

Let $f$ be the injection from atomic reachable configurations to reachable configurations, and let $M,N$ be two atomic reachable configurations. Then we have $f(M)\stackrel{{\scriptstyle\cdot}}{{\approx}}f(N)$ if and only if $M\stackrel{{\scriptstyle\cdot}}{{\approx}}N$.

Proof 3.5**.**

From Theorem 6 we have $M\stackrel{{\scriptstyle\cdot}}{{\approx}}f(M)$ and $N\stackrel{{\scriptstyle\cdot}}{{\approx}}f(N)$. The thesis follows then by transitivity of $\stackrel{{\scriptstyle\cdot}}{{\approx}}$.

The results above ensure that the loss of atomicity preserves the reachability of configurations yet does not make undesired configurations reachable.

3.2. Causal Consistency

Theorems 5 and 6 allow us to focus on the atomic reduction $\rightarrowtail$ for the purposes of establishing causal consistency. We follow the approach we developed in our prior work [MP16, MP17b], here considering the more general multiparty setting with asynchronous, higher-order communication; in turn, our prior approach adapts to the proof technique by Danos and Krivine [DK05] (developed for a reversible CCS).

In a nutshell, causal consistency concerns traces of transitions, each one endowed with an appropriate stamp. The proof of causal consistency relies on square, rearranging, and shortening lemmas, which together express properties of traces and transitions that characterize flexible and consistent reversible steps. We start by defining transitions:

{defi}

[Transitions and Stamps]

A transition $t$ is a triplet of the form $t:M\xRightarrow{\eta}N$ where $M\rightarrowtail N$ (cf. Def. 3.1) and the transition stamp $\eta$ is defined as follows:

• •

$\eta=\{\ell_{1},\mathtt{p}_{1},\cdots,\ell_{n},\mathtt{p}_{n}\}$, if Rule (Init) or (RInit) is used;

• •

$\eta=\{\mathtt{p},\mathtt{q}\}$, if one of Rules (AC), (AS), (RAC) and (RAS) is used;

• •

$\eta=\{\ell,\mathtt{p}\}$, if one of Rules (Beta), (Spawn), (RBeta) or (RSpawn) is used.

Some terminology on transitions, taken from [MP16, MP17b], is in order.

{defi}

[Terminology for Transitions] Suppose a transition $t:M\xRightarrow{\eta}N$.

• •

We say $M$ and $N$ are the source and target of $t$ (written $\mathtt{src}(t)$ and $\mathtt{trg}(t)$, respectively).

• •

Transition $t:M\xRightarrow{\eta}N$ is forward if M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\hookrightarrow}N and backward if M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\hookrightarrow}}}}N.

• •

The inverse of $t$, denoted $\overline{t}$, is the transition $\overline{t}:N\xRightarrow{\eta}M$.

• •

Two transitions are coinitial if they have the same source; cofinal if they have the same target; composable if the target of the first one is the source of the other.

• •

Given coinitial transitions $t_{1}:M\xRightarrow{\eta_{1}}N_{1}$ and $t_{2}:M\xRightarrow{\eta_{2}}N_{2}$, we define $t_{2}/t_{1}$ (read “$t_{2}$ after $t_{1}$”) as $N_{1}\xRightarrow{\eta_{2}}N_{2}$, i.e., the transition with stamp $\eta_{2}$ that starts from the target of $t_{1}$ and ends in the target of $t_{2}$.

Two important classes of transitions are conflicting and concurrent ones:

{defi}

Two coinitial transitions $t_{1}:M\xRightarrow{\eta_{1}}M_{1}$ and $t_{2}:M\xRightarrow{\eta_{2}}M_{2}$ are said to be in conflict if $\eta_{1}\cap\eta_{2}\neq\emptyset$. Two transitions are concurrent if they are not in conflict.

We now consider the so-called Square Lemma [DK04], which may be informally described as follows. Assume a configuration from which two transitions are possible: if these transitions are concurrent then the order in which they are executed does not matter, and the same configuration is reached.

Lemma 8** (Square).**

If $t_{1}:M\xRightarrow{\eta_{1}}M_{1}$ and $t_{2}:M\xRightarrow{\eta_{2}}M_{2}$ are coinitial and concurrent transitions, then there exist cofinal transitions $t_{2}/t_{1}=M_{1}\xRightarrow{\eta_{2}}N$ and $t_{1}/t_{2}=M_{2}\xRightarrow{\eta_{1}}N$.

Proof 3.6**.**

By case analysis on the possible rules used to derive $M\xRightarrow{\eta_{1}}M_{1}$ and $M\xRightarrow{\eta_{2}}M_{2}$. To define the valid combinations of rules, we define sets

[TABLE]

The licit combinations are given by pairs of rules in the set $\{(r_{i},r_{j})\,|\,\{r_{i},r_{j}\}\subset\textsc{Rule}\cup\overline{\textsc{Rule}}\}$. Let us note that the definition of concurrent transitions (Definition 3.2) ensures that the pairs $(r_{i},r_{j})$ concern rule applications that involve different participants.

All valid cases are treated similarly; we content ourselves by considering only the case (RAS, AC), in which queue equivalence (Definition 2.3.1) plays an important role. We have that:

[TABLE]

From $M$ we have two possible reductions: either $\mathtt{p}_{1},\mathtt{q}_{1}$ communicate or $\mathtt{p}_{2},\mathtt{q}_{2}$ undo the selection. By Definition 3.2, $\eta_{1}=\{\mathtt{p}_{1},\mathtt{q}_{1}\}$ and $\eta_{2}=\{\mathtt{p}_{2},\mathtt{q}_{2}\}$. By Rule AC we have:

[TABLE]

and by Rule RAS we have:

[TABLE]

Now it is easy to see that there is an $N$ such that $M_{1}\xRightarrow{\eta_{2}}N$ and $M_{2}\xRightarrow{\eta_{1}}N$:

[TABLE]

[TABLE]

Let us note that in $M_{1}$ the equivalence on queues (cf. Definition 2.3.1) allows the swapping of the two messages $(\mathtt{p}_{2}\,,\,\mathtt{q}_{2}\,,\,l_{w})\circ(\mathtt{p}_{1}\,,\,\mathtt{q}_{1}\,,\,V)$ so to enact the Rule RAS.

We now turn our attention to traces, sequences of pairwise composable transitions. We let $\rho$ range over traces. Notions of target, source, composability and inverse extend naturally from transitions to traces. We write $\varepsilon_{M}$ to denote the empty trace with source $M$, and $\rho_{1};\rho_{2}$ to denote the composition of two composable traces $\rho_{1}$ and $\rho_{2}$.

{defi}

We define $\asymp$ as the least equivalence between traces that is closed under composition and that obeys: i) $t_{1};t_{2}/t_{1}\asymp t_{2};t_{1}/t_{2}$; ii)  $t;\overline{t}\asymp\varepsilon_{\mathtt{src}(t)}$; iii) $\overline{t};t\asymp\varepsilon_{\mathtt{trg}(t)}$.

Intuitively, $\asymp$ says that: (a) given two concurrent transitions, the traces obtained by swapping their execution order are equivalent; (b) a trace consisting of opposing transitions is equivalent to the empty trace.

The proof of causal consistency follows that in [DK04], but with simpler arguments (because of our simpler transition stamps), which mirror those in [MP16, MP17b].

The following lemma says that, up to causal equivalence, traces can be rearranged so as to reach the maximum freedom of choice, first going only backwards, and then going only forward.

Lemma 9** (Rearranging).**

Let $\rho$ be a trace. There are forward traces $\rho^{\prime},\rho^{\prime\prime}$ such that $\rho\asymp\overline{\rho^{\prime}};\rho^{\prime\prime}$.

Proof 3.7**.**

By lexicographic induction on the length of $\rho$ and on the distance between the beginning of $\rho$ and the earliest pair of opposing transitions in $\rho$. The analysis uses both the Loop Lemma (Lemma 3) and the Square Lemma (Lemma 8).

If trace $\rho_{1}$ and forward trace $\rho_{2}$ start from the same configuration and end up in the same configuration, then $\rho_{1}$ may contain some “local steps”, not present in $\rho_{2}$, which must be eventually reversed—otherwise there would be a difference with respect to $\rho_{2}$. Hence, $\rho_{1}$ could be shortened by removing such local steps and their corresponding reverse steps.

Lemma 10** (Shortening).**

Let $\rho_{1},\rho_{2}$ be coinitial and cofinal traces, with $\rho_{2}$ forward. Then, there exists a forward trace $\rho^{\prime}_{1}$ of length at most that of $\rho_{1}$ such that $\rho^{\prime}_{1}\asymp\rho_{1}$.

Proof 3.8**.**

By induction on the length of $\rho_{1}$, using Square and Rearranging Lemmas (Lemmas 8 and 9). The proof uses the forward trace $\rho_{2}$ as guideline for shortening $\rho_{1}$ into a forward trace, relying on the fact that $\rho_{1}$ and $\rho_{2}$ share the same source and target.

We may now state our main result:

Theorem 11** (Causal consistency).**

Let $\rho_{1}$ and $\rho_{2}$ be coinitial traces, then $\rho_{1}\asymp\rho_{2}$ if and only if $\rho_{1}$ and $\rho_{2}$ are cofinal.

Proof 3.9**.**

The ‘if’ direction follows by definition of $\asymp$ and trace composition. The ‘only if’ direction uses Square, Rearranging, and Shortening Lemmas (Lemmas 8, 9, and 10).

At this point one may object that causal-consistency has been proved on the atomic semantics and not on the decoupled semantics, and wonder whether the chosen behavioural equivalence (cf. Definition 3.1) is causal-preserving. First, we observe that our notion of equivalence is a congruence, and that the only visible event in a message-passing system is the receipt of a message itself. Then it is easy to see that our equivalence preserves the order of messages sent, and hence that the decoupled semantics respects the same notion of causality of the atomic semantics.

3.3. Connecting (Reversible) Protocols and (Reversible) Configurations

We now connect the two levels of abstraction in our reversible model by relating protocols and configurations. This is the content of Theorem 13, which relies on a few auxiliary definitions.

We introduce a notion of well-formed processes and configurations that implement a given local type. Figure 14 reports a set of rules for decreeing well-formed processes: it is inspired by the type system for higher-order session processes defined in [KPY16].

Our system for well-formedness is simple, and relies on two contexts: $\Gamma$ (for recursion variables) and $\Delta$ (for assignments of variables to local types). We omit these contexts when empty and/or unimportant. Well-formedness uses the following judgments:

• •

$\vdash u::T$ says that $u$ is a name of local type $T$

• •

$\Gamma;\Delta\vdash V::U$ says that $V$ is a well-formed value of type $U$

• •

$\Gamma;\Delta\vdash P$ says that $P$ is a well-formed process

The first three rules in Figure 14 are for values: booleans and abstractions (rules for other base values are similar). Then we have a rule enforcing a weakening principle, and rules for inaction and application, which are as expected. The rule for output enables us to account for processes in which a communicated abstraction specifies a protocol which is continued outside the output action; this is case for process Betty in § 2.2.2, in which part of the protocol on $z$ is sent around as a thunk. The remaining rules, for input, selection, branching, and recursive processes, are self-explanatory. Notice that for the sake of simplicity, we consider restriction-free, single-threaded processes (i.e., no processes of the form $(\nu\,n)P$ and $P_{1}\;|\;P_{2}$).

We are interested in well-formed processes that implement a single session with local type $T$ along $u$ (a session name or a variable): {defi}[Well-Formed Processes] We say process $P$ is well-formed if $\emptyset;\{u:T\}\vdash P$ in the system of Figure 14, for some $u$ and $T$. This is denoted $P\stackrel{{\scriptstyle u}}{{\ltimes}}T$.

We may then define the configurations that implement a global type with history (cf. Def. 3). First, an auxiliary definition:

{defi}

[Reachable Global Types]

We say the global type with history $\mathsf{H}$ is reachable if it can be obtained from a global type $G$ via a sequence of {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,} transitions (cf. Fig. 3).

{defi}

[Configurations Implementing Global Types]

Let ${G}$ be a global type, with $\mathtt{\mathtt{pa}}(G)=\{\mathtt{p}_{1},\cdots,\mathtt{p}_{n}\}$.

• •

We say that configuration $M$ initially implements $G$, written $M\stackrel{{\scriptstyle\mathsf{o}}}{{\bowtie}}G$, if we have

[TABLE]

with $P_{i}\stackrel{{\scriptstyle x_{i}}}{{\ltimes}}G\!\downarrow_{\mathtt{p}_{i}}$, for all $i\in\{1,\!\cdots\!,n\}$, for some stores $\sigma_{1},\ldots,\sigma_{n}$.

• •

A configuration $N$ implements the global type with history $\mathsf{H}$, written $N\bowtie\mathsf{H}$, if there exist $M,G$ such that (i) $\mathsf{H}$ is reachable from $G$, (ii) $M\stackrel{{\scriptstyle\mathsf{o}}}{{\bowtie}}G$, and (iii) $N$ is reachable from $M$.

Observe how $M\stackrel{{\scriptstyle\mathsf{o}}}{{\bowtie}}G$ formalizes $M$ as the result of initializing the configuration, following Rule (Init) (cf. Fig. 6). This way, $N\bowtie\mathsf{H}$ reflects the evolution from an initial implementation, with $\mathsf{H}$ being reachable from $G$ and $N$ being reachable from $M$ following forward and backward rules. The following proposition details the shape of a configuration that is reachable from $M\stackrel{{\scriptstyle\mathsf{o}}}{{\bowtie}}G$:

Proposition 12**.**

Let $N\bowtie\mathsf{H}$ with $\mathtt{\mathtt{pa}}(\mathsf{H})=\{\mathtt{p}_{1},\cdots,\mathtt{p}_{n}\}$. Then we have

[TABLE]

where, for all $i\in\{1,\!\cdots\!,n\}$, {\lbag\mathtt{C}_{i}\;{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\textbf{;}}\;Q_{i}\rbag}\stackrel{{\scriptstyle{s}_{[\mathtt{p}_{i}]}}}{{\ltimes}}{\mathbb{T}_{i}\left[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}S_{i}}\right]} holds as in Figure 15.

Proof 3.10**.**

Immediate from Definition 3.1 (reachable configuration), Definition 14 (“initially implements”), and the reduction semantics $\longrightarrow$.

Recall that $\spadesuit$ can be either full {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}} or empty $\lozenge$; thus, if $M\bowtie\mathsf{H}$ then $M$ may not be stable.

The last ingredient required is a swapping relation over global types, denoted $\approx_{\mathtt{sw}}$, which enables behavior-preserving transformations among causally independent communications.

{defi}

[Swapping] We define $\approx_{\mathtt{sw}}$ as the smallest congruence on $G$ that satisfies the rules in Fig. 16 (where we omit the symmetric versions of (Sw1), (Sw2), and (Sw3)). We extend $\approx_{\mathtt{sw}}$ to global types with history $\mathsf{H}$ as follows: \mathbb{G}[\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}G_{1}]\approx_{\mathtt{sw}}\mathbb{G^{\prime}}[\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\text{{\textasciicircum\!\!\textasciicircum}}}G_{2}] if $\mathbb{G}[\mathtt{end}]\approx_{\mathtt{sw}}\mathbb{G^{\prime}}[\mathtt{end}]$ and $G_{1}\approx_{\mathtt{sw}}G_{2}$.

Notice that Definition 2.3.1 and swapping play similar rôles but at different levels: queues/configurations and global types, respectively.

We comment on the statement of Theorem 13, given next, which relates (i) transitions in the semantics of (high-level) global types (with history) with (ii) reductions in the semantics of their (low-level) process implementations. It is in two parts, which capture an asymmetry between a global type $\mathsf{H}$ and a configuration $M$, with $M\bowtie\mathsf{H}$: while Part (a) shows that the behavior of $\mathsf{H}$ can be closely mimicked by $M$, Part (b) shows that $M$ may have more immediate behaviors than $\mathsf{H}$: this is because $M$ may include several independent (and immediate) reductions (written M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N_{i} and M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N_{i} below), which are matched by $\mathsf{H}$ up to swapping. The asymmetry can then be interpreted as configurations being more concurrent (less sequential) than a global type.

Below, M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{\,j}\,}M^{\prime} denotes a sequence of $j\geq 0$ reduction steps (if $j=0$ then $M=M^{\prime}$). Also, we write \mathsf{H}^{\approx_{\mathtt{sw}}}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime\prime} to mean that \mathsf{H}\approx_{\mathtt{sw}}\mathsf{H}^{\prime}\land\mathsf{H}^{\prime}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime\prime}, for some $\mathsf{H}^{\prime}$ (and similarly for {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}).

Theorem 13**.**

Let $\mathsf{H}$ be a reachable global type with history (cf. Def. 14). Suppose $M\bowtie\mathsf{H}$.

1. (1)

If \mathsf{H}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime} then M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M^{\prime} and $M^{\prime}\bowtie\mathsf{H^{\prime}}$, for some $M^{\prime}$.

Also, if \mathsf{H}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}\mathsf{H}^{\prime} then M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}^{\,j}\,}M^{\prime} (with $j=1$ or $j=2$) and $M^{\prime}\bowtie\mathsf{H^{\prime}}$, for some $M^{\prime}$. 2. (2)

For all $N_{i}$ such that M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N_{i}, there exist $\mathsf{H}_{i},\mathsf{H}^{\prime}$, and $M^{\prime}$, such that \mathsf{H}^{\approx_{\mathtt{sw}}}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}_{i}, $N_{i}\bowtie\mathsf{H}_{i}$, N_{i}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright^{*}\,}M^{\prime}, \mathsf{H}_{i}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}^{*}\,}\mathsf{H}^{\prime}, and $M^{\prime}\bowtie\mathsf{H}^{\prime}$ (and similarly for {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}, {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}).

Proof 3.11**.**

We consider both parts separately:

**Part (a): **

By induction on the transitions \mathsf{H}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime} and \mathsf{H}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}\mathsf{H}^{\prime}, with a case analysis on the last applied rule (Fig. 3).

For \mathsf{H}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime} there are four possible transitions, we have a one-to-one correspondence:

• **•: **

a transition derived using Rule (FVal1) is matched by $M$ using Rule (Out);

• **•: **

a transition derived using Rule (FVal2) is matched by $M$ using Rule (In);

• **•: **

a transition derived using Rule (FCho1) is matched by $M$ using Rule (Sel);

• **•: **

a transition derived using Rule (FCho2) is matched by $M$ using Rule (Bra).

The analysis for \mathsf{H}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}\mathsf{H}^{\prime} is similar, but we may require an additional reduction step from $M$, depending on the tag of the corresponding monitor (cf. Prop. 12). If the tag of $M$ is {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge} then the transition can be immediately matched as follows ($j=1$):

• **•: **

a transition derived using Rule (BVal1) is matched by $M$ using Rule (ROut);

• **•: **

a transition derived using Rule (BVal2) is matched by $M$ using Rule (RIn);

• **•: **

a transition derived using Rule (BCho1) is matched by $M$ using Rule (RSel);

• **•: **

a transition derived using Rule (BCho2) is matched by $M$ using Rule (RBra).

Otherwise, if the tag of $M$ is $\lozenge$, then $j=2$ because an additional reduction (using Rule (RollS) or (RollC)) is required in order to reach a configuration with tag {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}.

**Part (b): **

By induction on transitions M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N and M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N, with a case analysis on the last applied rule, following similar lines. There are two main cases:

1. **(1): **

There is exactly one reduction M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N (and M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N), which involves participants that appear at the top-level in $\mathsf{H}$. 2. **(2): **

There are one or more reductions M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N_{i} (and M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N_{i}) whose involved participants cannot be found at the top-level in $\mathsf{H}$.

We discuss case (i) first. Suppose M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N: then the reduction was obtained using one of the following Rules (Out), (In), (Sel), (Bra), and  (Beta). Notice that a reduction with Rule (Spawn) is not possible under our definition of well-formed processes (and configurations). For the first four cases, a corresponding transition \mathsf{H}{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\looparrowright}}}\,}\mathsf{H}^{\prime} can be easily obtained, as in the analysis for Part (a); a reduction obtained with Rule (Beta) does not involve the global type, and so $\mathsf{H}^{\prime}=\mathsf{H}$. In either case, $N\bowtie\mathsf{H}^{\prime}$ holds easily. Now suppose M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N. Here the analysis depends on the tag in $M$: if it is {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge} then the reduction was derived using Rules (ROut), (RIn), (RSel), (RBra), or (RBeta). Here again a reduction via Rule (RSpawn) is not possible. As before, in the first four cases the reduction can be mimicked directly by one transition \mathsf{H}{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\looparrowright\,}\mathsf{H}^{\prime}; in the last one, there is no global type transition ($\mathsf{H}^{\prime}=\mathsf{H}$). If the tag is $\lozenge$ then the reduction is derived using Rules (RollS) or (RollC). This reduction is not mimicked by $\mathsf{H}$ but enables a reduction N{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}M^{\prime}, using one of the Rules (Out), (In), (Sel), (Bra), and  (Beta), which can be mimicked as discussed for the case {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}, ensuring $M^{\prime}\bowtie\mathsf{H}^{\prime}$.

In case (ii) we use $\approx_{\mathtt{sw}}$ to obtain behavior-preserving transformations $\mathsf{H}^{*}_{i}$ of $\mathsf{H}$ in which the participants involved in the reductions (M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}N_{i} or M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}N_{i}) appear at the top-level. Such transformations exist, because of assumption $M\bowtie\mathsf{H}$. This way, the reductions from $M$ can be matched by $\mathsf{H}^{*}_{i}$, following the analysis described in case (i); after all the independent communication actions have been performed and matched (there are finitely many of them), it is easy to obtain $M^{\prime}$ and $\mathsf{H}^{\prime}$ such that $M^{\prime}\bowtie\mathsf{H}^{\prime}$.

Summing up, we have that Theorem 11 ensures that reversibility in the atomic semantics is causally consistent. Theorem 6 transfers this result to decoupled semantics; since by Theorem 13 decoupled semantics defines a sound local implementation, we conclude that reversibility for global types is also causally consistent.

4. Discussion and Related Work

4.1. An Alternative Semantics

Our decoupled semantics for asynchronous communication, given by {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}\cup{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}, relies on a single (global) queue for all the participants in the session. This is different from the semantics in works such as [HYC08, KY13, KY14], where there is a queue per channel/participant. Here we discuss an alternative decoupled semantics with a dedicated (local) queue per participant, and argue that our main results hold also in such an alternative semantics.

The syntax of processes and configurations, given in Fig. 4, is kept largely unchanged; we only need to consider multiple queues s_{\mathtt{p}}:(h\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k)~{} for each participant $\mathtt{p}$ in the session (where $h$ is the input part $h$ and $k$ is the output part, as before). Intuitively, the communication of a message $m$ from $\mathtt{p}$ to $\mathtt{q}$ now operates as follows. First, the process implementation for $\mathtt{p}$ enqueues a message $\langle\mathtt{q},m\rangle$ to the output part of its own queue; subsequently, the message is moved to the input part of $\mathtt{q}$’s queue, where it is renamed as $\langle\mathtt{p},m\rangle$ to make its provenance explicit.

More formally, the rules in Fig. 17 and Fig. 18 define the alternative evaluation-closed forward and backward reduction relations, denoted {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\rightharpoonup}\, and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\rightharpoondown}\,.111For conciseness, Fig. 17 contains only rules for input-output communication; other rules follow similar lines. Rule (Init∗) is similar to Rule (Init) in Fig. 6 but it initialises a local queue for each participant in the given protocol $G$. Rules (Out∗) and (In∗) make the above intuitions formal by defining how communication operates when using separate queues for participants, ensuring that output and input steps must be supported by appropriate types in the monitors for $\mathtt{p}$ and $\mathtt{q}$. In particular, notice how Rule (In∗) involves the two different local queues (for $\mathtt{p}$ and for $\mathtt{q}$) and renames the participant mentioned in the message. Rules (RInit∗), (RollS∗), (ROut∗), and (RIn∗) are the corresponding backward rules, which are defined similarly as before because the tags ‘$\lozenge$’ and ‘{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\blacklozenge}’ are attached to monitors, rather than to queues. The equivalence on queues given by Definition 2.3.1 needs to be revised as follows:

{defi}

[Equivalence on message queues, revised] We define the structural equivalence on queues, denoted $\equiv_{\mathsf{q}}$, as follows:

[TABLE]

whenever $\mathtt{p}_{1}\neq\mathtt{p}_{2}$. The equivalence $\equiv_{\mathsf{q}}$ extends to configurations $M$ as expected.

The difference between the two decoupled semantics is in the shape of the queues. The following definition makes this difference precise.

{defi}

[From Single to Local Queues] Given s:(h\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k), a single queue as defined in Fig. 4, the local queue of participant $\mathtt{p}$ is s_{\mathtt{p}}:(h\lfloor\mathtt{p}\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k\rfloor\mathtt{p}), where:

[TABLE]

Given a reachable configuration $M$ (Def. 3.1) for a protocol with participants $\{\mathtt{p}_{1},\cdots,\mathtt{p}_{n}\}$, we write $[M]\!\!\downharpoonleft\!\downharpoonright$ to denote the configuration obtained from $M$ by (i) removing the single queue s:(h\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k) and (ii) adding in parallel a local queue s_{\mathtt{p}_{i}}:(h\lfloor\mathtt{p}_{i}\,{\color[rgb]{0.99,0.57,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.99,0.57,0}\pgfsys@color@cmyk@stroke{0}{0.42}{1}{0.01}\pgfsys@color@cmyk@fill{0}{0.42}{1}{0.01}\mathbf{\star}}\,k\rfloor\mathtt{p}_{i}) for each $\mathtt{p}_{i}\in\{\mathtt{p}_{1},\cdots,\mathtt{p}_{n}\}$.

Example 4.1**.**

Recall configuration $M_{7}$ as in § 2.3.3:

[TABLE]

where {\mathbb{T}_{7}\left[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\bullet}\right]}, $\sigma_{7}$, {\mathbb{T}_{8}\left[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\bullet}\right]}, $\sigma_{8}$, are as before and $h_{7}$ is as follows:

[TABLE]

Then, applying Def. 4.1, we obtain:

[TABLE]

where the difference with respect to $M_{7}$ is in the last line, with the following local queues:

[TABLE]

We now relate the decoupled semantics (given by {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}\cup{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}) with the alternative decoupled semantics (given by {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\rightharpoonup}\,\cup{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\rightharpoondown}\,) by means of the following correspondence:

Proposition 14**.**

Let $M$ be a reachable configuration. We have:

1. (1)

M{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}M^{\prime} if and only if [M]\!\!\downharpoonleft\!\downharpoonright{\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\rightharpoonup}\,[M^{\prime}]\!\!\downharpoonleft\!\downharpoonright. 2. (2)

[M]\!\!\downharpoonleft\!\downharpoonright{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,}[M^{\prime}]\!\!\downharpoonleft\!\downharpoonright if and only if M{\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\rightharpoondown}\,M^{\prime}.

Proof 4.2**.**

Immediate from the definitions of $[\cdot]\!\!\downharpoonleft\!\downharpoonright$, {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\,\curvearrowright\,}, and {\color[rgb]{0,0.8,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.8,0.9}\pgfsys@color@cmyk@stroke{1}{0.1}{0}{0.1}\pgfsys@color@cmyk@fill{1}{0.1}{0}{0.1}\rightharpoonup}\, (resp. {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\,\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{\curvearrowright}}}\,} and {\color[rgb]{1,0.1,0.14}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.1,0.14}\pgfsys@color@cmyk@stroke{0}{0.90}{0.86}{0}\pgfsys@color@cmyk@fill{0}{0.90}{0.86}{0}\rightharpoondown}\,).

This tight correspondence between the original and alternative decoupled semantics ensures that our main results (in particular, causal consistency) carry over to a setting in which each participant handles its own queue for messages.

4.2. Related Work

Reversibility in concurrency has received much attention in the last decade. A detailed overview of the literature on the intersection between reversibility and behavioral contracts/types appears in [MSG*+*20]. Within this research line, the works most related to ours are [TY16, DG16, CDG17, CDG19, FMT18, FMT20, BLd18, NY17, Kap20].

Tiezzi and Yoshida [TY16] study the cost of implementing different ways of reversing binary and multiparty sessions; since they work in a synchronous setting, these alternatives are simpler or incomparable to our asynchronous, decoupled rollback.

In a series of works, Dezani-Ciancaglini et al. have developed multiparty session types with checkpoints [DG16, CDG17, CDG19]. These checkpoints are choice points in the global protocol to which the computation may return. The initial theory has been presented in [DG16] and further developed in [CDG17], with improvements that include a more liberal syntax for processes and types and refined representations for past communications. The work in [CDG19] extends [CDG17] with flexible choices and connecting communications, allowing for different sets of participants in each branch. The intuition is that in some parts of the protocol (as delimited by a choice construct) some participants are required to take part in the interaction, while some others may be optional.

We briefly compare our approach with respect to the framework in [CDG17]. While our reversible actions are embedded in/guaranteed by the semantics, rollbacks in [CDG17] should specify the name of the checkpoint to which computation should revert. Defining reversibility in [CDG17] requires modifying both processes and types. In contrast, we consider untyped processes governed by local types (with cursors) as monitors. While we show causal consistency with a direct proof, in [CDG17] causal consistency follows indirectly, as a consequence of typing. Another difference with respect to [CDG17] is that reversibility in our model is fine-grained, in that we allow reversible actions concerning exactly two of the protocol participants; in [CDG17], when a checkpoint is taken, also parties not related with that choice are forced to return to a checkpoint. A distinctive aspect of [CDG17] is that when a branch of a choice is reversed, it is discarded: this way, the same choice is not redone in the future. We have chosen to be more liberal, as the same action can be done and redone infinite times. To encode this behavior, we could use the reversibility modes—annotations that describe the reversibility capabilities of the processes governed by types)—that we introduced in [MP17b].

Similarly to our work, Francalanza et al. [FMT18, FMT20] use monitors that enact reversibility by storing the decision points (e.g., distributed choices) that the different participants may take, and by coordinating with each other in order to bring the system back to a previous consistent state when certain conditions are met. To do so, they extend the global graphs by Tuosto and Guanciale [TG18] (a formalism that expresses the behaviour of a message passing system from a global point of view) with a decoration on choices, which includes a condition dictating when a computation on a particular branch of a distributed choice should be reversed. Then, these extended global descriptions can be used to (i) synthesise actors implementing the normal (forward) local behaviour of the system prescribed by the global graph, but also (ii) synthesise monitors that are able to coordinate a distributed rollback when certain conditions (denoting abnormal behaviour) are met. Their synthesis algorithm produces Erlang code, with two actors per participant derived from the global graph: one implements the normal/forward behaviour of the participant; the second one (a monitor) implements its backward behaviour. Reversibility is confined into distributed choices, and triggered by conditions on the internal state of some participants. In contrast, in our framework every communication step can be undone; the mechanism devised in [FMT18, FMT20] can be encoded in an extension of our framework with conditional reversibility.

Neykova and Yoshida  [NY17] develop a recovery algorithm for Erlang programs by exploiting causal information induced by global protocols. They then show that their recovery algorithm outperforms Erlang’s built-in recovery algorithm.

Behavioural contracts are abstract descriptions of expected communication patterns followed by either clients or servers during their interaction. They come naturally equipped with a notion of compliance: when a client and a server follow compliant contracts, their interaction is guaranteed to progress or successfully complete. Barbanera et al. [BLd18] study two extensions of behavioural contracts: (i) retractable contracts dealing with backtracking and (ii) speculative contracts dealing with speculative execution. These two extensions give rise to the same notion of compliance. As a consequence, they also give rise to the same subcontract relation, which determines when one server can be replaced by another while preserving compliance.

From a global specification (e.g., a global graph) an abstract semantics can be derived [GT19]. The semantics is abstract since it is given in terms of a partial order of events, representing the causality induced by the global specification. Recently, Kapus-Kolar [Kap20] has enhanced this abstract semantics to account for reversibility. Here, the assumption is that a global graph is realizable (i.e., the projection function can be defined on all participants) and that each automata implementing the behaviour of a single participant has an inverse. Then, it is shown that the causality induced by the global specification is preserved also while going backwards.

5. Concluding Remarks

We have presented a process framework of reversible, multiparty protocols built upon session-based concurrency. As illustrated throughout the paper, the distinguishing features of our framework (decoupled rollbacks and abstraction passing, including delegation) endow it with substantial expressiveness, improving on and distinguishing it from prior works.

Our processes/configurations are untyped, but their (reversible) behaviour is governed by monitors derived from local (session) types. In our view, our monitored approach to reversibility is particularly appropriate for specifying and reasoning about systems with components whose behaviour may not be statically analyzed (e.g., legacy components or services available as black-boxes). A monitored approach is general enough to support also the analysis of reversible systems that combine typed and untyped components.

We proved that our reversible semantics is causally consistent, which ensures that reversing a computation leads to a state that could have been reached by performing only forward steps. The proof is challenging (and, in our view, also interesting), as we must resort to an alternative atomic semantics for rollbacks (Fig. 12 and 13). We then connected reversibility at the level of process/configurations with reversibility at the level of global types, therefore linking the operational and declarative levels of abstraction typical of multiparty sessions communication-centric software systems.

Extensions and Future Work

As already mentioned, our framework does not include name passing, which is known to be representable, in a fully abstract way, using name abstractions [KPY16]. Primitive support for name passing is not difficult, but would come at the cost of additional notational burden. An extension with name passing would allow us to relate our framework with known typed frameworks for monitored networks (without reversibility) based on multiparty sessions [BCD*+*17].

In future work, we plan to extend our framework with reversibility modes [MP17b], which implement controlled reversibility [LMSS11] by specifying how many times a particular protocol step can be reversed—zero (e.g., it is an atomic action), one, or infinite times. (Currently, all actions can be reversed infinite times.) In a related vein, we plan to explore variants of our model in which certain protocol branches are “forgotten” after they have been reversed; this modification is delicate, because it would weaken the notion of causal consistency.

On the practical side, the work [dVP19] describes a Haskell implementation of our reversible model, where algebraic types are used to represent all the various formal ingredients defined in § 2. We plan to keep improving this implementation, as we believe that pure functional languages support natively reversibility. In this direction, it would be beneficial to have a “reversible workbench” to test and compare all the different semantics of the aforementioned reversible behavioural types.

Acknowledgements

We are grateful to Peter D. Mosses for useful exchanges and suggestions. We would also like to thank the anonymous reviewers for their valuable suggestions and constructive feedback.

Mezzina has been partially supported by the French ANR project DCore ANR-18-CE25-0007 and by the Italian INdAM - GNCS 2020 project ‘Sistemi Reversibili Concorrenti: dai Modelli ai Linguaggi’. Pérez has been partially supported by the Dutch Research Council (NWO) under project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).