Reversibility and Predictions

Abstract

This paper analyses the introduction of a non-reversible mechanism in a reversible calculus (called $\varOmega \rho \pi$), intended to be used as an oracle which contains persistent memories of previously reversed computation. As a second step, we introduce the notion of weak causal consistency which relaxes the classical causal consistency by allowing the backward semantics not to revert to a previous state, but to a state related to a previous state and we show that $\varOmega \rho \pi$ is weakly causally consistent. We finally present a practical application of this calculus.

1 Introduction

Motivations. Reversibility is the ability, for a system, to undo some actions that were previously taken. We can approach this field from various perspectives such as circuit design, quantum algorithms, automaton, etc. In this paper, we are interested in the application of reversibility to concurrent systems. There already exists multiple works in this context, for debugging [4], for fault tolerance [14, 18], for biological or chemical modelling [1, 2, 7, 16], or even for reliable concurrent programming abstraction [12].

In concurrent systems, the very notion of reversibility is not trivial. Indeed, since reductions are not deterministic, defining the notion of predecessor is less intuitive. For instance, consider the following CCS process [13]: $a.0\ |\ b.0$. There are two possible forward reductions: either $a.0\ |\ b.0 \overset{a}{\rightarrow } b.0$, or $a.0\ |\ b.0 \overset{b}{\rightarrow } a.0$, and both reduce to $0$: both $a.0$ and $b.0$ are predecessors of $0$. Intuitively, reverting to any of those states is acceptable, regardless of the forward sequence.

The standard property of a reversible system is causal consistent reversibility, which captures this intuition. Causal consistent reversibility states that a backward reduction can undo an action, provided that its consequences (if any) are undone beforehand.

There are works which intentionally break causal consistent reversibility. Typical applications include reversible calculi to model chemical reactions with catalyst: an example is a reaction between three molecules $A$, $B$, and $C$, where the objective is to bind $A$ and $B$ together. For the reaction to happen, $B$ first have to bind with the catalyst $C$, to create molecule $BC$, which can in turn bind with $A$, to create $ABC$. Finally, the first binding is reverted, which results in $AB$ and $C$ apart. One can clearly see that such reduction is not causally consistent: the first reaction is reverted while the second holds. Such reversibility is called out-of-causal-order reversibility. Calculi which model such chemical reactions include [16] (which first explicitly mentions out-of-causal-order reversibility) and Kuhn and Ulidowski’s Calculus of Covalent Bonding [6, 7] (in which they distinguish CCB, which is not causally consistent, and CCBs a core calculus which is). [5] compares in detail three out-of-causal-order reversible process calculi, while [15] studies three forms of reversibility (backtracking, causal reversibility, and out-of-causal-order reversibility) in Petri nets.

Breaking causal consistency can also be motivated by practical applications. For instance, in [8], Lanese et al. introduce the croll-$\pi$ calculus, which is a reversible $\pi$-calculus in which, when a memory is reinstalled in a revert sequence, the original process is replaced by a continuation. Such approach is not causally-consistent, stricto sensu¹.

In this paper, we study the relation between algorithms based on trial and error and reversibility. An example of such algorithm is a naive consensus algorithm, in which each process tries its own value, and when it receives a smaller value from a peer, it rolls back and tries again with this smaller value. Such algorithm converges toward a state in which all processes agree on the same value.

Informally, we focus on a class of algorithms that behave in four steps: (i) read the current state; (ii) improve it; (iii) store it; and (iv) start over. Among those four steps, only the second depends on the algorithm. Standard reversible process algebra, such as $\rho \pi$, implement the fourth one (or $\mathtt {roll}-\pi$ [9] for explicit rollback control).

In this paper, our goal is to define a calculus which also covers steps (i) and (iii). In particular, the stored state should not be reverted during backward execution. Another way to view the mechanism is that processes can predict information from the future state of the system. This is the reason why we call the context an oracle.

Our second objective is to characterise the reversible nature of such calculus. Intuitively, such calculus is not causally-consistent, since the state of the store is not reverted. Therefore, we relax the notion of causal-consistency by introducing weak causal consistency. In a nutshell, weak causal consistency takes as parameter a relation $\mathcal {R}$, and allows backward reduction to reach new states (thus breaking regular causal consistency), under the condition that there exists a related state which is reachable using forward only reduction. In particular, for our application, we are interested in a simulation relation. Taking the identity as the parameter relation, our definition falls back on regular causal consistency. We expect this property to be an intermediate point between strong causal consistency and out-of-causal-order reversibility.

Another interesting aspect of this calculus is that the backward semantics is partial, in the sense that its effects are confined to some parts of the term. This notion of partial reversibility is barely discussed in this paper, but we think it is important to explicit it for its potential practical applications.

Approach. At first, we introduce a calculus (called $\varOmega \rho \pi$) based on $\rho \pi$ [10], to which we add two primitives: $\mathtt {inform}\langle \cdot \rangle$ and $\mathtt {forecast}(\cdot ) \triangleright \cdot$. These two primitives are used to interact with a context (which we call the oracle): sending on $\mathtt {inform}\langle \cdot \rangle$ stores a process in the context, and receiving from $\mathtt {forecast}(\cdot ) \triangleright \cdot$ reads the context. The important aspect of the context is that it is preserved through backward reductions.

