Explicit Identifiers and Contexts in Reversible Concurrent Calculus

Abstract

Existing formalisms for the algebraic specification and representation of networks of reversible agents suffer some shortcomings. Despite multiple attempts, reversible declensions of the Calculus of Communicating Systems (CCS) do not offer satisfactory adaptation of notions usual in “forward-only” process algebras, such as replication or context. Existing formalisms disallow the “hot-plugging” of processes during their execution in contexts with their own past. They also assume the existence of “eternally fresh” keys or identifiers that, if implemented poorly, could result in unnecessary bottlenecks and look-ups involving all the threads. In this paper, we begin investigating those issues, by first designing a process algebra endowed with a mechanism to generate identifiers without the need to consult with the other threads. We use this calculus to recast the possible representations of non-determinism in CCS, and as a by-product establish a simple and straightforward definition of concurrency. Our reversible calculus is then proven to satisfy expected properties. We also observe that none of the reversible bisimulations defined thus far are congruences under our notion of “reversible” contexts.

This work has been supported by French ANR project DCore ANR-18-CE25-0007.

1 Introduction: Filling the Blanks in Reversible Process Algebras

Reversibility’s Future is intertwined with the development of formal models for analyzing and certifying concurrent behaviors. Even if the development of quantum computers [30], CMOS adiabatic circuits [18] and computing biochemical systems promise unprecedented efficiency or “energy-free” computers, it would be a mistake to believe that whenone of those technologies—each with their own connection to reversibility—reaches a mature stage, distribution of the computing capacities will become superfluous. On the opposite, the future probably resides in connecting together computers using different paradigms (i.e., “traditional”, quantum, biological, etc.), and possibly themselves heterogeneous (for instance using the “classical control of quantum data” motto [37]). In this coming situation, “traditional” model-checking techniques will face an even worst state explosion problem in presence of reversibility, that e.g. the usual “back-tracking” methods will likely fail to circumvent. Due to the notorious difficulty of connecting heterogeneous systems correctly and the “volatile” nature of reversible computers—that can erase all trace of their actions—, it seems absolutely necessary to design languages for the specification and verification of reversible distributed systems.

Process Algebras offer an ideal touch of abstraction while maintaining implementable specification and verification languages. In the family of process calculi, the Calculus of Communicating Systems (CCS) [35] plays a particular role, both as seminal work and as direct root of numerous systems (e.g. $\pi$- [42], Ambient [33], applied [1] and distributed [23] calculi). Reversible CCS (RCCS) [15] and CCS with keys (CCSK) [38] are two extensions to CCS providing a better understanding of the mechanisms underlying reversible concurrent computation—and they actually turned out to be the two faces of the same coin [27]. Most [3, 14, 32, 34]—if not all—of the later systems developed to enhance the expressiveness with some respect (rollback operator, name-passing abilities, probabilistic features) stem from one approach or the other. However, those two systems, as well as their extensions, both share the same drawbacks, in terms of missing features and missing opportunities.

An Incomplete Picture is offered by RCCS and CCSK, as they miss “expected” features despite repetitive attempts. For instance, no satisfactory notion of context was ever defined: the discussed notions [5] do not allow the “hot-plugging” of a process with a past into a context with a past as well. As a consequence, defining congruence is impossible, forbidding the study of bisimilarities—though they are at the core of process algebras [41]. Also, recursion and replication are different [36], but only recursion have been investigated [22, 25] or mentioned [15, 16], and only for “memory-less” processes. Stated differently, the study of the duplication of systems with a past has been left aside.

Opportunities Have Been Missed as previous process algebras are conservative extensions of restricted versions of CCS, instead of considering “a fresh start”. For instance, reversible calculi inherited the sum operator in its guarded version: while this restriction certainly makes sense when studying (weak) bisimulations for forward-only models, we believe it would be profitable to suspend this restriction and consider all sums, to establish their specificities and interests in the reversible frame. Also, both RCCS and CCSK have impractical mechanisms for keys or identifiers: aside from supposing “eternal freshness”—which requires to “ping” all threads when performing a transition, creating a potential bottle-neck—, they also require to inspect, in the worst case scenario, all the memories of all the threads before performing a backward transition.