Introducing these primitives prevents our calculus to be causally consistent: it is possible to revert to the original configuration, but with a different context. Nonetheless, we still have a notion of consistency: a configuration with an uninitialised context can simulate any context. The second part of this work is to characterise this weaker notion of causal consistency.

We finally conclude with a practical application: we implement a distributed Sieve of Eratosthenes.

Contributions. The main contributions of this papers are: (i) a partially reversible calculus $\varOmega \rho \pi$, which adds two primitives to save a process across backward reductions; (ii) the definition of weak causal consistency, which relaxes the usual causal consistency; (iii) a proof that $\varOmega \rho \pi$ is weakly causally consistent; and (iv) an application of $\varOmega \rho \pi$, which illustrates the capabilities and limitations of the calculus.

Outline. The paper is organised as follow: Sect. 2 introduces informally the $\rho \pi$ calculus, on which $\varOmega \rho \pi$ is based, and the notion of simulation which is latter used. Section 3 defines the $\varOmega \rho \pi$ calculus. We explain how the calculus relates to $\rho \pi$ and we argue that the oracle behaves as expected. Section 4 is a small section devoted to the introduction of weak causal consistency. Section 5 shows our main result, which is that $\varOmega \rho \pi$ is weakly causally consistent. Section 6 contains the application example. Finally, Sect. 7 concludes the paper.

2 Preliminary Considerations

In this first section, we present existing work on which the core of this paper is based. In the first subsection, we informally present $\rho \pi$, a reversible variant of the higher-order $\pi$-calculus. In the second subsection, we present the notion of simulation, used in multiple works.

2.1 Informal Introduction to $\rho \pi$

The $\rho \pi$ calculus is a reversible higher-order process calculus, first introduced in [10]. In this section, we informally introduce the $\rho \pi$ calculus, and we refer the interested reader to Lanese’s paper for a more detailed presentation.

Fig. 1.

Syntax of $\rho \pi$

Terms of the $\rho \pi$ calculus (whose syntax is shown in Fig. 1) are composed of a configuration, built up from threads and memories. Threads are themself composed of a process (which is similar to processes of the higher-order $\pi$-calculus)) and a tag, used as an identifier for the process.

The basic building blocks of processes are the emission of a message $P$ on a name $a$ (written $a\langle P\rangle$) and the reception of a message on a name $a$ (written $a(X)\triangleright P$). When a message (for instance $Q$) is received, the free occurrences of $X$ in $P$ are replaced by $Q$, and the resulting process is assigned a new fresh tag. In addition, upon message exchange, a new memory is created, which contains the state of the two processes prior to the message exchange. Informally, the forward reduction rule is the following:

$$k_1 : a\langle P\rangle \ |\ k_2 : a(X)\triangleright Q \twoheadrightarrow \nu k.k : Q\{^{P}/_{X}\}\ |\ [k_1 : a\langle P\rangle \ |\ k_2 : a(X)\triangleright Q; k]$$

In this forward rule, notice that the memory contains the tag of the resulting process. This allows the backward execution of the configuration, by replacing a process by the relevant memory:

$$\begin{aligned} k : P\ |\ [M; k]\rightsquigarrow M \end{aligned}$$

2.2 State Simulation

Given a set of states $\mathbb {S}$ and a reduction relation $\rightarrow$ over states of $\mathbb {S}$, the notion of simulation, originally defined in [17], formalises the statement “any reduction of state $S_1$ can be done by state $S_2$”.

Definition 1 (Weak simulation)

Given two states $S_1, S_2\in \mathbb {S}$, a state $S_2$ simulates another state $S_1$ (noted $S_1\precsim S_2$) if and only if:

$$\forall S_1^\prime \cdot S_1\rightarrow S_1^\prime \Rightarrow \exists S_2^\prime \cdot S_2\rightarrow ^\star S_2^\prime \wedge S_1^\prime \precsim S_2^\prime $$

where $\rightarrow ^\star$ is the reflexive and transitive closure of $\rightarrow$.

Notice that state simulation is reflexive and transitive.

Remark 1

In Sects. 5 and following of this paper, we use a stronger form of simulation in which $S_2\rightarrow S_2^\prime$ and $S_1\rightarrow S_1^\prime$ using the same reduction rule.

3 The $\varOmega \rho \pi$ Calculus

In this first section, we present the $\varOmega \rho \pi$ calculus, which is built on top of the $\rho \pi$ calculus, itself built on top of the higher-order $\pi$ calculus ($\mathtt{HO}\pi$).

Processes of $\mathtt{HO}\pi$ are composed of a multiple sequences of message sending and receiving, with possible name restrictions. The semantics of $\mathtt{HO}\pi$ is that when a process sends a process $P$ and, simultaneously, a process expects to receive a process (variable $X$) on the same channel, then the second process replaces free occurances of $X$ by $P$. The $\rho \pi$ calculus decorates $\mathtt{HO}\pi$ processes in order to allow reverse executions of message communications. The first subsection of this section informally introduces $\rho \pi$.

In $\varOmega \rho \pi$, we decorate $\rho \pi$ configurations with a process. We say a decorated $\rho \pi$ configuration is a context. We obtain the semantics of contexts by lifting the $\rho \pi$ semantics to contexts. To interact with the context, we add two primitives $\mathtt {inform}$ and $\mathtt {forecast}$ (which act as special channels) to write and read the context.