Our Proposal for “yet” another language is guided by the desire to “complete the picture”, but starts from scratch instead of trying to “correct” existing systems¹. We start by defining an “identified calculus” that sidesteps the previous limitations of the key and memory mechanisms and considers multiple declensions of the sum: 1. the summation [35, p. 68], that we call “non-deterministic choice” and write , [44], 2. the guarded sum, $+$, and 3. the internal choice, $\sqcap$, inspired from the Communicating Sequential Processes (CSP) [24]—even if we are aware that this operator can be represented [2, p. 225] in forward systems, we would like to re-consider all the options in the reversible set-up, where “representation” can have a different meaning.Our formalism meets the usual criterion, and allows to sketch interesting definitions for contexts, that allows to prove that, even under a mild notion of context, the usual bisimulation for reversible calculi is not a congruence. As a by-product, we obtain a notion of concurrency, both for forward and forward-and-backward calculi, that rests solely on identifiers and can be checked locally.

Our Contribution tries to lay out a solid foundation to study reversible process algebras in all generality, and opens some questions that have been left out. Our detailed frame explicits aspects not often acknowledged, but does not yet answer questions such as “what is the right structural congruence for reversible calculi” [7]: while we can define a structural relation for our calculus, we would like to get a better take on what a congruence for reversible calculi is before committing. How our three sums differ and what benefits they could provide is also left for future work, possibly requiring a better understanding of non-determinism in the systems we model. Another direction for future work is to study new features stemming from reversibility, such as the capacity of distinguishing between multiple replications, based on how they replicate the memory mechanism allowing to reverse the computation.

All proofs and some ancillary definitions are in the extended version [8].

2 Forward-Only Identified Calculus with Multiple Sums

We enrich CCS’s processes and labeled transition system (LTS) with identifiers needed to define reversible systems: indeed, in addition to the usual labels, the reversible LTS developed thus far all annotate the transition with an additional key or identifier that becomes part of the memory. This development can be carried out independently of the reversible aspect, and could be of independent interest. Our formal “identifier structures” allows to precisely define how such identifiers could be generated while guaranteeing eternal freshness of the identifiers used to annotate the transitions (Lemma 1) of our calculus that extends CCS conservatively (Lemma 2).

2.1 Preamble: Identifier Structures, Patterns, Seeds and Splitters

Definition 1 (Identifier Structure and Pattern)

An identifier structure $\mathsf {IS}= (\mathsf {I}, \gamma , \oplus )$ is s.t.

• $\mathsf {I}$ is an infinite set of identifiers, with a partition between infinite sets of atomic identifiers $\mathsf {I}_a$ and paired identifiers $\mathsf {I}_p$, i.e. $\mathsf {I}_a \cup \mathsf {I}_p = \mathsf {I}$, $\mathsf {I}_a \cap \mathsf {I}_p = \emptyset$,

• $\gamma : \mathbb {N}\rightarrow \mathsf {I}_a$ is a bijection called a generator,

• $\oplus : \mathsf {I}_a \times \mathsf {I}_a \rightarrow \mathsf {I}_p$ is a bijection called a pairing function.

Given an identifier structure $\mathsf {IS}$, an identifier pattern $\mathsf {ip}$ is a tuple $(c,s)$ of integers called current and step such that $s > 0$. The stream of atomic identifiers generated by $(c,s)$ is $\mathsf {IS}(c,s) = \gamma (c), \gamma (c + s), \gamma (c + s + s), \gamma (c +s +s+s),\ldots$.

Example 1

Traditionally, a pairing function is a bijection between $\mathbb {N}\times \mathbb {N}$ and $\mathbb {N}$, and the canonical examples are Cantor’s bijection and $(m, n) \mapsto 2^m(2n+1)-1$ [40, 43]. Let $\mathrm {p}$ be any of those pairing function, and let $\mathrm {p}^{-}(m, n) = -(\mathrm {p}(m, n))$.

Then, $\mathsf {I}{\mathbb {Z}}= (\mathbb {Z}, \mathrm {id}_{\mathbb {N}}, \mathrm {p}^{-})$ is an identifier structure, with $\mathsf {I}_a = \mathbb {N}$ and $\mathsf {I}_p = \mathbb {Z}^{-}$. The streams $\mathsf {I}{\mathbb {Z}}(0, 2)$ and $\mathsf {I}{\mathbb {Z}}(1, 2)$ are the series of even and odd numbers.