3.1 Syntax

The syntax of the $\varOmega \rho \pi$ calculus is given in Fig. 2. Processes are similar to the regular $\mathtt{HO}\pi$ calculus, with the addition of the inform and forecast primitives. Configurations, tags and memories are similar to those of $\rho \pi$ (up to the addition of the primitives).

Contrary to $\rho \pi$, configurations are not directly executed: there are embedded in a context, which annotates the configuration with a process.

Fig. 2.

Syntax of $\varOmega \rho \pi$. The differences with $\rho \pi$ are highlighted.

Let $\mathbb {C}$ be the set of contexts, $\mathbb {M}$ the set of configurations and $\mathbb {P}$ the set of processes. We let $P$, $Q$ and their decorated variants range over $\mathbb {P}$; $M$, $N$ and their decorated variants range over $\mathbb {M}$ and $C$ and its decorated variants range over $\mathbb {C}$. We say that a context $C$ is initial when it does not contain memory.

Names $a, b, \dots$ take their values from $\mathbb {N}$, which does not contains $\mathtt {forecast}$ and $\mathtt {inform}$.

As in $\rho \pi$, $\tilde{h}$ denotes a vector of keys.

3.2 Semantics

The semantics of $\varOmega \rho \pi$ is defined in two successive parts: first we define the semantics of configurations, as a labelled transition system, then we define the semantics of contexts, using the semantics of configurations. Intuitively, the semantics of configurations acts as the semantics of $\rho \pi$ (up to the required modifications), and the labels of transitions expose the interactions with the oracle. The semantics of contexts simply interprets the labels, updates the oracle accordingly, or constraint the transitions that can be taken by the configurations.

Configuration Semantics. The configuration semantics is defined using two reduction relations (a forward reduction relation $\overset{}{\twoheadrightarrow _c}$ and a backward reduction relation $\overset{}{\rightsquigarrow _c}$). As usual, we use a structural congruence relation (see Fig. 3), which allows to reorder the processes.

Fig. 3.

Structural congruence for $\varOmega \rho \pi$ configurations.

We also use an evaluation context (see Fig. 4). Intuitively, an evaluation context is a process with a hole.

Fig. 4.

Evaluation context

A relation $\mathcal {R}$ over configurations is evaluation-closed if it satisfies the two inference rules in Fig. 5.

Fig. 5.

Inference rules for evaluation-closed relations.

The configuration semantics is defined as the least evaluation-closed relation that satisfies the rules in Fig. 6.

Fig. 6.

Reduction rules of $\varOmega \rho \pi$ configuration semantics.

Reduction rules are heavily based to $\rho \pi$ rules, with the following differences:

• transitions are labeled: reading a process $P$ from the oracle labels the transition with $\overline{P}$, setting the oracle to $P$ labels it with $P$, and all other transitions are labeled with the special symbol $\tau$; and

• memories created by the modification of the oracle do not contain a receiver process.

Notice that the primitives seemingly act like regular channels.

The two rules (C.Fw) and (C.Bw) correspond to the forward and backward rules of the regular $\rho \pi$ calculus: the former perform the exchange of a message, and creates an associated memory, and the backward rule replace a process by the corresponding memory. Notice that, since those two rules do not interact with the oracle, their label is $\tau$.

Rule (C.Inf) allows a process to update the oracle. Since we are at the configuration level, and therefore the oracle is not visible here, this rule simply reduces to an empty process, and emits a label $\overline{P}$, where $P$ is the new process stored in the oracle.

On the other hand, with rule (C.For), a process $\mathtt {forecast}(X) \triangleright Q$ can read a process $P$ from the oracle, and substitute free occurrences of $X$ by $P$ in $Q$. Since we are at the configuration level, the oracle is not visible, and the process $P$ read is not constrained at this point. Instead, a label $P$ is emitted, which is then used below to constraint the reduction.

Global Semantics. The global semantics is defined using two reduction relations: a forward reduction relation (noted $\twoheadrightarrow$) and a backward reduction relation (noted $\rightsquigarrow$), defined according to the reduction rules given in Fig. 7.

Fig. 7.

Reduction rules of $\varOmega \rho \pi$ global semantics.

Silent configuration transitions are simply lifted to the global semantics (rules G.Fw and G.Bw). If the configuration transition exposes a $\overline{Q}$ label, then the context is updated accordingly (rule G.Inform). Notice that we require the newly stored process to simulates the previous one, which captures the intuition of refinement of the stored value². On the other hand, for forecast labels ($P$), the corresponding configuration transition is allowed only if the label matches the context (rule G.Forecast).

We note $\rightarrow$ the semantics of $\varOmega \rho \pi$, defined as $\rightarrow = \twoheadrightarrow \cup \rightsquigarrow$. Also, $\rightarrow ^\star$, $\twoheadrightarrow ^\star$ and $\rightsquigarrow ^\star$ are the transitive and reflective closure of $\rightarrow$, $\twoheadrightarrow$ and $\rightsquigarrow$.