We now assume given an identifier structure $\mathsf {IS}$ and use $\mathsf {I}{\mathbb {Z}}$ in our examples.

Definition 2 (Compatible Identifier Patterns)

Two identifier patterns $\mathsf {ip}_1$ and $\mathsf {ip}_2$ are compatible, $\mathsf {ip}_1 \perp \mathsf {ip}_2$, if the identifiers in the streams $\mathsf {IS}(\mathsf {ip}_1)$ and $\mathsf {IS}(\mathsf {ip}_2)$ are all different.

Definition 3 (Splitter)

A splitter is a function from identifier pattern to pairs of compatible identifier patterns, and we let (resp. ) be its first (resp. second) projection.

We now assume that every identifier structure $\mathsf {IS}$ is endowed with a splitter.

Example 2

For $\mathsf {I}{\mathbb {Z}}$ the obvious splitter is . Note that , and it is easy to check that the two streams $\mathsf {I}{\mathbb {Z}}(0, 2)$ and $\mathsf {I}{\mathbb {Z}}(1, 2)$ have no identifier in common. However, $(1, 7)$ and $(2, 13)$ are not compatible in $\mathsf {I}{\mathbb {Z}}$, as their streams both contain $15$.

Definition 4 (Seed (Splitter))

A seed $\mathsf {s}$ is either an identifier pattern $\mathsf {ip}$, or a pair of seeds $(\mathsf {s}_1, \mathsf {s}_2)$ such that all the identifier patterns occurring in $\mathsf {s}_1$ and $\mathsf {s}_2$ are pairwise compatible. Two seeds $\mathsf {s}_1$ and $\mathsf {s}_2$ are compatible, $\mathsf {s}_1 \perp \mathsf {s}_2$, if all the identifier patterns in $\mathsf {s}_1$ and $\mathsf {s}_2$ are compatible.

We extend the splitter and its projections (for $j \in \{1, 2\}$) to functions from seeds to seeds that we write and defined by

Example 3

A seed over $\mathsf {I}{\mathbb {Z}}$ is .

2.2 Identified CCS and Unicity Property

We will now discuss and detail how a general version of (forward-only) CCS can be equipped with identifiers structures so that every transition will be labeled not only by a (co-)name, $\tau$ or $\upsilon$², but also by an identifier that is guaranteed to be unique in the trace.

Definition 5 (Names, Co-names and Labels)

Let $\mathsf {N}=\{a,b,c,\dots \}$ be a set of names and $\overline{\mathsf {N}}=\{\overline{a},\overline{b},\overline{c},\dots \}$ its set of co-names. We define the set of labels $\mathsf {L}= \mathsf {N}\cup \overline{\mathsf {N}} \cup \{\tau , \upsilon \}$, and use $\alpha$ (resp. $\mu$, $\lambda$) to range over $\mathsf {L}$ (resp. $\mathsf {L}\backslash \{\tau \}$, $\mathsf {L}\backslash \{\tau , \upsilon \}$). The complement of a name is given by a bijection $\overline{\cdot }:\mathsf {N}\rightarrow \overline{\mathsf {N}}$, whose inverse is also written $\overline{\cdot }$.

Definition 6 (Operators)

As usual, the inactive process $0$ is not written when preceded by a prefix, and we call $P$ and $Q$ the “threads” in a process $P \mid Q$.

The labeled transition system (LTS) for this version of CCS, that we denote , can be read from Fig. 1 by removing the seeds and the identifiers. Now, to define an identified declension of that calculus, we need to describe how each thread of a process can access its own identifier pattern to independently “pull” fresh identifiers when needed, without having to perform global look-ups. We start by defining how a seed can be “attached” to a CCS process.

Definition 7 (Identified Process)

Given an identifier structure $\mathsf {IS}$, an identified process is a CCS process $P$ endowed with a seed $\mathsf {s}$ that we denote $\mathsf {s}\circ P$.

We assume fixed a particular identifier structure , and now need to introduce how we “split” identifier patterns, to formalize when a process evolves from e.g. $\mathsf {ip}\circ a.(P\mid Q)$ that requires only one identifier pattern to $(\mathsf {ip}_1, \mathsf {ip}_2) \circ P \mid Q$, that requires two—because we want $P$ and $Q$ to be able to pull identifiers from respectively $\mathsf {ip}_1$ and $\mathsf {ip}_2$ without the need for an agreement. To make sure that our processes are always “well-identified” (Definition 10), i.e. with a matching number of threads and identifier patterns, we introduce an helper function.