A trace is a sequence of transitions $\sigma = t_1; \dots ; t_n$ with $t_i = C_{i-1} \rightarrow C_i$. When $C_0$ is initial, we call the trace initial. When $t_1; \dots ; t_i$ are the only G.Inform reduction of $\sigma$ (i.e. if none of $t_{i+1}; \dots ; t_n$ is a G.Inform reduction), we call $\sigma$ a forecast sequence ($t_i$ is called the last inform transition of the sequence). A trace that contains only forward (resp. backward) transitions is called forward trace (resp. backward trace). We note $\epsilon$ for an empty trace. Two traces $t_1;\dots ; t_n$ and $t_1^\prime ; \dots ; t_m^\prime$ are said coinitial if $t_1 = C_1\rightarrow C$ and $t^\prime _1 = C_1\rightarrow C^\prime$ and cofinal if $t_n = C\rightarrow C_f$ and $t_m^\prime = C^\prime \rightarrow C_f$.

Example. The example in Fig. 8 shows an execution of a $\varOmega \rho \pi$ context. The initial context is $c\langle P_1\rangle \ |\ {c\langle P_2\rangle }$. This context contains two processes to be read on $c$. The configuration is composed of two threads. The first one (initially with tag $k_1$) reads the context, and then receives one of the two process on $c$ (due to the non-deterministic semantics, the choice is random), and runs it. Intuitively, it launches one of the process at random. Notice, in particular, that if it rolls back to the initial configuration, an other process can be selected during a second attempt. The second process (initially with tag $k_2$), performs a definitive choice. Similarly to the first thread, it selects one of the possible process at random, but contrary to the first thread, it modifies the context to store that choice.

In the example, first $k_1$ reduces, and first chooses process $P_1$, which is run (the two first reductions). At this point, if the process rolls back and restarts, it still has the choice (not shown). After, $k_2$ reads the context, then selects $P_2$, and finally modifies the oracle (transitions $3$, $4$ and $5$). At this point, the selection is definitive³. A sequence of backward reduction revert the configuration in its initial state, but with the context modified. Now, when the first two reduction are replayed, $k_1$ has no choice and selects $P_2$.

Fig. 8.

Example of a $\varOmega \rho \pi$ forward and backward execution. On each line, the part of the term that takes the next transition is coloured in red. The result of the previous transition is coloured in blue on the next line. When the result of the previous transition also takes the next transition, it is coloured in green. (Color figure online)

3.3 Oracle Soundness

In this subsection, we argue that the oracle behaves as expected: we expect that, looking at a trace, any reduction G.Forecast that occurs should forecast $P$, when the previous reduction G.Inform that occurs in the trace sets the oracle with process $P$, regardless of any backward reduction in between (or with the initial $P$ if no G.Inform transition is taken).

More formally, given a trace $\sigma$, for any subtrace $\sigma _{ij} = t_i; \dots ; t_j$ of $\sigma$ with $t_k = M |_{P}\rightarrow N |_{Q}$ the last inform transition of $\sigma _{ij}$, for any $t\in t_{k+1};\dots ;t_j$, $t$ is either G.Fw, G.Bw or G.Forecast with context $Q$.

To begin with, we show that the context does not change, except during G.Inform transition.

Lemma 1

Given a trace $\sigma$ such that the final context is $M |_{P}$.

The last G.Inform reduction (if any) in $\sigma$ is $N |_{Q}\twoheadrightarrow N^\prime |_{P}$.

Proof

By induction on the length of $\sigma$. In the case $\sigma$ is $\epsilon$, then trivially, $Q = P$ and no reduction occurs.

In the case $\sigma = \sigma ^\prime ; t$. Let $N |_{R}$ be the final context of the $\sigma ^\prime$ trace. Let $t$ be $N |_{R}\rightarrow M |_{P}$. We proceed by case analysis of the transition $t$, the cases G.Fw, G.Forecast and G.Bw are trivial. If $t$ is G.Inform, then $t = N |_{R}\twoheadrightarrow M |_{P}$, and it is the last G.Inform transition.

Using this fact, we show that G.Forecast reductions read the context set by the previous G.Inform reduction⁴.

Lemma 2

Given a trace $\sigma = t_1; \dots ; t_n$ with $t_i = M |_{P}\twoheadrightarrow M^\prime |_{Q}$ being the last G.Inform reduction of $\sigma$, then for any G.Forecast reduction $t$ in the subtrace $t_{i+1}; \dots ; t_n$, $t = N |_{Q}\twoheadrightarrow N^\prime |_{Q}$.

Corollary 1 (Oracle soundness)

Given a trace $\sigma$, for any G.Forecast reduction $M |_{P}\twoheadrightarrow M^\prime |_{P}$, the preceding G.Inform transition is $N |_{Q}\twoheadrightarrow N^\prime |_{P}$.

4 Weak Causal Consistency

The $\varOmega \rho \pi$ calculus is not causally consistent: it is possible to inform the oracle and then go back to the initial configuration (up to context), which is, obviously, not reachable using only forward reductions (see Fig. 9: the modification of the oracle happens after —in Lamport terms— the message exchange).

Fig. 9.

Example of a sequence of reductions which leads to a configuration that can not be reached using only forward reductions.

However, our calculus still exhibits an almost causally consistent behaviour: the embedded configuration is the same and the initial $P\ |\ Q$ context is more general than a specific context $P$, in the sense that any reduction with a context $P$ can be done by a context $P\ |\ Q$.