Definition 8 (Splitter Helper)

Given a process $P$ and an identifier pattern $\mathsf {ip}$, we define

and write e.g. for the “recomposition” of the pair into the identified process .

Note that in the definition below, only the rules act., $+$ and $\sqcap$ can “uncover” threads, and hence are the only place where is invoked.

Definition 9 (ILTS)

We let the identified labeled transition system between identified processes be the union of all the relations for $i \in \mathsf {I}$ and $\alpha \in \mathsf {L}$ of Fig. 1. Structural relation is as usual [8] but will not be used.

Fig. 1.

Rules of the identified labeled transition system (ILTS)

Example 4

The result of is $((0, 2), ((1, 4), (3, 4))) \circ (a \mid (b \mid (c+d))$, and $a$ (resp. $b$, $c+d$) would get its next transition identified with $0$ (resp. $1$, $3$).

Definition 10 (Well-Identified Process)

An identified process $\mathsf {s}\circ P$ is well-identified iff $\mathsf {s}= (\mathsf {s}_1, \mathsf {s}_2)$, $P = P_1 \mid P_2$ and $\mathsf {s}_1 \circ P_1$ and $\mathsf {s}_2 \circ P_2$ are both well-identified, or $P$ is not of the form $P_1 \mid P_2$ and $\mathsf {s}$ is an identifier pattern.

We now always assume that identified processes are well-identified.

Definition 11 (Traces)

In a transition , process $\mathsf {s}\circ P$ is the source, and $\mathsf {s}'\circ P'$ is the target of transition $t$. Two transitions are coinitial (resp. cofinal) if they have the same source (resp. target). Transitions $t_1$ and $t_2$ are composable, $t_1;t_2$, if the target of $t_1$ is the source of $t_2$. A sequence of pairwise composable transitions is called a trace, written $t_1; \cdots ; t_n$.

Lemma 1 (Unicity)

The trace of an identified process contains any identifier at most once, and if a transition has identifier $i_1 \oplus i_2 \in \mathsf {I}_p$, then neither $i_1$ nor $i_2$ occur in the trace.

Lemma 2

For all CCS process $P$, $\exists \mathsf {s}$ s.t. .

Definition 12 (Concurrency and Compatible Identifiers)

Two coinitial transitions and are concurrent iff $i_1$ and $i_2$ are compatible, $i_1 \perp i_2$, i.e. iff

Example 5

The identified process $\mathsf {s}\circ P = ((0, 2), (1, 2)) \circ a + b \mid \overline{a}.c$ has four possible transitions:

Among them, only $t_1$ and $t_3$, and $t_2$ and $t_3$ are concurrent: transitions are concurrent when they do not use overlapping identifiers, not even as part of synchronizations.

Hence, concurrency becomes an “easily observable” feature that does not require inspection of the term, of its future transitions—as for “the diamond property” [29]—or of an intermediate relation on proof terms [11, p. 415]. We believe this contribution to be of independent interest, and it will help significantly the precision and efficiency of our forward-and-backward calculus in multiple respect.

3 Reversible and Identified CCS

A reversible calculus is always defined by a forward calculus and a backward calculus. Here, we define the forward part as an extension of the identified calculus of Definition 9, without copying the information about the seeds for conciseness, but using the identifiers they provide. The backward calculus will require to make the seed explicit again, and we made the choice of having backward transitions re-use the identifier from their corresponding forward transition, and to restore the seed in its previous state. Expected properties are detailed in Sect. 3.2.

3.1 Defining the Identified Reversible CCS

Definition 13 (Memories and Reversible Processes)

Let , $d \in \{\mathrm {L}, \mathrm {R}\}$, we define memory events, memories and identified reversible processes as follows, for $n \geqslant 0$:

In a memory event, if $n = 0$, then we will simply write $\_$. We generally do not write the trailing empty memories in memory stacks, e.g. we will write $e$ instead of $e.\emptyset$.

Stated differently, our memory are represented as a stack or tuples of stacks, on which we define the following two operations.

Definition 14 (Operations on Memories)

The identifier substitution in a memory event is written and is defined as substitutions usually are. The identified insertion is defined by

The operations are easily extended to memories by simply propagating them to all memory events.

When defining the forward LTS below, we omit the identifier patterns to help with readability, but the reader should assume that those rules are “on top” of the rules in Fig. 1. The rules for the backward LTS, in Fig. 3, includes both the seeds and memories, and is the exact symmetric of the forward identified LTS with memory, up to the condition in the parallel group that we discuss later. A bit similarly to the splitter helper (Definition 8), we need an operation that duplicates a memory if needed, that we define on processes with memory but without seeds for clarity.

Definition 15 (Memory Duplication)

Given a process $P$ and a memory $m$, we define

and write e.g. $\delta ^?(m) \rhd a \mid b$ for the “recomposition” of the pair of identified processes $\delta ^?(m, a \mid b) = (\delta ^?(m, a), \delta ^?(m, b)) = (m \rhd a, m \rhd b)$ into the process $[m, m] \rhd a \mid b$.

Definition 16 (IRLTS)

We let the identified reversible labeled transition system between identified reversible processes be the union of all the relations and for $i \in \mathsf {I}$ and $\alpha \in \mathsf {L}$ of Figs. 2 and 3, and let $\twoheadrightarrow =\rightarrow \cup \rightsquigarrow$. Structural relation is as usual [8] but will not be used.

Fig. 2.

Forward rules of the identified reversible labeled transition system (IRLTS)

In its first version, RCCS was using the whole memory as an identifier [15], but then it moved to use specific identifiers [4, 31], closer in inspiration to CCSK’s keys [38]. This strategy, however, forces the act. rules (forward and backward) to check that the identifier picked (or present in the memory event that is being reversed) is not occurring in the memory, while our system can simply pick identifiers from the seed without having to inspect the memory, and can go backward simply by looking if the memory event has identifier in $\mathsf {I}_a$—something enforced by requiring the identifier to be of the form $\gamma ^{-1}(c)$. Furthermore, memory events and annotated prefixes, as used in RCCS and CCSK, do not carry information on whenever they synchronized with other threads: retrieving this information require to inspect all the memories, or keys, of all the other threads, while our system simply observes if the identifier is in $\mathsf {I}_p$, hence enforcing a “locality” property. However, when backtracking, the memories of the threads need to be checked for “compatibility”, otherwise i.e. $((1, 2), (2, 2)) \circ [\langle {0, a, \_}\rangle , \langle {0, a, \_}\rangle ] \rhd P \mid Q$ could backtrack to $((1, 2), (0, 2)) \circ [\langle {0, a, \_}\rangle , \emptyset ] \rhd P \mid a.Q$ and then be stuck instead of $(0, 1) \circ \emptyset \rhd a.(P \mid Q)$.

Fig. 3.

Backward rules of the identified reversible labeled transition system (IRLTS)

3.2 Properties: From Concurrency to Causal Consistency and Unicity

We now prove that our calculus satisfies typical properties for reversible process calculi [13, 15, 26, 38]. Notice that showing that the forward-only part of our calculus is a conservative extension of CCS is done by extending Lemma 2 to accommodate memories and it is immediate. We give a notion of concurrency, and prove that our calculus enjoys the required axioms to obtain causal consistency “for free” [28]. All our properties, as commonly done, are limited to the reachable processes.

Definition 17 (Initial, Reachable and Origin Process)

A process $\mathsf {s}\circ m \rhd P$ is initial if $\mathsf {s}\circ P$ is well-identified and if $m = \emptyset$ if $P$ is not of the form $P_1 \mid P_2$, or if $m = [m_1, m_2]$, $P = P_1 \mid P_2$ and for $j \in \{1, 2\}$ are initial. A process $R$ is reachable if it can be derived from an initial process, its origin, written $O_{R}$, by applying the rules in Figs. 2 and 3.

Concurrency. To define concurrency in the forward and backward identified LTS is easy when both transitions have the same direction: forward transitions will adopt the definition of the identified calculus, and backward transitions will always be concurrent. More care is required when transitions have opposite directions, but the seed provides a good mechanism to define concurrency easily. In a nutshell, the forward transition will be in conflict with the backward transition when the forward identifier was obtained using the identifier pattern(s) that have been used to generate the backward identifier, something we call “being downstream”. Identifying the identifier pattern(s) that have been used to generate an identifier in the memory is actually immediate:

Definition 18

Given a backward transition , we write $\mathsf {ip}_t$ (resp. $\mathsf {ip}_t^1$, $\mathsf {ip}_t^2$) for the unique identifier pattern(s) in $\mathsf {s}'$ such that $i \in \mathsf {I}_a$ (resp. $i_1$ and $i_2$ s.t. $i_1 \oplus i_2 = i \in \mathsf {I}_p$) is the first identifier in the stream generated by $\mathsf {ip}_t$ (resp. are the first identifiers in the streams generated by $\mathsf {ip}_t^1$ and $\mathsf {ip}_t^2$).

Definition 19 (Downstream)

An identifier $i$ is downstream of an identifier pattern $(c, s)$ if

Definition 20 (Concurrency)

Two different coinitial transitions and are concurrent iff

• $t_1$ and $t_2$ are forward transitions and $i_1 \perp i_2$ (Definition 12);

• $t_1$ is a forward and $t_2$ is a backward transition and $i_1$ (or $i_1^1$ and $i_1^2$ if $i_1= i_1^1 \oplus i_1^2$) is not downstream of $\mathsf {ip}_{t_2}$ (or $\mathsf {ip}_{t_2}^1$ nor $\mathsf {ip}_{t_2}^2$);

• $t_1$ and $t_2$ are backward transitions.

Example 6

Re-using the process from Example 5 and adding the memories, after having performed $t_1$ and $t_3$, we obtain the process $\mathsf {s}\circ [m_1,m_2] \rhd 0 \mid c$, where $\mathsf {s}=((2,2),(3,2))$, $m_1=\langle {0, a, (+, b, \mathrm {R})}\rangle$ and $m_2= \langle {1, \overline{a}, \_}\rangle$, that has three possible transitions:

Among them, $t_2$ and $t_3$ are concurrent, as they are both backward, as well as $t_1$ and $t_3$, as $3$ was not generated by $\mathsf {ip}_{t_3} = (0, 2)$. However, as $3$ is downstream of $\mathsf {ip}_{t_2} = (1, 2)$, $t_1$ and $t_2$ are not concurrent.

Causal Consistency. We now prove that our framework enjoys causal consistency, a property stating that an action can be reversed only provided all its consequences have been undone. Causal consistency holds for a calculus which satisfies four basic axioms [28]: Loop Lemma—“any reduction can be undone”—, Square Property—“concurrent transitions can be executed in any order”—, Concurrency (independence) of the backward transitions—“coinitial backward transitions are concurrent”— and Well-foundedness—“each process has a finite past”. Additionally, it is assumed that the semantics is equipped with the independence relation, in our case concurrency relation.

Lemma 3 (Axioms)

For every reachable processes $R$, $R'$, IRLTS satisfies the following axioms:

• Loop Lemma: for every forward transition there exists a backward transition and vice versa.

• Square Property: if and are two coinitial concurrent transitions, there exist two cofinal transitions and .

• Backward Transitions are Concurrent: any two coinitial backward transitions and where $t_1\ne t_2$ are concurrent.

• Well-Foundedness: there is no infinite backward computation.

We now define the “causal equivalence” [15] relation on traces allowing to swap concurrent transitions and to delete transitions triggered in both directions. The causal equivalence relation is defined for the LTSI which satisfies the Square Property and re-use the notations from above.

Definition 21 (Causal Equivalence)

Causal equivalence, $\sim$, is the least equivalence relation on traces closed under composition satisfying $t_1;t'_2 \sim t_2;t'_1$ and $t;t^{\bullet }\sim \epsilon$— $\epsilon$ being the empty trace.

Now, given the notion of causal equivalence, using an axiomatic approach [28] and that our reversible semantics satisfies necessary axioms, we obtain that our framework satisfies causal consistency, given bellow.

Theorem 1 (Causal Consistency)

In IRLTS, two traces are coinitial and cofinal iff they are causally equivalent.

Finally, we give the equivalent to the “unicity lemma” (Lemma 2) for IRLTS: note that since the same transition can occur multiple times, and as backward and forward transitions may share the same identifiers, we can have the exact same guarantee that any transition uses identifiers only once only up to causal consistency.

Lemma 4 (Unicity for IRLTS)

For a given trace $d$, there exist a trace $d'$, such that $d'\sim d$ and $d'$ contains any identifier at most once, and if a transition in $d'$ has identifier $i_1 \oplus i_2 \in \mathsf {I}_p$, then neither $i_1$ nor $i_2$ occur in $d'$.

3.3 Links to RCCS and CCSK: Translations and Comparisons

It is possible to work out an encoding of our IRLTS terms into RCCS and CCSK terms [8]. Our calculus is more general, since it allows multiple sums, and more precise, since the identifier mechanism is explicit, but has some drawbacks with respect to those calculi as well.

While RCCS “maximally distributes” the memories to all the threads, our calculus for the time being forces all the memories to be stored in one shared place. Poor implementations of this mechanism could result in important bottlenecks, as memories need to be centralized: however, we believe that an asynchronous handling of the memory accesses could allow to bypass this limitation in our calculus, but reserve this question for future work. With respect to CCSK, our memory events are potentially duplicated every time the $\delta ^?$ operator is applied, resulting in a space waste, while CCSK never duplicates any memory event. Furthermore, the stability of CCSK’s terms through execution—as the number of threads does not change during the computation—could be another advantage.

We believe the encoding we present to be fairly straightforward, and that it will open up the possibility of switching from one calculus to another based on the needs to distribute the memories or to reduce the memory footprint.

4 Contexts, and How We Do Not Have Congruences yet

We remind the reader of the definition of contexts $C[\cdot ]$ on CCS terms $\mathsf {P}$, before introducing contexts $C^{\mathsf {I}}[\cdot ]$ (resp. $M[\cdot ]$, $C^{\mathsf {R}}[\cdot ]$) on identified terms $\mathsf {I}$ (resp. on memories $\mathsf {M}$, on identified reversible terms $\mathsf {R}$).

Definition 22 (Term Context)

A context $C[\cdot ] : \mathsf {P}\rightarrow \mathsf {P}$ is inductively defined using all process operators and a fresh symbol $\cdot$ (the slot) as follows (omitting the symmetric contexts):

When placing an identified term into a context, we want to make sure that a well-identified process remains well-identified, something that can be easily achieved by noting that for all process $P$ and seed $\mathsf {s}$, is always well-identified, for the following definition of :

Definition 23 (Unifier)

Given a process $P$ and a seed $\mathsf {s}$, we define

Definition 24 (Identified Context)

An identified context $C^{\mathsf {I}}[\cdot ] : \mathsf {I}\rightarrow \mathsf {I}$ is defined using term contexts as .

Example 7

A term $(0, 1) \circ a + b$, in the identified context , gives the term $((0, 2), (1, 2)) \circ a + b \mid \overline{a}$ from Example 5. The term $((0, 2), (1, 2))\circ a \mid b$ placed in the same context would give $((0, 4), (1, 4)), (2, 4)) \circ (a \mid b)\mid \overline{a}$.

To study memory contexts, we write $\mathsf {M}$ for the set of all memories.

Definition 25 (Memory Context)

A memory context $M[\cdot ] : \mathsf {M}\rightarrow \mathsf {M}$ is inductively defined using the operators and operations of Definitions 13, 14 and 15, an “append” operation and a fresh symbol $\cdot$ (the slot) as follows:

Where $e. m = [e.m_1, e.m_2]$and $m . e = [m_1 . e, m_2 . e]$ if $m = [m_1, m_2]$, and $m.e = m' . e . \emptyset$ if $m = m' . \emptyset$.

Definition 26 (Reversible Context)

A reversible context $C^{\mathsf {R}}[\cdot ] : \mathsf {R}\rightarrow \mathsf {R}$ is defined using term and memory contexts as . It is memory neutral if $M[\cdot ]$ is built using only $\cdot$, $[\emptyset , M[\cdot ]]$ and $[M[\cdot ], \emptyset ]$.

Of course, a reversible context can change the past of a reversible process $R$, and hence the initial process $O_{R}$ to which it corresponds (Definition 17).

Example 8

Let $C^{\mathsf {R}}[\cdot ]_1 = [\emptyset , \cdot ] \rhd P \mid C[\cdot ]$ and $C^{\mathsf {R}}[\cdot ]_2 = \delta ^?[\cdot ] \rhd P \mid C[\cdot ]$. Letting $R = (1, 1) \circ \langle {0, a, \_}\rangle \rhd b$, we obtain $C^{\mathsf {R}}[R]_1 = ((1, 2), (2, 2)) \circ [\emptyset , \langle {0, a, \_}\rangle ] \rhd P \mid b$ and $C^{\mathsf {R}}[R]_2 = ((1, 2), (2, 2)) \circ [\langle {0, a, \_}\rangle , \langle {0, a, \_}\rangle ] \rhd P \mid b$, and we have