This section formalises this intuition, which we call weak causal consistency. In this section, we consider a generic transition system, with a set of states $\mathbb {S}$, equipped with a forward transition relation $\twoheadrightarrow$ and a backward transition relation $\rightsquigarrow$ and a (general) transition relation $\rightarrow = \twoheadrightarrow \cup \rightsquigarrow$.

$\mathcal {R}$-weak Causal Consistency. Given a relation $\mathcal {R}\subseteq \mathbb {S}\times \mathbb {S}$, a reversible system is $\mathcal {R}$-weakly causally consistent is for each state $C_f$ reachable from an initial state $C_i$, there exists a related state $C_f^\prime$ reachable using only forward transitions. We first define the notion of initial state (a state that can only take forward reductions), and we then formalise our notion of weak causal consistency.

Definition 2 (Initial state)

A state $C_i$ is initial (noted ) if and only if there exists no $C$ such that $C_i\rightsquigarrow C$.

Definition 3 (Weak causal consistency)

A reversible transition system $\varSigma = \langle \mathbb {S}, \twoheadrightarrow , \rightsquigarrow \rangle$ is weakly causally consistent (with respect to $\mathcal {R}$) if and only if:

This definition is intentionally very broad, depending on the chosen $\mathcal {R}$. In the rest of this paper, we will only consider some particular cases. As we will see in the rest of this paper, we think interesting cases include preorder relations, e.g. simulation relation, or other evaluation-closed relations.

Notice that this definition is close to the definition of reversibility developed by Caires et al. in [3] (Definition 3.4).

Remark 2

Notice that if the relation $\mathcal {R}$ we consider is the identity, we fall back on the definition of (strong) causal consistency. Therefore, weak causal consistency is a conservative extension of causal consistency.

5 Weak Causal Consistency of $\varOmega \rho \pi$

In this section, we show that $\varOmega \rho \pi$ is $\precsim$-weakly causally consistent. We can not show weak causal consistency as causal consistency is usually shown (see for instance the proof of causal consistency of the $\rho \pi$ calculus [10], the details of the proof are shown in Mezzina’s thesis [11]), since the loop lemma does not hold in our calculus. Instead, we show the causal consistency in two steps: (i) we show that, if an initial trace $\sigma$ does not contain G.Inform reductions, then there exists a coinitial and cofinal forward trace $\sigma _\twoheadrightarrow$, this is shown by relating this particular trace to an equivalent one in $\rho \pi$ and using the causal consistency of $\rho \pi$; (ii) we show that, for every trace $\sigma$, there is a coinitial and cofinal trace $\sigma _s$ free of G.Inform. A summary of the proof is shown in Fig. 10.

Fig. 10.

Summary of the causal consistence proof: for any trace $\sigma$ (top) from $C_i$ to $C_f$, it is possible to find a coinitial and cofinal trace $\sigma _s$. Aside, we show that any G.Inform free trace (in particular $\sigma _s$) of the $\varOmega \rho \pi$ calculus can be played in $\rho \pi$ calculus ($\sigma _s^{\rho \pi }$, bottom left). We introduce a function $f_{\sigma _s}$ to do the conversion. Since $\rho \pi$ is causally consistent, there necessarily exists an equivalent forward sequence $\sigma _\twoheadrightarrow ^{\rho \pi }$ (middle left), which can finally be played instead of $\sigma _g$ ($\sigma _\twoheadrightarrow$, top left).

5.1 States Simulation

As we have seen in the previous section, weak causal consistency relies on states simulating each other. Hence, we first exhibit some similar states we will rely on in the subsequent sections.

First, a term with $P$ in the context simulates any term composed of the same configuration and a process $Q$ such that $P\precsim Q$ in the context. This is trivial, since $\precsim$ is evaluation closed.

Lemma 3

$\forall M\in \mathbb {M}, P, Q\in \mathbb {P}\cdot P\precsim Q\Rightarrow M |_{P}\precsim M |_{Q}$

Also, any $\kappa : \mathtt {inform}\langle P\rangle$ simulates $\kappa : 0$. Surprisingly the rule is easy, but not trivial, due to backward reductions.

Lemma 4

$\forall M\in \mathbb {M}, P, S\in \mathbb {P}\cdot M\ |\ \kappa : \mathtt {inform}\langle P\rangle |_{S} \precsim M\ |\ \kappa : 0 |_{S}$

Proof

We have to show that, for any $C$ such that $M\ |\ \kappa : 0 |_{S} \rightarrow C$, there exists $C^\prime$ such that $M\ |\ \kappa : \mathtt {inform}\langle P\rangle |_{S} \rightarrow C^\prime$.

We proceed by case analysis on the reduction rule used. Only G.Bw and G.Inform are not trivial.