Note that not all of the reversible contexts, when instantiated with a reversible term, will give accessible terms. Typically, the context $[\emptyset , \cdot ] \rhd \cdot$ will be “broken” since the memory pair created will never coincide with the structure of the term and its memory inserted in those slots. However, even restricted to contexts producing accessible terms, reversible contexts are strictly more expressive that term contexts. To make this more precise in Lemma 5, we use two bisimulations close in spirit to Forward-reverse bisimulation [39] and back-and-forth bisimulation [10], but that leave some flexibility regarding identifiers and corresponds to Hereditary-History Preserving Bisimulations [6]. Those bisimulations—B&F and SB&F  [6, 8]—are not congruences, not even under “memory neutral” contexts.

Lemma 5

For all non-initial reversible process $R$, there exists reversible contexts $C^{\mathsf {R}}[\cdot ]$ such $O_{C^{\mathsf {R}}[R]}$ is reachable and for all term context $C[\cdot ]$, $C[O_{R}]$ and $O_{C^{\mathsf {R}}[R]}$ are not B&F.

Theorem 2

B&F and SB&F are not congruences, not even under memory neutral contexts.

Proof

The processes $R_1 = (1, 1) \circ \langle {0, a, \_}\rangle \rhd b+b$ and $R_2 = (1, 1) \circ \langle {0, a, (+, a.b, \mathrm {R})}\rangle \rhd b$ are B&F, but letting $C^{\mathsf {R}}[\cdot ] = \cdot \rhd \cdot + c$, $C^{\mathsf {R}}[R_1]$ and $C^{\mathsf {R}}[R_2]$ are not. Indeed, it is easy to check that $R_1$ and $R_2$, as well as $O_{R_1} = (0, 1) \circ \emptyset \rhd a .(b+b)$ and $O_{R_2} = (0, 1) \circ \emptyset \rhd (a.b) + (a.b)$, are B&F, but $O_{C^{\mathsf {R}}[R_1]} = (0, 1) \circ \emptyset \rhd a.((b+b)+c)$ and $O_{C^{\mathsf {R}}[R_2]} = (0, 1) \circ \emptyset \rhd (a.(b+c))+(a.b)$ are not B&F, and hence $C^{\mathsf {R}}[R_1]$ and $C^{\mathsf {R}}[R_2]$ cannot be either. The same example works for SB&F.