• G.Bw: From the premisses of G.Bw and C.Bw, $M\ |\ \kappa : 0 \equiv \nu k.k : P\ |\ [Q; k]$. If $\kappa$ is independent of $k$, then the result trivially holds. If $\kappa = \langle h_i, \tilde{h}\rangle \cdot k$, then $M\ |\ \kappa : 0 \equiv M^\prime \ |\ (\nu k.\langle h_j, \tilde{h}\rangle \cdot k : R\ |\ \langle h_i, \tilde{h}\rangle \cdot k : 0)\ |\ [Q; k]\equiv M^\prime \ |\ (\nu k.k : R\ |\ 0)\ |\ [Q; k]$ (notice that it is possible that $\kappa = k$, in which case $R = 0$). Then the backward reduction that occurs is $M^\prime \ |\ (\nu k.k : R\ |\ 0)\ |\ [Q; k] |_{S}\rightsquigarrow M^\prime \ |\ Q |_{S}$. Finally, with the same reasoning, we have $M\ |\ \kappa : \mathtt {inform}\langle P\rangle \equiv M^\prime \ |\ (\nu k.k : R\ |\ \mathtt {inform}\langle P\rangle )\ |\ [Q; k]$, which can reduce using G.Bw: $M^\prime \ |\ (\nu k.k : R\ |\ \mathtt {inform}\langle P\rangle )\ |\ [Q; k] |_{S}\rightsquigarrow M^\prime \ |\ Q |_{S}$. The result holds by reflexivity of $\precsim$.

• G.Inform: We suppose the $\mathtt {inform}\langle \cdot \rangle$ that reduces is $k : \mathtt {inform}\langle P\rangle$. In the case it is an other $\mathtt {inform}\langle \cdot \rangle$ in $M$, the result trivially holds. From the premisses of G.Inform, $M\ |\ k : \mathtt {inform}\langle P\rangle |_{S}$ reduces to $M\ |\ \nu k^\prime .k^\prime : 0\ |\ [k : \mathtt {inform}\langle P\rangle ; k^\prime ] |_{P}$ and $P\precsim S$. We have to show that $M\ |\ \nu k^\prime .k^\prime : 0\ |\ [k : \mathtt {inform}\langle P\rangle ; k^\prime ] |_{P}\precsim M\ |\ k : 0 |_{S}$. Only the case G.Forecast is relevant. In that case, according to the premisses of G.Forecast and C.For, $M\equiv M^\prime \ |\ \kappa : \mathtt {forecast}(X) \triangleright Q$. Therefore, $M\ |\ \nu k^\prime .k^\prime : 0\ |\ [k : \mathtt {inform}\langle P\rangle ; k^\prime ] |_{P}$ reduces to $M^\prime \ |\ \nu k^{\prime \prime }.k^{\prime \prime } : Q\{^{P}/_{X}\}\ |\ [\mu ; \kappa ]\ |\ \nu k^\prime .k^\prime : 0\ |\ [k : \mathtt {inform}\langle P\rangle ; k^\prime ] |_{P}$ and, similarly, $M\ |\ k : 0 |_{S}$ reduces to $M^\prime \ |\ \nu k.k : Q\{^{S}/_{X}\}\ |\ [\mu ; \kappa ]\ |\ k : 0 |_{S}$. Since $P\precsim S$, $M^\prime \ |\ \nu k.k : Q\{^{P}/_{X}\}\ |\ [\mu ; \kappa ]\ |\ \nu k^\prime .k^\prime : 0\ |\ [k : \mathtt {inform}\langle P\rangle ; k^\prime ] |_{P} \precsim M^\prime \ |\ \nu k.k : Q\{^{S}/_{X}\}\ |\ [\mu ; \kappa ]\ |\ k : 0 |_{S}$.

Corollary 2

$\forall M\in \mathbb {M}, P,R, S\in \mathbb {P}\cdot R\precsim S\Rightarrow M\ |\ \kappa : \mathtt {inform}\langle P\rangle |_{R} \precsim M\ |\ \kappa : 0 |_{S}$

Proof

From Lemmas 3 and 4, $M\ |\ \kappa : \mathtt {inform}\langle P\rangle |_{R} \precsim M\ |\ \kappa : 0 |_{R} \precsim M\ |\ \kappa : 0 |_{S}$. The result holds by transitivity of $\precsim$.

5.2 Causal Consistency of the Traces Without G.Inform Reductions

When a $\varOmega \rho \pi$ trace $\sigma$ does not contain G.Inform reduction, there is a one-to-one mapping between the global semantics of $\varOmega \rho \pi$ contexts, and the configuration semantics of $\varOmega \rho \pi$ configurations. To clarify this paragraph, we will only work with the configuration fragment of $\varOmega \rho \pi$.

The configuration semantics is analogous to the regular $\rho \pi$ semantics, except for $\mathtt {inform}\langle P\rangle$ and $\mathtt {forecast}(X) \triangleright Q$ primitives. Encoding the $\mathtt {inform}\langle P\rangle$ primitive in $\rho \pi$ is easy: it acts like an oblivious channel and one just need to add a repeating $\mathtt {inform}(X)\triangleright 0$ process (and, anyway, since $\sigma$ does not contain G.Inform reduction, we could even ignore them).

Encoding the $\mathtt {forecast}(X) \triangleright Q$ primitive is almost as simple. Since the trace does not contain G.Inform reduction, the context is constant. Let $P$ be the process it contains. We only need to add enough $\mathtt {forecast}\langle P\rangle$. To avoid any problem with the key, we can simply add them under the same key than the forecast. That is, we replace each $\kappa : \mathtt {forecast}(X) \triangleright Q$, by $\kappa : \mathtt {forecast}(X) \triangleright Q\ |\ \mathtt {forecast}\langle P\rangle$. Note that this replacement also includes occurrences in memories.

Definition 4

The function $[[M |_{R} ]]_{=} [[M ]]_{R}$ encodes an $\varOmega \rho \pi$ context into a $\rho \pi$ configuration, where $[[M ]]_{R}$ is defined in Figs. 11 and 12.

Fig. 11.

Rules to encode an $\varOmega \rho \pi$ configuration into a $\rho \pi$ configuration.

Fig. 12.

Rules to encode an $\varOmega \rho \pi$ process into a $\rho \pi$ process.

Trivially, ignoring G.Inform transitions, an encoded $\varOmega \rho \pi$ configuration simulates the original configuration, and an $\varOmega \rho \pi$ configuration simulates the forward reductions of its encoded counterparts, using only forward rules:

Lemma 5

For any $\varOmega \rho \pi$ contexts $C_1$ and $C_2$, $[[C_1 ]]_{}\twoheadrightarrow [[C_2 ]]_{}\Rightarrow C_1\twoheadrightarrow C_2$. If $C_1\twoheadrightarrow C_2$ without a G.Inform reduction, then $[[C_1 ]]_{}\twoheadrightarrow [[C_2 ]]_{}$. If $C_1\rightsquigarrow C_2$, then $[[C_1 ]]_{}\rightsquigarrow [[C_2 ]]_{}$.

Corollary 3

$\varOmega \rho \pi$, without G.Inform reductions, is causally consistent.

Proof

Suppose $C_i\rightarrow ^\star C_f$, for . Then there exists a $\rho \pi$ reduction $[[C_i ]]_{}\rightarrow ^\star [[C_f ]]_{}$.

Since $\rho \pi$ is causally consistent, there exists a forward reduction $[[C_i ]]_{}\twoheadrightarrow ^\star [[C_f ]]_{}$. Therefore there exists a forward reduction $C_i\twoheadrightarrow ^\star C_f$.

5.3 Existence of a Trace Free of G.Inform Reductions

We are given an initial trace $\sigma = t_1; \dots ; t_n$ with $C_i$ the initial configuration. Our goal is to show that there exists a coinitial and cofinal trace $\sigma _f; \sigma _i$ such that $\sigma _f$ is free of G.Inform reductions. We proceed in two steps: (i) we consider a forecast sequence $\sigma ^\prime$ and we show that we can move the (initial) G.Inform reductions at the end of the trace (see Fig. 13); (ii) we consider an initial trace and we show that we can then move all G.Inform reductions at the end of the trace, by successively pushing the first G.Inform reductions toward the end of the trace.

Fig. 13.

Illustration of Lemma 6. If a configuration $M |_{P}$ reduces to $N |_{Q}$ using a G.Inform reduction, then the initial configuration simulates the final configuration.

Lemma 6 (Inform removal)

$\forall M\in \mathbb {M}\cdot M |_{P}\rightarrow N |_{Q}\Rightarrow M |_{P}\precsim N |_{Q}$

Proof

Since the transition changes the context, it is a G.Inform transition. Thus, $M = M^\prime \ |\ \kappa : \mathtt {inform}\langle P\rangle$ and $N = M^\prime \ |\ \kappa : 0$. From Lemma 4, we have that $M |_{P}\precsim N |_{P}$. From the premisses of rule G.Inform, $P\precsim Q$. From Lemma 3, we have that $M |_{P}\precsim M |_{Q}$. Finally, from the transitivity of the simulation relation, $M |_{P}\precsim N |_{Q}$.

A corollary of this lemma is that for any sequence of reductions from $C_i$ to $C_f$, it is possible to remove all G.Inform reductions and reach a new $C_f^\prime$ which can simulate $C_f$.

Corollary 4

For all initial configuration $C_i$, for all configuration $C_f$ such that $C_i\rightarrow ^\star C_f$, there exists a configuration $C_f^\prime$ such that $C_i\rightarrow ^\star C_f^\prime$ without G.Inform reduction and $C_f^\prime \precsim C_f$.

Proof

Let $\sigma = t_1; \dots ; t_n$ be the trace of the sequence of reduction $C_i\rightarrow ^\star C_f$.

By induction on the number of G.Inform reductions in $\sigma$. The base case ($0$ G.Inform reduction in $\sigma$) follows from the previous section.

For the inductive case, consider there are $n$ G.Inform reductions in $\sigma$, let $t_j = C_{j-1}\twoheadrightarrow C_j$ be the first one and $t_k = C_{k-1}\twoheadrightarrow C_k$ the second one. That is, $C_j\rightarrow ^\star C_{k-1}$ without G.Inform reduction.

From Lemma 6, $C_{j-1}\precsim C_j$, there exists a $C_{k-1}^\prime$ such that $C_{j-1}\rightarrow ^\star C_{k-1}^\prime$ and $C_{k-1}^\prime \precsim C_{k-1}$. Let $\sigma _1$ be the trace of that sequence of reductions. From Remark 1, $\sigma _s$ does not contain G.Inform reduction.

Also, since $C_{k-1}^\prime \precsim C_{k-1}$, there exists a $C_f^\prime$ such that $C_{k-1}\rightarrow ^\star C_f^\prime$ and $C_f^\prime \precsim C_f$.

Finally, we have $C_i \rightarrow ^\star C_{k-1}^\prime \rightarrow ^\star C_f^\prime$. This sequence contains one less G.Inform reduction. Thus, from the induction hypothesis, there exists $C_f^{\prime \prime }$ such that $C_i\rightarrow ^\star C_f^{\prime \prime }$ without G.Inform reduction and such that $C_f^{\prime \prime }\precsim C_f^\prime$.