We believe similar reasoning and example can help realizing that none of the bisimulations introduced for reversible calculi are congruences under our definition of reversible context. Some congruences for reversible calculi have been studied [5], but they allowed the context to be applied only to the origins of the reversible terms: whenever interesting congruences allowing contexts to be applied to non-initial terms exist is still an open problem, in our opinion, but we believe our formal frame will allow to study it more precisely.

5 Conclusion

We like to think of our contribution as a first sketch enabling researchers to tackle much more ambitious problems. It is our hope that our identified calculus can at the same time help sidestepping some of the implementation issues for reversible protocols [12], and can be re-used for RCCS or CCSK as a convenient base, or plug-in, to obtain distributed and reliable keys or identifiers. We also hope that the probabilistic choice [17]—whose representation requires to either develop an auxiliary relation [17, p. 67], to make the transition system become probabilistic as well [9], or to use Segala automata [44]—will be within the realm of reversible protocols, as its implications and applications could be numerous. The interleaving of the sums—for instance in the mixed choice [21], that offers both probabilistic choice and nondeterministic choice—could then possibly be unlocked and provides opportunities to model and study more complex behavior without leaving the reversible frame.

It is known that CCS is not “universally expressive” [19, 20], and we would like to assess how universal the protocol detailed in this paper is. To that aim, careful study of reversible and heterogeneous computing devices will be required, that in turns could shed a new light on some of the questions we left unanswered. Typically, this could lead to the development of “location-aware” calculi, where the distribution of seeds and memory is made explicit, or to make progress in the definition of “the right” structural congruence [7]. Last but not least, interesting declensions of contexts were left out in this study, taking for instance a reversible context $\cdot \rhd P$ that “throws away” the term under study but “steals” its memory.