Finally, from the transitivity of simulation, $C_f^{\prime \prime }\precsim C_f$.

6 Application: Sieve of Eratosthenes

Presentation. In this section, we informally discuss an example application of the oracle introduced in $\varOmega \rho \pi$. This example consists in a distributed implementation of the Sieve of Eratosthenes algorithm to find prime numbers. Despite being quite simple, it shows that partial reversibility of $\varOmega \rho \pi$ allows a notion of forward progress, which is not the case in pure causally consistent reversible calculi.

For this example, for the sake of simplicity, we add integers, sets and tuples as primitive values of our calculus, and we assume we have usual primitive functions to manipulate those values.

The Sieve of Eratosthenes is a simple algorithm to find prime numbers under a limit $l$. This algorithm begins with a set of integers from $2$ to $l$, and iterate over each integers $i$ in the set, removing multiples of $i$. When a fixpoint is reached, the set contains all prime numbers below $l$.

In our example, we adapt this algorithm for a distributed setting: instead of iterating over $i$, we take a second set of integer between $2$ and $\lceil \sqrt{l}\rceil$, from which concurrent processes select a local $i$.

For our example, the oracle contains a tuple of two sets: the first is the set of prime candidates, which we call the sieve and the second is the set of possible values for $i$ (which we call values). Each thread reads this oracle, selects a possible $i$ and removes its multiples from the sieve. Figure 14 shows an implementation of this distributed variant of the Sieve of Eratosthenes. For the sake of conciseness, we only show a single process, but one could choose an arbitrary number of similar processes. Initially, the oracle contains the two sets $\{2, \dots , l\}$ and $\{2, \dots \lceil \sqrt{l}\rceil \}$. Notice that, once a possible $i$ is tested, it is removed from the set of possible values.

Fig. 14.

A distributed implementation of the Sieve of Eratosthenes. This implementation has only one process, with tag $k_1$, but it could contain an arbitrary number of similar processes.

Discussion. The term we show in Fig. 14 is safe, in the sense that when we reach a configuration in which the oracle is $\langle sieve, \emptyset \rangle$, we know that $sieve$ contains only prime numbers. However, there is no guarantee that this state is eventually reached. First, as with regular reversible calculi, we can loop in a forward/backward reduction for ever (if the oracle is not updated in between, there is no progress). We ignore this problem since it is common in reversible calculi.

However, the primitives we introduced with the oracle introduce a new problem, which is that forecasts and informs are not atomic: if two receptions are done concurrently, there is a possibility to have a read–modify–write inconsistency. The second issue is deeper. To solve it, we would have to introduce standard atomic primitives, such as compare-and-swap, to interact with the oracle.

Nonetheless, even with this drawback, this example is interesting. It shows that we have a notion of progress, which can be used to implement standard algorithms for concurrent programming.

7 Conclusion and Future Work

We presented $\varOmega \rho \pi$, a reversible calculus in which process can be stored in an oracle, which is preserved during backward reductions. This oracle is controlled by two primitives which act as two channels $\mathtt {inform}$ and $\mathtt {forecast}$. Until a process is set, any process can be received from the $\mathtt {forecast}$ primitive (it acts as a random process). Once a process $P$ is sent to the $\mathtt {inform}$ channel, any message received from the $\mathtt {forecast}$ channel is that process $P$ (until a new process $Q$ is sent to $\mathtt {inform}$) even if the configuration does backward reductions.

Our second main contribution is the definition of a notion of weak causal consistency. Weak causal consistency states that for any reachable state, there must exists a similar state reachable using only forward reductions. We think that, in addition to the calculus presented here, this notion of weak causal consistency may be suitable to study other reversible process calculi, for instance those in which backward reductions introduce some garbage which should be ignored.

Future work could improve this paper on two directions.

First, our work can be extended by allowing the process stored in the context to reduce as any other process, following standard $\mathtt{HO}\pi$ semantics. Thus, terms would have two parts: a reversible part (in the configuration) and a non-reversible side (in the context). Our $\mathtt {forecast}$ and $\mathtt {inform}$ primitives would allow processes to cross the boundary between the two sides. On a longer term, we could imagine allowing reversible and non-reversible processes to communicate via standard channels (and removing $\mathtt {forecast}$ and $\mathtt {inform}$ channel, which would become useless). Such approach would result in a reversibility confined to some processes, in a globally non-reversible process (or vice-versa).

On the other hand, we could try to relax the simulation constraint in the premisses of rule G.Inform, which is an important practical limitation. Instead of having a simulation constraint, we could allow a relation $\mathcal {R}$, given as a parameter of the semantics. With sufficient constraints on this relation (typically reflexivity, transitivity and evaluation closure), we could try to prove the weak causal consistency property of $\varOmega \rho \pi$ with respect to such $\mathcal {R}$.

Finally, an underlying aspect of this work is to introduce some notion of progress in the context of reversible computation. Usually, reversible computation loses this notion by the very nature of the computation: there is an initial configuration, but no final one, as it is always possible to take backward and forward steps; nor any notion of progress, as anything that is done can be undone. Using oracles and contexts as presented in this paper can be used to reintroduce a notion of progress, for instance by having a convergence criterion on the context.