Ivan Lanese
email: ivan.lanese@gmail.com

Doriana Medić
email: doriana.medic@gmail.com

A General Approach to Derive Uncontrolled Reversible Semantics (TR)

Keywords: 2012 ACM Subject Classification Theory of computation → Concurrency; Computing methodologies → Concurrent computing methodologies Reversible computing, causality, process calculi, Erlang

Reversible computing is a paradigm where programs can execute backward as well as in the usual forward direction. Reversible computing is attracting interest due to its applications in areas as different as biochemical modelling, simulation, robotics and debugging, among others. In concurrent systems the main notion of reversible computing is called causal-consistent reversibility, and it allows one to undo an action if and only if its consequences, if any, have already been undone.

This paper presents a general and automatic technique to define a causal-consistent reversible extension for given forward models. We support models defined using a reduction semantics in a specific format and consider a causality relation based on resources consumed and produced. The considered format is general enough to fit many formalisms studied in the literature on causalconsistent reversibility, notably Higher-Order π-calculus and Core Erlang, an intermediate language in the Erlang compilation. Reversible extensions of these models in the literature are ad hoc, while we build them using the same general technique. This also allows us to show in a uniform way that a number of relevant properties, causal-consistency in particular, hold in the reversible extensions we build. Our technique also allows us to go beyond the reversible models in the literature: we cover a larger fragment of Core Erlang, including remote error handling based on links, which has never been considered in the reversibility literature.

Introduction

Reversible computing considers systems that can compute backward, recovering past states, as well as forward. The studies on reversible computing gained in popularity in the 60's, thanks to the observation that only irreversible actions need to produce heat [21]. Beyond obtaining computing machinery with low heat dissipation, reversible computing found its application in a wide range of fields, from biochemical modelling [6,12,19,[START_REF][END_REF] to simulation [8], robotics [33], programming [34,[START_REF] Danos | Reversible communicating systems[END_REF]28] and program debugging [5,[START_REF] Lanese | A theory of reversibility for Erlang[END_REF]35,27]. The main objective of the theoretical computer science community in this research area has been to provide a foundational understanding of reversibility. Nowadays, in the literature, there is a number of formalisms describing different approaches to reversibility with the purpose to better understand its properties and characteristics, e.g. reversible computation in process algebras [10,41,25], Petri Nets [39,36], event structures [46], logic circuits [14], etc.

In a sequential system, backward computation is obtained by undoing forward actions in reverse order of execution, starting from the last one. Undoing a forward action can be seen as a backward action. In a concurrent setting, where many processes are running at the same time, identifying the last action is not an easy task, and may sometimes be impossible. Therefore, alternative approaches have been considered. Here we consider the causal-consistent approach [10,41,26], which focuses on the causality relations between actions to decide which actions can be undone. Consequently, while designing a reversible model following the causal-consistent approach, one needs to take care of storing information on the past of the system, to be able to recover past states, but also causality information, to know which forward steps can be undone at a given moment. In order to show that a reversible model follows the causal-consistent approach, a number of properties need to be proved [10]. The most relevant are the Loop Lemma, showing that each action can be undone, the Square Lemma, showing that the chosen notion of causality is compatible with the semantics, and Causal Consistency, showing that the correct information is stored. More recently [31], Causal Safety and Causal Liveness have also been proposed, stating that an action can be undone if and only if its consequences, if any, are undone beforehand.

The aim of this paper is to explore how to mechanically obtain a causal-consistent reversible extension of a given forward-only model. This is in sharp contrast with most of the reversible models in the concurrency literature, which have been defined manually. An advantage of building the reversible model in this way is that the properties mentioned before are satisfied by construction. The only other work we are aware of providing an automatic technique is [41], which considers process calculi defined in a specific SOS format [42]. Differently from [41], we focus on forward systems defined using a reduction semantics (Section 2.1). While this is more limited since it does not consider open systems, our approach can deal with systems that do not fit the model in [41]. This is the case for both our case studies, namely higher-order π [43] and Core Erlang [START_REF] Boothe | Efficient algorithms for bidirectional debugging[END_REF].

Given a forward-only system, we aim at building its uncontrolled [26] causal-consistent reversible extension. Here with uncontrolled we mean that at any moment both forward actions and backward actions are possible, and there is no policy on which action to prefer. Uncontrolled semantics is the basis for a reversible model, on top of which control policies selecting the actions to be done or undone can be added [11,23,2,24].

Our approach works in two main steps. First, we attach a unique identifier, called key, to every entity (process, messages, etc.) of the forward system, and then we enrich the model with memories, where past information is stored (Section 2.2). After defining our method, we show that the reversible models built using it satisfy the properties of causal-consistent reversible models discussed above (Section 3). We prove them using a novel approach [31], which consists in showing that the system satisfies a few basic axioms.

Example 1. The classical syntax of is as follows:

P, Q ::= a P | a(X) P | (P | Q) | νa (P ) | X | 0
Process variables are represented with X and channel names with a, b, c. Process a P sends message P over channel a while a(X) P denotes a process which receives a message on channel a and replaces it for X inside P . There is no continuation after output since the calculus is asynchronous. We denote parallel composition with P | Q and its neutral element with 0. Restriction of name a inside P is written νa (P ). The binders are νa (P ) and a(X) P , where the scope of name a and variable X is process P . We denote the set of free names of process P with fn(P ).

In order to fit our framework we need to separate entities from systems. In this case, an entity is any HOπ process whose topmost operator is neither a parallel composition nor a restriction nor 0. The syntax of systems is thus as follows

N := P | (N 1 | N 2 ) | νa (N ) | 0
where parallel composition and 0 are the operators required by our framework and restriction is an infinite family of unary operators with one instance for each name a.

Thanks to the syntax above, a generic system can be represented as a term T [P 1 , . . . , P n ], where T [• 1 , . . . , • n ] is a context with n numbered holes built from composition operators, possibly including parallel composition, and 0. The term T [P 1 , . . . , P n ] is obtained by replacing • i with P i for each i ∈ {1, . . . , n}.

We complement our syntax with a structural congruence, specified by axioms of the form T [P 1 , . . . , P n ] ≡ T [P 1 , . . . , P n ] and closed under contexts, reflexivity, symmetry and transitivity. As can be seen from the rule format, structural congruence cannot change the number of entities in a term. Also, it is understood that P i and P i refer to the same entity, which can however evolve while preserving its identity. This assumption will become clearer later on, when we introduce keys (to track the identity) and the causality relation. We assume structural rules ensuring that parallel composition is associative, commutative, and has 0 as neutral element.

We illustrate below that the structural congruence of HOπ satisfies the requirements.

Example 2. Sample HOπ structural rules are as follows, the full structural congruence is in Appendix A.1.

(Alpha) νa P ≡ νb P {b/a} if b / ∈ fn(P ) (ParC) P | Q ≡ Q | P (ResF) (νa P ) | Q ≡ νa (P | Q) if a / ∈ fn(Q) Rule (Alpha) is α-conversion. Rule (Alpha)
is seen in our framework as an infinite family of rules (and the same for rule (ResF) for scope extrusion), for each a, P and b satisfying the side condition. Hence, no side condition is needed in the instance. Note that P on the left-hand side and P {b/a} on the right-hand side are understood to be the same entity. Rule (ParC) establishes commutativity of parallel composition as required. It exploits contexts of the form

• 1 | • 2 and • 2 | • 1 .
The reduction semantics of the forward model needs to have the format described in Figure 1, which includes two rules ((Par) and (Eqv)), which need to belong to the semantics, and two schemas ((Scm-Act) and (Scm-Opn)). The semantics can contain any number of instances of the schemas (possibly an infinite number), obtained by replacing all placeholders with terms of the corresponding category (e.g., P 1 with an entity, T with a context, and so on). One may notice that rule (Par) is an instance of schema (Scm-Opn): this means that such an instance is required. Anyway, being an instance, we do not need to deal with it explicitly in the following.

Rule schema (Scm-Act) allows one to specify interactions between entities. It is understood that such an interaction consumes the entities P 1 , . . . , P n and produces the entities Q 1 , . . . , Q m . This intuition will be captured by keys and the causality relation. The created entities are composed in a term

T [Q 1 , . . . , Q m ],
where T is a context built from composition operators. Rules in this schema, together with rule (Par), allowing a system to execute inside a parallel composition, define the behaviour of parallel composition. The behaviour of other operators is described by rule schema (Scm-Opn). Notably, this schema allows a single entity to execute at each step. Rule (Eqv) allows one to exploit structural congruence.

We see below how the rule for communication of HOπ fits the format given in Figure 1. The full semantics of HOπ and the explanation of how it fits the format is in Appendix A.1.

Example 3. The communication rule (Act) of HOπ, where process Q is received and bound to variable X, is defined as:

(Act) a Q | a(X) P P {Q/X}
Rule (Act) can be seen as an infinite family of rules fitting schema (Scm-Act). Notice that the number of entities in the resulting process may vary, e.g., in:

a νb (b P | b(Y ) Y | c Q ) | a(X) X νb (b P | b(Y ) Y | c Q )
the resulting process has three entities b P , b(Y ) Y and c Q , composed using a context

T = νb (• 1 | • 2 | • 3 ).
Example 4. The CCS reduction a.P + Q|!a.R CCS P |!a.R|R, where the output a synchronises with the replicated input !a and Q is discarded, can be seen as an instance of schema (Scm-Act) as well. Indeed, the two parallel entities a.P + Q and !a.R interact to produce the three entities P , !a.R and R on the right-hand side (assuming P and R to be single entities).

Definition of the Reversible System

In order to define the causal-consistent reversible extension of a given system, one first needs to extend the forward semantics so to keep track of past states. This information will be used by the backward semantics. In particular, we use unique keys to distinguish identical entities which have different history, and memories to recall parts of the system which have been changed by a computational step. More in detail, each entity of a system is labelled with its unique key. Also, each step of the system produces a memory allowing one to undo it. We refer to systems extended with keys and memories as configurations.

Definition 5. The syntax of configurations R is defined by the following grammar:

R ::= k : P | op n (R 1 , . . . , R n ) | 0 | [R ; C] C ::= T [k 1 : • 1 , . . . , k m : • m ]
where operators op n are the same as in the forward system and T is a context composed of operators op n and 0. Also, • i are numbered holes, to be filled by the processes with keys k i .

Intuitively, a memory µ = [R ; C] is composed of the configuration R which gave rise to the forward step and the context C of the configuration resulting from it.

Example 6. The syntax of the reversible HOπ-calculus is defined as:

R ::= k : P | (R 1 | R 2 ) | νa (R) | 0 | [R ; C]
where entities P are as in the underlying calculus and a unique key k is attached to each of them. Note that now parallel composition and restriction operators are applied to configurations. Finally, memories are also part of the syntax.

We now define the structural congruence and the forward and backward operational semantics for the reversible system. As in the original model, we can represent a reversible system as T [k 1 : P 1 , . . . , k n : P n ], where T is a context built from operators op n and 0. The main difference w.r.t. the original calculus is that now each entity is labelled with its key. We have one structural rule for each structural rule of the original semantics, with the same context T , but now entities are labelled with keys, and keys on both sides are the same.

T [k 1 : P 1 , . . . , k n : P n ] ≡ T [k 1 : P 1 , . . . , k n : P n ]
We define below the function key(•) that computes the set of keys in a configuration R:

(F-Scm-Act) P1 | . . . | Pn T [Q1, . . . ,
(F-Scm-Opn) R i R i (key(R i ) \ key(R i )) ∩ (key(R0, . . . , R i-1 , R i+1 , . . . , Rn) = ∅ opn(R0, . . . , R i , . . . , Rn) opn(R0, . . . , R i , . . . , Rn) (F-Eqv) R ≡ R R R1 R1 ≡ R 1 R R 1 Figure 2 Forward
(B-Eqv) R ≡ R R R1 R1 ≡ R 1 R R 1
Figure 3 Backward rules of the uncontrolled reversible semantics Definition 7. The set of keys of a configuration R, written as key(R), is defined as:

key(k : P ) = {k} key(op n (R 1 , . . . , R n )) = key(R 1 ) ∪ . . . ∪ key(R n ) key(0) = ∅ key([R ; C]) = key(R) ∪ key(C)
The forward rules of the uncontrolled reversible semantics are in Figure 2. For schemas (F-Scm-Act) and (F-Scm-Opn) we have one instance for each instance of the corresponding schema in the original semantics. For schema (F-Scm-Act) the main difference w.r.t. the original schema is that entities are labelled with keys and a memory stores information on the performed step. More precisely, entities Q 1 , . . . Q m on the right-hand side have fresh keys j 1 , . . . , j m . Also, the left configuration R = k 1 :

P 1 | . . . | k n : P n is saved in a memory µ = [R; C] together with the context C = T [j 1 : • 1 , . . . , j m : • m ]
of the resulting configuration. In this way, the structure of the obtained system and the newly generated keys are recorded. They will be needed to perform the corresponding backward step. As far as the schema (F-Scm-Opn) is concerned, the only novelty is the side condition ensuring that keys introduced during the step are fresh for the whole system. The structural congruence rule (F-Eqv) is the same as in the original semantics (but structural congruence preserves keys).

The backward rules, depicted in Figure 3, are symmetric w.r.t. the forward ones. With rule schema (B-Scm-Act) the forward action that produced term T [j 1 : Q 1 , . . . , j m : Q m ] is undone. The past state of the system k 1 : P 1 | . . . | k n : P n is restored from the memory µ. The context C = T [j 1 : • 1 , . . . , j m : • m ] inside µ additionally ensures that all entities produced by the forward action, together with the term composing them, are available in the configuration and are consumed by the backward step.

Properties

In this section, we show that the reversible semantics defined using the approach in the previous section satisfies a number of properties expected from a causal-consistent reversible semantics. In particular, the reversible semantics is a conservative extension of the forward semantics, and it is causally consistent [10].

Since our syntax allows for a number of ill-formed terms, as commonly done, in the following we restrict the attention to reachable configurations, defined below.

Definition 10 (Initial and reachable configuration). A configuration R is initial if it does not contain memories and all keys are distinct. A configuration R is reachable if it can be derived from an initial configuration by applying the rules in Figures 2 and3.

Correspondence between reversible and original semantics

In this section we prove that the forward reversible semantics is a conservative extension of the original semantics. To this end, we first define the erasing function ϕ that given a configuration R, by deleting histories and keys, generates a forward-only system N .

Definition 11 (Erasing function). The function ϕ : R -→ N , where R and N denote respectively the sets of configurations and of original systems, is inductively defined as follows:

ϕ(k : P ) = P ϕ([R ; C]) = 0 ϕ(0) = 0 ϕ(op n (R 1 , . . . , R n )) = op n (ϕ(R 1 ), . . . , ϕ(R n ))
Now, we can show that the forward semantics of a configuration R and the semantics of its projection on the forward system ϕ(R) are strong bisimilar (Definition 28 in Appendix A.2).

Theorem 12. For each configuration R, its forward semantics and the semantics of ϕ(R) are strong bisimilar.

Concurrency and Causal Consistency

In order to prove that the defined reversible semantics is indeed causal-consistent we need to define a causality relation on our systems. We define it directly on reversible systems, for two reasons. First, keys and memories help in this respect. Second, in a reversible system the concurrency relation induces a causality relation (see [29,Def. 11 and Lemma 6]).

We extend the reduction semantics to a notion of transitions, which carry in the label information on the used resources, in form of the memory involved in the transition. Formally, we define transitions t of a system R as t : R µ -→ R , where µ is the memory created by the transition, if it is forward, or consumed by it, if it is backward. There, R is the source while R is the target of the transitions t. Two transitions are coinitial (resp. cofinal) if they have the same source (resp. target), and composable if the target of the former is the source of the latter. A derivation d from the source R to the target R , written as d : R -→ * R , is a sequence of composable transitions. A zero steps derivation is written .

The concurrency relation between transitions states that two coinitial transitions are concurrent if they do not share entities. Formally:

Definition 13 (Concurrent transitions). Two coinitial transitions t : R µ -→ R and t : R µ --→ R are concurrent, written t c t , if key(µ ) ∩ key(µ ) = ∅. Coinitial transitions which are not concurrent are in conflict.
Notably, our notion of concurrency is extracted from the operational semantics (via its extension with keys and memories), hence it can be obtained also for those models where no notion of concurrency exists in the literature, like most mainstream programming languages.

Having fixed a notion of concurrency, we can proceed to show the Causal Consistency of the reversible semantics. To prove it, we use the recent axiomatic approach given in [31], which allows one to show a number of properties relevant for reversible calculi, such as the Parabolic Lemma (PL) and Causal Consistency (CC), by just proving a few basic axioms. The advantage is that proving the axioms is simpler than proving the results directly. Moreover, [31] introduces two new properties: Causal Safety (CS) stating that an action cannot be reversed until all actions caused by it have been reversed; and Causal Liveness (CL) saying that actions do not necessarily need to be reversed in the exact inverse order of the forward execution, but can be reversed in any order consistent with CS.

In the following we give the axioms and auxiliary definitions required by the framework of [31] necessary to show Causal Consistency, Safety and Liveness.

First, we re-formulate our framework as a Labelled Transition System with Independence (LTSI, see also [44]) (R, L, -→, ι), where R is a set of systems, L is the set of action labels, -→ ⊂ R × L × R is a transition relation and ι is the independence relation, namely an irreflexive symmetric binary relation on transitions. In our case, R is the set of configurations and L the set of labels of our transitions. The latter include both forward and backward transitions. Also, the notion of independence is defined on coinitial transitions and it coincides with the notion of concurrency, namely ι = c . A key property required by the framework in [31] is that each action is reversible, as shown by the following result.

Lemma 14 (Loop Lemma). For every reachable configuration R and forward transition t : R µ R , there exists a backward transition t • : R µ R and vice versa.

From now on we denote with t • the reverse of t. The basic properties required to show causal consistency are as follows. SP states that independent transitions can be executed in any order. We follow the standard notation and write t 2 /t 1 for the residual of t 2 after t 1 . Coinitial backward transitions are always independent by BTI. WF ensures that each system has a finite past.

To state Causal Consistency, we first define Causal Equivalence [10], an equivalence relation between derivations which stipulates that independent transitions can be swapped while pairs of reverse transitions can be removed from the derivation. The definition is well-posed if the LTSI satisfies the Square Property.

Definition 16 (Causal equivalence). Causal equivalence, ∼, is the least equivalence relation between derivations closed under composition satisfying

t 1 ; t 2 /t 1 ∼ t 2 ; t 1 /t 2 t; t • ∼
We now define two properties needed for Causal Safety and Causal Liveness, namely Coinitial propagation of independence (CPI) and Coinitial independence respects events (CIRE).

Definition 17 (Coinitial propagation of independence (CPI)). If whenever t

1 : R µ1 -→ R , t 2 : R µ2 -→ R , t 2 : R µ2 -→ R and t 1 : R µ1 -→ R with t 1 c t 2 , then we have t 2 c t •
1 . We introduce the notion of event, needed to state (CIRE), and define independence (concurrency in our case) on them.

Definition 18 (Events). Let (R, L, -→, c ) be a LTSI satisfying SP,BTI,WF and CPI. Let ≈ be the smallest equivalence relation satisfying

: if t 1 : R µ1 -→ R , t 2 : R µ2 -→ R , t 2 : R µ2 -→ R and t 1 : R µ1 -→ R and t 1 c t 2 , then t 1 ≈ t 1 . The equivalence classes of forward transitions R µ R , written [R, µ, R ], are the events. The equivalence classes of reverse transitions R µ R , [R, µ • , R ], are the reverse events. A labelling function l from - → / ≈ to L is defined by settings l([R, µ, R ]) = l([R, µ • , R ]) = µ. Events e 1 ,
-→ R ρ -→ * R . Transition R µ -→ R can be undone in R , that is there is a transition R 1 µ -→ R with (R, µ, R ) ≈ (R 1 , µ, R ), if (CL) and only if (CS) R µ -→ R is concurrent to all transitions R ρ -→ * R which are not undone in R ρ -→ * R .

Case Studies

In this section we apply our approach to two relevant case studies from the literature, the Higher-Order π-calculus [43] and Core Erlang [START_REF] Boothe | Efficient algorithms for bidirectional debugging[END_REF]. Causal-consistent reversible semantics for both of them are available in the literature [25,28]. We show that the ones derived using our approach, albeit syntactically different, are equivalent to the ones in the literature.

In the case of Core Erlang we go beyond the literature, which covers only the functional and concurrent fragment of Core Erlang, showing how to deal also with constructs for error handling based on links.

Reversible Semantics for Higher-Order π-calculus

In the previous sections, we already shown how to apply our approach to the Higher-Order π-calculus. We show here that the semantics derived using our approach is equivalent to the one of ρπ, the reversible HOπ in the literature [25]. Additionally, it is easy to see that the notion of concurrency induced by our approach (Definition 13) on HOπ matches the definition of concurrent transitions of [25, Definition 9]. Our reversible HOπ and the one in the literature are indeed quite close, but for a few differences. Our approach stores a context for the resulting term, in ρπ only a key is kept. Actually, the context is always composed by parallel operators and restriction operators. The former are always collected during ρπ backward steps, the latter are instead removed by ρπ structural congruence when no more needed. Also, in ρπ restrictions for keys are explicit, in our approach they are implicit. In addition, the single key kept in ρπ is split into multiple complex tags, in direct correspondence with our keys, by ρπ structural congruence, hence in ρπ one key is enough.

For instance, starting from the system R = k 1 : a P 1 | P 2 | k 2 : a(X) X, in our reversible HOπ semantics, by applying rule (F-Act), we have:

k 1 : a P 1 | P 2 | k 2 : a(X) X j 1 : P 1 | j 2 : P 2 | [R ; j 1 : • 1 | j 2 : • 2 ]
In ρπ, by applying rule (R.Fw) followed by structural congruence [25], we have:

R νk .k(P 1 | P 2 ) | [R ; k] ≡ νk, j .( j 1 , j • k : P 1 | j 2 , j • k : P 2 ) | [R ; k]
Structural congruence splits key k referring to the whole continuation into complex tags j i , j • k, where j = {j 1 , j 2 } and i ∈ {1, 2}. By using structural congruence, complex tags for single entities can be always generated, as in our example above. Despite the differences, our reversible HOπ semantics and ρπ semantics [25] are equivalent. To show this, we exploit the encoding function • : R -→ M which translates a reversible HOπ configuration into a ρπ configuration. Function • needs to extract the set of keys of all entities obtained by the split from the memory of our HOπ system and to construct the complex tags of ρπ configuration. The encoding function together with other technical details can be found in Appendix A.3. Using the encoding function above we can show a bijective correspondence between transitions in our approach and ρπ transitions.

Theorem 24. Let R be a reachable configuration of reversible HOπ with R = M . There is a transition R -→ R in reversible HOπ iff there is a ρπ transition M -→ M with R ≡ M .

Reversible Semantics for Erlang

In this section we apply our approach to Core Erlang [START_REF] Boothe | Efficient algorithms for bidirectional debugging[END_REF], an intermediate step in the compilation of the concurrent and functional language Erlang. We also show the equivalence between the obtained reversible semantics and the one in [29]. As a forward model, we use the logging semantics of Core Erlang [29, Figure 14] (used also in [30]) with some minor changes: we use floating messages, as in [32], instead of a global mailbox Γ and we omit the labels of the relation →. Indeed, labels are used in [29] to log the steps of the computation so to be able to replay it from logs [30,29]. In our work, we are not interested in replaying from logs, therefore we do not need this information. The semantics of Core Erlang is defined in a modular way as in [29], with relation -→ modelling the evaluation of expressions and relation → representing reductions of systems. Due to space constraints, we only present the application of our approach to selected rules of the evaluation of systems -→, referring to the Appendix A.4 for the others. Since evaluation of expressions is not central for us, we refer to [29] for their description.

A Core Erlang system E is defined as a pool of processes and floating messages:

E := p, θ, e | (p, p , v) | (E 1 | E 2 )
where p, θ, e represents a process evaluating expression e in environment θ and uniquely identified by a pid (process identifier) p; (p, p , v) stands for a floating message carrying value v sent by the process with pid p to the one with pid p . A floating message is a message in the system after it is sent and before it is received.

We show below rules (Send) and (Rec) of Core Erlang semantics, the full semantics is in Figure 7 of Appendix A.4. Roughly speaking, rule (Send) states that if the evaluation of the expression e in the premise requires as a side effect to send value v to process p , the process evolves accordingly and a corresponding message is added to the system. Dually, rule (Rec) receives a message if the expression e requires a message matching some clauses cl n and the message at hand indeed matches one of the clauses (second premise). Now, we can apply our approach to the Core Erlang semantics and derive a reversible semantics for it. A reversible Core Erlang configuration, denoted with R, is defined as usual by adding keys and memories to an Erlang systems, as formalised by the following grammar:

R ::= k : p, θ, e | k : (p, p , v) | (R 1 | R 2 ) | [R; C]
In the following, we give the forward rules (F-Send) and (F-Rec) of the reversible semantics for Erlang. The complete set of forward rules is given in Figure 8 Actually, both rules are to be interpreted as schemas, so that premises related to the semantics of expressions and to match are used to select the allowed instances and do not occur in actual instances. E.g., an allowed instance for (F-Send) is: where ! is Erlang operator for sending. Below, we give the backward rules (B-Send) and (B-Rec) of the reversible semantics for Erlang. The complete set of backward rules is given in Figure 9 of Appendix A.4. When the action is undone, the prior state of the process is restored from the memory µ. The reversible semantics obtained by applying our approach to Core Erlang is not exactly the same as the one of [29]. There are two important differences. First, we are not using execution logs, that we removed from the semantics we gave in input to our approach, since we do not need them. Another difference is in how the past information of the system is stored. In [29], a history element h is kept as part of the process p, h, θ, e . It contains information to recover all past states of the process. In our reversible semantics, each step generates a memory with the information needed to reverse it, and the memories are connected using keys. Also, memories are not inside processes but floating in the configuration.

In the following, we prove that, despite the differences above, the two semantics capture the same behaviours. To this end, we first show that the two semantics are based on the same notion of causality (by showing that conflicting transitions are the same) and then that they are strong back and forth barbed equivalent [25]. Here we just discuss the idea, we refer to Appendix A.5 for the technical details.

The notion of conflict for reversible Core Erlang in [29, Definition 12] (which is an instance of the happened-before relation [20] as discussed in [29]) is defined in general terms, referring to which actions (e.g., send, . . . ) are performed and by which processes. Hence, it is also applicable to our reversible Core Erlang. We show below that it coincides with the definition we gave, based on keys and memories.

Theorem 25 (Causal correspondence). Two coinitial transitions t 1 and t 2 of our reversible Core Erlang semantics are in conflict according to [29,Definition 12] iff they are in conflict according to Definition 13.

We show below that the reversible semantics of Erlang in [29] and ours are strong back and forth barbed equivalent [25]. We let E to stand for a Core Erlang system, L for a reversible Erlang system as in [29] and R for one of our reversible Erlang configurations.

Following [32], we write E ↓ p if the system E contains a floating message targeting a process with pid p (i.e., if (p , p, v) | E ≡ E for some p , v and E ). We use the same notation for systems L and configurations R, writing L ↓ p and R ↓ p.

We now adapt the definition of back and forth barbed bisimulation [25] to reversible Erlang. In words, two reversible semantics are back and forth barbed bisimilar if they have the same barbs and they can match each other execution steps. Formally:

Definition 26. Relation R is a strong back and forth barbed simulation if (L, R) ∈ R implies: L ↓ p implies R ↓ p L L implies R R with (L , R ) ∈ R L L implies R R with (L , R ) ∈ R Relation R

Reversible Link Semantics for Erlang

Here, we apply our approach to the remote error handling mechanism of Core Erlang, based on links. No reversible semantics for it exists in the literature as far as we know. Defining it correctly does not present specific technical challenges, but it requires care, hence its definition is an interesting result on its own.

We start by giving some general idea about links and their role in Erlang (see [15] for more details). A link can be seen as a bidirectional path between two processes along which error signals travel. This can be used, e.g., to signal normal or abnormal termination. A process terminates normally when its code is completely executed, or it can terminate abnormally with a "reason", meaning that some faulty behaviour occurred during the execution. In both the cases, the process signals its termination to linked processes. This gives to the receiver the role of a controller in charge of handling the termination. There are two possibilities, depending on the nature of the receiver process: it can terminate too, or, if it is a system process, it can trap the termination signal and "resolve" the faulty behaviour. For instance, it could ignore it and continue with its execution, or start a copy of the terminated process, etc. Thanks to this feature, Erlang is particularly suited to build fault-tolerant systems [1].

In Erlang, links between two processes can be created by calling either function link(), linking any two processes (provided they are not terminated yet) or function spawn_link(), which spawns a new process and links it with the parent process atomically. In this work, we concentrate on function spawn_link(). Function link() can be dealt with similarly.

We start from the Core Erlang semantics discussed in the previous section and extend it to support the functions spawn_link() and process_flag(). The latter allows one to set the state of a process to system process, i.e. a process which will trap the error signal, or nonsystem process. More precisely, we add to Core Erlang syntax (see [29, Section 2.1, Figure 1]) expressions spawn_link(expr, [expr 1 , . . . , expr 1 ]) and process_flag(expr 1 , expr 2 ). In our case, function process_flag() is always called as process_flag(trap_exit, f lag), where the process becomes a system process if flag = true, a non-system process otherwise.

We show now a sample Erlang program to clarify the error handling mechanism described above. It calculates the sum of a given list of elements and returns invalid if the list contains some non-numeric element.

The execution starts by calling function total(), which first sets the process flag to true. In this way, the process will be able to trap termination signals from any process linked with it. The execution proceeds by calling function spawn_link(), which atomically spawns and links a new process, executing function sumProcess(), in charge of calculating the sum via auxiliary function sum(). Because of the link, when the linked process terminates, its parent process will receive an exit notification message.

Finally, function receiveValue() is invoked. It checks whether the computation finished without misbehaviours: if this is the case message { EXIT , P id, normal} is received and the function will read the result of the computation. To integrate the functions spawn_link() and process_flag(), we add to processes two pieces of information, the set of links l and the flag f . The link set l is updated when a link is created, adding the pid of the other process, or destroyed, removing it. The flag f is a Boolean, tracking whether a process is a system process or not. Also, we say that the process p, θ, e, l, f is terminated if e = v for some value v (normal termination) or e = r for some reason r (faulty termination).

Formally, a Core Erlang system supporting links is defined as a pool of floating messages, live and terminated processes, with the following grammar:

E := p, θ, e, l, f | (p, p , v) | (E 1 | E 2 )
By applying our approach we obtain the syntax for reversible Core Erlang supporting links below. As usual, keys and memories are added to the system.

R := k : p, θ, e, l, f | k : (p, p , v) | R 1 | R 2 | [R; C]
The new rules of the reversible semantics of Erlang supporting links are in Figure 4, but for rule (F-Nrm) which is very similar to rule (F-Err) and is given in Appendix A.6. We do not show the original semantics, which can however be easily deduced by removing keys and memories from the one in Figure 4. The reversible semantics includes also all the rules in Figure 8, with the only addition of the set of links l and flag f in each process, which are not affected by those rules, but for the fact that when a process is spawned its link set is initialised to empty and its flag to false.

Rule (F-SpLink) above is similar to rule (F-Spawn) in Figure 8, with the addition that the link between the two processes is created, by inserting the pid of the other process in the link set. Rules (F-Err) and (F-Nrm) are similar: they both model the signalling of the termination of a process p to all the processes it is linked with. In both of them links are broken, by removing pids from link sets. The effect of termination depends on whether it is a normal termination, as in rule (F-Nrm), or an error termination, as in rule (F-Err). Also, a termination signal affects system processes and non-system processes differently, and this is why in the two rules we split the processes in two groups according to the value of the flag. It can be set to the desired value using rule (F-Flag).

(F-Err) l = {p1, . . . , pm} 1 ≤ i ≤ n ⇒ f i = true ∧ n + 1 ≤ i ≤ m ⇒ f i = false h, h i , j i are fresh keys k : p, θ, r, l, f | 1≤i≤m k i : p i , θ i , e i , l i , f i h : p, θ, r, ∅, f | 1≤i≤n h i : p i , θ i , e i , l i \ {p}, f i | 1≤i≤n j i : (p, p i , { EXIT , p, r}) | n+1≤i≤m h i : p i , θ i , r, l i \ {p}, f i | [k : p, θ, r, l, f | 1≤i≤m k i : p i , θ i , e i , l i , f i ; h : • h | 1≤i≤m h i : • hi | 1≤i≤n j i : • ji ]
Figure 4 Forward rules of the reversible link semantics for Erlang

In rule (F-Err), the process terminates for some reason r. In this case messages { EXIT , p, r} where p is the pid of the terminated process are sent to all system processes while non-system processes are forced to terminate. We can see the latter, e.g., in non-system process p m , θ m , r, l m \ {p}, f m where expressions e m is replaced by reason r, denoting abnormal termination. A memory is generated as usual, recording the past state of the system and the configuration of the resulting processes.

In rule (F-Nrm), the process terminates normally. The only differences w.r.t. rule (F-Err) is that non-system processes are unaffected and the messages are of the form { EXIT , p, normal}.

Backward rules are as usual.

We need to couple the rules in Figure 4, describing the semantics of Erlang configurations, with rules describing the evaluation of expressions, as the ones in [29, Figure 11]. Two main changes are needed. First, evaluation of operators may produce either a value or an error:

(Call3) eval(op, v1, . . . , vn) = x with x = v ∨ x = r θ, call op(v1, . . . , vn) τ -→ θ, x
Then, one also needs to add rules to evaluate the functions spawn_link() and process_flag(). They are quite standard and can be found in Appendix A.6.

We are working to integrate the error mechanisms above into Erlang reversible debugger CauDEr [27]. CauDEr follows the reversible semantics of Core Erlang in [29], however our results can be rephrased in that setting, as hinted at by Theorems 25 and 27.

Conclusion, Related and Future Work

We presented a fully automatic method to extend a given forward model to a reversible one. Notably, our approach only needs a syntax and a reduction semantics of the forward model fitting our constraints. A causal semantics is produced as a by-product of our approach (see Definition 13). We exploited our method to obtain reversible extensions of Higher-Order π and Core Erlang. We showed that the obtained reversible semantics are equivalent to the ones in the literature [25,29]. As an illustration that our approach can go beyond the literature, we tackled Core Erlang constructs for remote error handling based on links.

Sequential systems would correspond in our framework to single entities which evolve using instances of schemas having a single entity both on the left-and on the right-hand side. While our approach would create a reversible semantics for them, undoing actions in reverse order of execution, many of our results would become trivial.

In the concurrency literature, one can find many approaches defining a single reversible formalism or studying its properties, all using techniques tailored to the chosen model (e.g., [10,9,25,38,17,37,3,18,28,36]). Indeed, our work can be seen as a generalisation of [25,28], which we also used as case studies. A few works present general approaches able to cope with a number of formalisms. Our work fits in this class, hence we compare it below with the other approaches of this kind we are aware of. Also, since we deal with concurrent models, we focus on approaches targeting them as well.

Beyond ours, the only work that we are aware of providing a general and fully automatic method to derive a reversible semantics is [41], which considers calculi defined in a specific SOS format. Their approach allows to deal with open systems since their semantics is SOS, while our approach based on a reduction semantics considers only close systems. On the other hand, the higher degree of abstraction provided by reduction semantics simplifies the approach and makes it applicable to a wider range of formalisms. Indeed, the approach in [41] cannot cope with our two case studies, Higher-Order π-calculus and Core Erlang, since they do not fit their SOS format.

Also [4], which presents a modular framework to define reversible extensions of models such as CCS and concurrent X-machines, can deal with open systems. Its main limitation is that it is not fully automatic. Indeed, it requires to manually refine the labels of a given LTS to ensure properties such as determinism and codeterminism. This is far from trivial.

Two abstract approaches to reversibility are [13] and [31]. The former focuses on the interplay between reversible and irreversible actions, hence its results become trivial if, like in our case, there are no irreversible actions. We exploited the latter to prove properties of reversible models built using our approach. It concentrates on deriving properties from a set of axioms but gives no indication about how to render an irreversible system reversible.

Uncontrolled reversible semantics as obtained by our approach are the foundation of a reversible model on which one can build on, by adding control mechanisms [24] such as irreversible actions [11], rollback operators [17] or energy potentials [2]. An interesting line for future work is to integrate such approaches in our framework. For rollback, we could follow the ideas in [22], which leave however open the issue of how to manage rollback targets.

Another direction for future work is to adapt our approach so to handle further forward models. For instance, we currently cannot cope with the semantics of muKlaim defined in [17], since its concurrency model includes read dependencies. In particular, our approach is based on consumed and produced resources, while in [17] resources can also be read without being consumed. More in general, our approach can cope well with message-based concurrency modelled by some form of happened-before relation [20] (e.g., beyond our case studies, CCS, π-calculus and place-transition Petri nets) but not with read-write concurrency (e.g., beyond muKlaim, imperative languages). In order to extend our method to cope with read-write concurrency, we need to identify resources which are read but not consumed.

A last direction for future work concerns reducing the memory overhead of our approach. While it is difficult to find optimisations sound for every instance, many optimisations can work on specific classes of instances. E.g., in models where the context T in the instances of schema (Scm-Act) is always composed by parallel operators only, as in Core Erlang, there is no need to store T , but it is enough to store the set of fresh keys.

(F-Par) R R (key(R ) \ key(R)) ∩ key(R1) = ∅ R | R1 R | R1 (F-Res) R R νa (R) νa (R ) (F-Eqv) R ≡ R R R1 R1 ≡ R 1 R R 1 (B-Act) µ = [k1 : a P | k2 : a(X) P ; T [j1 : •1, . . . , jm : •m]] T [j1 : Q1, . . . , jm : Qm] | µ k1 : a P | k2 : a(X) P (B-Par) R R R | R1 R | R1 (B-Res) R R νa (R ) νa (R) (B-Eqv) R ≡ R R R1 R1 ≡ R 1 R R 1
Figure 5 Forward and backward rules of the reversible semantics for the Higher-Order π-calculus

A Proofs and further technical material

A.1 Higher-Order π-calculus and reversible HOπ-calculus

This section recalls the semantics of the HOπ-calculus [43], discusses how it fits our framework and details the reversible semantics derived for it using our approach.

The standard rules of the structural congruence for the HOπ-calculus are:

(ParC) P | Q ≡ Q | P (ParA) P | (Q | S) ≡ (P | Q) | S (Nil) P | 0 ≡ P (Alpha) νa P ≡ νb P {b/a} if b / ∈ fn(P ) (ResF) (νa P ) | Q ≡ νa (P | Q) if a / ∈ fn(Q)
Rules ParC and ParA ensure that parallel composition is commutative and associative, while rule Nil defines 0 as neutral element as required by our framework. Rules Alpha and ResF can be seen as infinite families of rules, for each a, b, P and Q satisfying the side conditions. Hence, side conditions are not needed in the instance. The semantics of HOπ is given with the reduction relation below:

(Act) a Q | a(X) P P {Q/X} (Par)

P P P | Q P | Q (Res)
P P νa P νa P (Eqv)

P ≡ P P Q Q ≡ Q P Q
Rule (Act) is the communication rule where process Q is received and bound to variable X. Process P can execute inside a parallel or a restriction operator thanks to rules (Par) and (Res), respectively. Rules (Par) and (Eqv) are as required by our framework. Rules (Act) and (Res) can be seen as infinite families of rules fitting schemas (Scm-Act) and (Scm-Opn), respectively.

In Figure 5, we give forward and backward rules of the reversible semantics for the HOπ-calculus derived using our approach.

col(νa (R)) = col(R) col(R 1 | R 2 ) = col(R 1 ) ∪ col(R 2 ) col([R ; C]) = {key(C) k } where k is fresh if |key(C)| > 1 col([R ; C]) = {key(C)} if |key(C)| = 1 col(k : P ) = ∅ col(0) = ∅ Figure 6 Function col()
Below, we give a necessary auxiliary definition and proof that our framework satisfies properties CS and CL.

Definition 35 (Independence respects events (IRE)). Whenever t 1 ≈ t c t 2 we have t 1 c t 2 .

A.3 Correspondence between our reversible HOπ and ρπ

This section contains technical material necessary to prove the correspondence between our reversible HOπ and ρπ (Theorem 24 of Section 4.1).

In the following, we recall the definition of a thread normal form from [25, Lemma 1] using which, by exploiting structural congruence, unique keys are generated for each primitive thread process in a configuration (primitive thread processes are entities in our terminology).

Definition 37 (Thread normal form). For any closed configuration M in ρπ, we have

M ≡ ν ũ i∈I (κ i : ρ i ) j∈J [µ j ; k j ] with ρ i = a i P i or ρ i = a i (X i ) P i
The encoding works in two steps: a first step explores memories in our reversible systems to find related sets of keys, the second step uses the gathered information to actually perform the translation. The first step of translation is done by the function col(R) which computes sets of keys extracted from the memory component C. Additionally, if C contains more than one key, the extracted set of keys is annotated with a fresh key k, what is denoted with key(C) k . The formal definition of function col(R) is in Figure 6. Note that the result of function col(R) is a set of sets of keys. We denote with hk and h sets key(C) k and key(C), respectively. We also assume to have a fresh key generator, giving us fresh keys k as needed.

The second step performs the translation of a given system R and uses as a parameter a set of sets of keys S as above, which is initialised as S = col(R). Let us denote with M the set of all ρπ [25] configurations in normal form and with R the set of all reversible systems obtained by applying our approach to the HOπ-calculus. The encoding function

• : R -→ M, is defined as:

R = νK R col(R) where K = ( hk ∈col(R) h ∪ {k}) ∪ {h}∈col(R) {h} νa R S = νa R S R 1 | R 2 S = R 1 S | R 2 S [R ; C] S = [ R S ; C S ] h : P S = h, h • k : P if h ∈ h for some hk ∈ S h : P S = h : P if h / ∈ h for all hk ∈ S C S = k if key(C) k ∈ S C S = h if key(C) = {h}
Let us comment on it. The first rule computes the parameter col(R) containing information on keys, to be used in the rest of the translation, and creates restrictions for all the keys occurring in it. The other rules just propagate the set S, till one of the last 4 rules applies. The first two deal with keys labeling processes: it the key belongs to a non-singleton set, then it is replaced by a complex tag, otherwise it is left unchanged. The two last rules remove the context C in the memory, which is not needed in ρπ, replacing it with a key. If C contains only one key, this is the key used. If it contains more than one key instead the fresh key k generated for the set of keys is used. The keys in the set will become complex tags, carrying k so to make the connection between the memory and all the processes created by the corresponding transition.

Let us show a simple example to clarify how the translation works.

Example 38. Let us consider the system produced by the sample transition in Section 4.1:

R = j 1 : P 1 | j 2 : P 2 | [R ; j 1 : • 1 | j 2 : • 2 ] We have col(R ) = {{j 1 , j 2 } k }
where k is a fresh key. We now have:

R =νj 1 , j 2 , k R col(R ) = =νj 1 , j 2 , k j 1 : P 1 col(R ) | j 2 : P 2 col(R ) | [R ; j 1 : • 1 | j 2 : • 2 ] col(R ) =νj 1 , j 2 , k j 1 , {j 1 , j 2 } • k : P 1 | j 2 , {j 1 , j 2 } • k : P 2 | [ R col(R ) ; j 1 : • 1 | j 2 : • 2 col(R ) ] =νj 1 , j 2 , k j 1 , {j 1 , j 2 } • k : P 1 | j 2 , {j 1 , j 2 } • k : P 2 | [R ; k]
where R is unchanged since it only contains keys not occurring in col(R ).

In the following, we show that there exists a transition in reversible HOπ if and only if there exists a corresponding transition in ρπ.

Lemma 39. Let R be a reachable system in reversible HOπ and R = M . For each transition in our reversible HOπ R -→ R , there exists a corresponding ρπ transition M -→ M with M ≡ R .

Proof. Forward transitions: by induction on the derivation R R and by case analysis on the last applied rule.

F-Act we have transition

k 1 : a P | k 2 : a(X) P T [j 1 : Q 1 , . . . , j m : Q m ] | [k 1 : a P | k 2 : a(X) P ; C] = R
where C = T [j 1 : • 1 , . . . , j m : • m ], with the premise a P | a(X) P P {P/X} with P {P/X} ≡ T

[Q 1 , . . . , Q m ]
In ρπ we have R = M = k 1 : a P | k 2 : a(X) P and we can separate two cases, depending whether the resulting process P {P/X} has a parallel composition on the top-level or not.

• If resulting process does not have a parallel composition on top-level, then P {P/X} ≡ νã Q 1 and we have system R = νã j 1 :

Q 1 | [k 1 : a P | k 2 : a(X) P ; νã [j 1 : • 1 ]].
In ρπ by applying rule (R.Fw) on configuration M , we have

k 1 : a P | k 2 : a(X) P νj 1 . (j 1 : P {P/X}) | [k 1 : a P | k 2 : a(X) P ; j 1 ] = M
For configuration M , by Definition 37, there is a normal form

M = νã, j 1 . (j 1 : Q 1 ) | [k 1 : a P | k 2 : a(X) P ; j 1 ]
By applying encoding function • on R , we have M = R with M ≡ M = R .

• If the resulting process has a parallel composition on top-level, then we can assume that P {P/X} consists of m entities and

P {P/X} ≡ νã (Q 1 | • • • | Q m )
. Now, we have system

R = νã (j 1 : Q 1 | • • • | j m : Q m ) | [k 1 : a P | k 2 : a(X) P ; νã (j 1 : • 1 | • • • | j m : • m )]
In ρπ by applying rule (R.Fw) on configuration M , we have

M = νã, k, j. i∈I j i , j • k : Q i | [k 1 : a P | k 2 : a(X) P ; k]
By applying encoding function

• on R , we have M = R with M ≡ M = R . F-Par then R = R 1 | R 2 and we have transition R 1 | R 2 R 1 | R 2 with premise R 1 R 1 where (key(R 1 )\key(R 1 ))∩key(R 2 ) = ∅. Systems R, R 1 and
R 2 where set I = {1, . . . , n}, can be written as:

R = νã (k : a P | k : a(X) P ) | ν b i∈I (k i : ρ i ) | j∈J [S j ; C j ]
where

R 1 = νã (k : a P | k : a(X) P ) and R 2 = ν b i∈I (k i : ρ i ) | j∈J [S j ; C j ]
Now, system R 1 can execute forward step and we obtain system

R 1 = νã T [j 1 : Q 1 , . . . , j m : Q m ] | [k : a P | k : a(X) P ; T [j 1 : • 1 , . . . , j m : • m ]] while system R is R = νã T [j 1 : Q 1 , . . . , j m : Q m ] | [k : a P | k : a(X) P ; T [j 1 : • 1 , . . . , j m : • m ]] | R 2
When we apply the encoding function • on systems R and R 1 , we obtain configurations

M = R and M 1 = R 1 such that M = ν ũ, ã. (κ : a P | κ : a(X) P ) | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
where keys k , k and k i are translated into tags κ , κ and κ i for i ∈ {1, . . . , n}. Symbol ũ represents the restricted names b and new keys generated while translating system R.

Past states S j are encoded into ρπ past states µ j and contexts C j are substituted with keys t j . We can derive the configuration M 1 as:

M 1 = ν ũ, ã. (κ : a P | κ : a(X) P ) By inductive hypothesis, we have that R 1 R 1 and M 1 = R 1 implies M 1 M 1 with M 1 ≡ R 1 .
Then in ρπ we obtain configuration

M 1 = ν ũ, ã, t. t : P {P/X} | [κ : a P | κ : a(X) P ; t]
Now, we have two cases depending whether P {P/X} has a parallel composition on the top-level or not.

• if there is no parallel composition on the top-level in process P {P/X}, we have

P {P/X} = νc Q 1 and configuration M 1 is M 1 = ν ũ, ã, t. t : νc Q 1 | [κ : a P | κ : a(X) P ; t]
In ρπ, we can apply rule (R.Ctx) on configuration M with premise M 1 M 1 and obtain a configuration

M = ν ũ, ã, t. t : νc Q 1 | [κ : a P | κ : a(X) P ; t] | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
For configuration M , there is a normal form

M = ν ũ, ã, c, t. t : Q 1 | [κ : a P | κ : a(X) P ; t] | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
By applying encoding function • on R , we have M ≡ M = R where T [j 1 : Q 1 , . . . , j m : Q m ] = νc t : Q 1 since there is no parallel composition.

• if there is a parallel composition on the top-level in process P {P/X}, we have

P {P/X} ≡ νc (Q 1 | • • • | Q m ) and configuration M 1 is M 1 ≡ ν ũ, ã, t. t : νc (Q 1 | • • • | Q m ) | [κ : a P | κ : a(X) P ; t]
In ρπ, we can apply rule (R.Ctx) on configuration M with premise M 1 M 1 and obtain a configuration

M ≡ ν ũ, ã, t. t : νc (Q 1 | • • • | Q m ) | [µ ; t] | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
For configuration M and set L = {1, . . . , m}, there is a normal form M M = ν ũ, ã, c, j, t. t :

l∈L (δ l : Q l ) | [µ ; t] | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
In reversible HOπ, by applying rule (F-Par) on system R with premise R 1 R 1 , we obtain a system

R = νã, c j 1 : Q 1 | [k : a P | k : a(X) P ; νc j 1 : • 1 ] | R 2 Now for k = j 1 , we have R = M ≡ M .
• if there is a parallel composition on the top-level in process P {P/X}, we have

P {P/X} ≡ νc (Q 1 | • • • | Q m ) and normal form of process M is M = ν ũ, ã, c, j, k. i∈I j i , j • k : Q i | [µ; k] | ν ũ i∈I (κ i : ρ i ) | j∈J [µ j ; t j ]
where µ = k : a P | k : a(X) P , I = {1, . . . , m} and j = {j 1 , . . . , j m }. In reversible HOπ, by applying rule (F-Par) on system R with premise R 1 R 1 , we obtain a system

R = νã, c (j 1 : Q 1 | • • • | j m : Q m ) | [k : a P | k : a(X) P ; C] | R 2 where C = νc (j 1 : • 1 | • • • | j m : • m )
. Then, we have R = M ≡ M as desired. R.Eqv then for a system R and its translation to ρπ R = M , we have M M with premise M ≡ M 1 , M 1 M 1 , M 1 ≡ M . By inductive hypothesis, there are systems

R 1 and R 1 such that R 1 R 1 with R 1 = M 1 and R 1 ≡ M 1 .
Since M 1 and M are translations of systems R 1 and R, from M ≡ M 1 ( R ≡ R 1 )we can conclude R ≡ R 1 (from the fact that encoding function preserves structural congruence). Now, on system R we can apply rule (F-Eqv) and obtain R ≡ M , as desired. Backward transitions: given a system R, its translation to ρπ is R = M , from ρπ Loop Lemma [25, Lemma 6], we have M M implies M M . Since lemma holds for forward transitions, we have that there exists a corresponding transition in our reversible HOπ R R, with M = R and M ≡ R . By applying Loop Lemma (Lemma 14) we have R R , as desired.

Theorem 24. Let R be a reachable configuration of reversible HOπ with R = M . There is a transition R -→ R in reversible HOπ iff there is a ρπ transition M -→ M with R ≡ M .

Proof. The proof is a direct consequence of lemmata 39 and 40.

A.4 Classic and reversible semantics for Core Erlang

This section recalls a reduction semantics for Core Erlang [29] and presents forward and backward rules of the reversible semantics for Core Erlang obtained using approach (Section 4.2).

In Figure 7 we give the reduction semantics for Core Erlang. The function pid(•) used in rule (Par) extracts the set of pids of processes in a given system. It is used to ensure that the pid of the newly spawned process is fresh.

The forward rules of the reversible semantics are given in Figure 8. Rule (F-Par) allows configurations to execute as part of a larger configuration with the additional condition that keys generated by the execution are not part of the parallel configuration.

Backward rules of the reversible semantics are given in Figure 9. Notably, to capture exactly the instances produced by our approach some side conditions would be needed. E.g., in rule B-Par one would need condition pid(R ) ∩ pid(R ) = ∅. However, such conditions are always satisfied in reachable configurations.

E → E pid(E ) ∩ pid(E1) = ∅ E | E1 → E | E1
Figure 7 System rules of standard Core Erlang

A.5 Causal correspondence and barbed equivalence between reversible semantics of Erlang

This section contains proofs of Theorems 25 and 27 (Section 4.2).

Causal correspondence between two reversible semantics of Erlang

Lemma 41. Two different coinitial transitions t 1 and t 2 of our reversible Core Erlang semantics are in conflict according to Definition 13 if they are in conflict according to [29,Definition 12].

Proof. From [29,Definition 12] we have that two different coinitial transitions are in conflict if:

both transitions are forward, they consider the same process p and the applied rule on both transition is receive (in one transition, received message is identified with key k 1 , while in the other, message is identified with k 2 , where k 1 = k 2 ).

In our reversible semantics, we assume to have two coinitial transitions t 1 and t 2 , which execute rule (F-Rec) on the same process p identified with the key k. Since they are both executed on the same process, we have k ∈ key(µ 1 ) and k ∈ key(µ 2 ), where µ 1 and µ 2 are memories created by transitions t 1 and t 2 , respectively. Therefore, we have k ∈ key(µ 1 ) ∩ key(µ 2 ) and by Definition 13, transitions t 1 and t 2 are in conflict. one transition is forward, applied on the process p 1 and the other one is backward transition that undoes the spawning of the process p 1 .

In our reversible semantics, we assume to have two coinitial transitions t 1 and t 2 , where t 1 is forward transition applied on the process p 1 and t 2 is backward transition that undoes the spawning of the process p 1 . In this case, memory produced by transition t 1 is

µ 1 = [R 1 ; C 1 ] and consumed by transition t 2 is µ 2 = [R 2 ; C 2 ].
Let us assume that the process p 1 is identified with the key k before the execution of transitions t 1 and t 2 (i.e. we have a process k : p 1 , θ, e belonging to our initial system). Now, since transition t 1 is applied on the process p 1 it implies k ∈ key(R 1 ). Transition t 2 consumes the memory produced in the action that spawned process p 1 , hence we have k ∈ key(C 2 ). Therefore, from Definition 13 we have k ∈ key(µ 1 ) ∩ key(µ 2 ) and transitions t 1 and t 2 are in conflict. one is a forward transition where process p 1 receives a message with the key k and the other one is a backward transition that undoes the sending of the same message. (F-Spawn)

θ, e In our reversible semantics, we assume to have two coinitial transitions t 1 and t 2 , where t 1 is a forward transition where process p 1 receives a message with the key k and t 2 is a backward transition that undoes the sending of the same message. This case is very similar to the previous one. For memory µ 1 = [R 1 ; C 1 ], produced by transition t 1 , holds k ∈ key(R 1 ) (since the message identified with k is consumed) and for memory µ 2 = [R 2 ; C 2 ], consumed by transition t 2 , holds k ∈ key(C 2 ) (since t 2 undoes the sending of the message identified by k ). Therefore, by Definition 13 we have k ∈ key(µ 1 ) ∩ key(µ 2 ) what implies that transitions t 1 and t 2 are in conflict. one transition is a forward and the other one is a backward transition such that p 1 = p 2 = p.

spawn(κ,f /n,[vn ]) ------------→ θ ,
(F-Par) R R pid(R ) ∩ pid(R ) = ∅ and (key(R ) \ key(R)) ∩ key(R ) = ∅ R | R R | R
In our reversible semantics, we assume to have two coinitial transitions t 1 (forward) and t 2 (backward) executed on the same process p. If the key of the process p is k, then for transition t 1 holds k ∈ key(R 1 ) (since t 1 is a forward transition which consumes process p), where µ 1 = [R 1 ; C 1 ] is the memory produced by transition. On the other side, for the transition t 2 , will hold k ∈ key(C 2 ) (since t 2 is a backward transition executed on the process p), where µ 2 = [R 2 ; C 2 ] is the memory consumed by transition. Therefore, from Definition 13 we have that transitions t 1 and t 2 are in conflict.

Lemma 42. Two different coinitial transitions t 1 and t 2 of our reversible Core Erlang semantics are in conflict according to [29,Definition 12] if they are in conflict according to Definition 13.

Proof. By Definition 13 we have that two coinitial transitions t 1 and t 2 are in conflict if key(µ 1 ) ∩ key(µ 2 ) = ∅ where µ 1 = [R 1 ; C 1 ] and µ 2 = [R 2 ; C 2 ] are memories produced or consumed by transitions t 1 and t 2 . Now, we have three basic cases when expression key(µ 1 ) ∩ key(µ 2 ) = ∅ is satisfied:

if there exists a key k such that k ∈ key(R 1 ) ∧ k ∈ key(R 2 ), then we have the following options:

-both transitions are forward and executed on the same process. The only possibility that two different forward transitions are executed on the same process is if the applied rule for both transitions is (F-Rec) where transitions are receiving different messages. In the logging semantics [29], this case corresponds to the first case of [29, Definition 12].

-both transitions are backward and executed on the same process. This case is impossible since transitions are coinitial and different. In particular, the only possibility to execute two backward coinitial transitions on the same process is if µ 1 = µ 2 . Therefore, we have t 1 = t 2 , what is not the case, since transitions are different. if there exists a key k such that k ∈ key(R 1 ) ∧ k ∈ key(C 2 ) or k ∈ key(C 1 ) ∧ k ∈ key(R 2 ). In this case, the only option is if one transition is forward and one is backward. Let us show the case when k ∈ key(R 1 ) ∧ k ∈ key(C 2 ), the other case is similar. Then we have that t 1 is a forward and t 2 is a backward transition. Now we have the following cases depending whether transitions are executed on the same process or not:

-transitions are executed on the same process. In the reversible logging semantics [29], this case corresponds to the forth case of [29,Definition 12].

-transitions are executed on two different processes. Then we have two special subcases: (i) transition t 1 is executed on the process p and transition t 2 undoes the spawning of the process p. In the logging semantics [29], this case corresponds to the second case of [29,Definition 12].

(ii) with transition t 1 process receives the message identified with the key k and transition t 2 undoes the sending of the message identified with k. In the logging semantics [29], this case corresponds to the third case of [29,Definition 12].

if there exists a key k such that k ∈ key(C 1 ) ∧ k ∈ key(C 2 ). Then we have the following options depending on whether the transitions t 1 and t 2 are forward or backward:

-both transitions are backward; in this case, since we are limited on reachable processes, t 1 = t 2 , what is not the case.

-both transitions are forward; this case can be avoided because of the non-determinism in the choice of the fresh identifier k when a new entity is produced Theorem 25 (Causal correspondence). Two coinitial transitions t 1 and t 2 of our reversible Core Erlang semantics are in conflict according to [29,Definition 12] iff they are in conflict according to Definition 13.

Proof. The proof is a direct consequence of lemmata 41 and 42.

Strong back and forth barbed equivalence between two reversible semantics of Erlang

The difference between a simple forward Erlang system (Figure 7) and the one of [29, Figure 14] is that we used the floating messages instead of the global mailbox Γ. In Figure 10 we recall the forward rules of reversible logging semantics [29] where floating messages are used instead of the global mailbox. This modification does not have any impact on the behaviour of the system, it just allows for a simpler technical treatment.

In the following, we recall definitions of an initial process in both reversible models.

Definition 43. Logging reversible system is initial when there are no floating messages in the system and every process is of the shape p, w, (), id, e , where id is the identity substitution.

Definition 44. Our reversible system is initial when there are no memory and floating messages in the system and every process is of the shape p, id, e , where id is the identity substitution.

Remark 45. The initial system does not have any past information, therefore it has no backward moves. For every reversible process, the initial system is unique. We denote initial systems of reversible logging and our reversible semantics of Erlang with L i and R i , respectively.

In what follows, we define the erasing function δ(•) which given a logging system L, generates the Erlang system E, by deleting all past information. Definition 46. The erasing function δ : L -→ E that maps reversible logging system to the simple forward Erlang system is defined as:

Figure 1

 1 Figure 1 Forward rules structure; Scm-rules are schemas

  send(p ,v) ------→ θ , e p, θ, e → p, θ , e | (p, p , v) (Rec) θ, e rec(κ,cln) ------→ θ , e and matchrec(θ, cln, v) = (θ i , e i ) (p , p, v) | p, θ, e → p, θ θ i , e {κ → e i }

  ---→ θ , e k1, k2 are fresh keys k : p, θ, e k1 : p, θ , e | k2 : (p, p , v) | [k : p, θ, e ; k1 : •1 | k2 : ---→ θ , e and matchrec(θ, cln, v) = (θ i , e i ) k1 is a fresh key k2 : (p , p, v) | k : p, θ, e k1 : p, θ θ i , e {κ → e i } | [k2 : (p , p, v) | k : p, θ, e ; k1 : •1]

  k1, k2 are fresh keys k : p, θ, p !5 k1 : p, θ, 5 | k2 : (p, p , 5) | [k : p, θ, p !5 ; k1 : •1 | k2 : •2]

(

  B-Send) k1 : p, θ , e | k2 : (p, p , v) | [k : p, θ, e ; k1 : •1 | k2 : •2] k : p, θ, e (B-Rec) k1 : p, θ , e | [k2 : (p , p, v) | k : p, θ, e ; k1 : •1] k2 : (p , p, v) | k : p, θ, e

  f /n,[vn])---------------→ θ , e p is a fresh pid k1, k2 are fresh keysk : p, θ, e, l, f k1 : p, θ , e {κ → p }, l ∪ {p }, f | k2 : p , id, apply f /n (vn), {p}, f alse | [k : p, θ, e, l, f ; k1 : •1 | k2 : ----------------→ θ ,e k1 is a fresh key k : p, θ, e, l, f k1 : p, θ , e {κ → f }, l, f | [k : p, θ, e, l, f ; k1 : •1]

  j1, . . . jm are fresh keys and P {P/X} = T [Q1, . . . , Qm] k1 : a P | k2 : a(X) P T [j1 : Q1, . . . , jm : Qm] | [k1 : a P | k2 : a(X) P ; T [j1 : •1, . . . , jm : •m]]

Property 4 .

 4 LTSI (R, L, -→, c ) satisfies IRE. Proof. The proof follows from [31, Proposition 5.3 (1)] and the fact that (R, L, -→, c ) satisfies (CIRE) (Proposition 20). Theorem 36. LTSI (R, L, -→, c ) satisfies Causal Safety and Causal Liveness. Proof. The proofs of Causal Safety and Causal Liveness, follow from the fact that our framework satisfies properties (IRE) and (CPI) (Property 4 and Proposition 20) and by [31, Theorem 4.13] and [31, Theorem 4.14], respectively.

k 1 :

 1 a P | k 2 : a(X) P νk. (k : P {P/X}) | [k 1 : a P | k 2 : a(X) P ; k] = M For configuration M and set I = {1, . . . , m}, by Definition 37, there is a normal form

  ---→ θ , e and matchrec(θ, cln, v) = (θ i , e i ) (p , p, v) | p, θ, e → p, θ θ i , e {κ → e i } , e → p, θ , e | (p, p , v) f /n,[vn]) -----------→ θ , e p is a fresh pid p, θ, e → p, θ , e {κ → p } | p , id, apply f /n (vn) (Par)

  k : p, θ, e k1 : p, θ , e | [k : p, θ, e ; k1 : •1] are fresh keys k : p, θ, e k1 : p, θ , e | k2 : (p, p , v) | [k : p, θ, e ; k1 : •1 | k2 : •2] ----→ θ , e and matchrec(θ, cln, v) = (θi, ei) k1 is a fresh key k2 : (p , p, v) | k : p, θ, e k1 : p, θ θi, e {κ → ei} | [k2 : (p , p, v) | k : p, θ, e ; k1 : •1]

Figure 8 Figure 9

 89 Figure 8 Forward rules of the reversible semantics for Erlang

(Figure 10

 10 Figure 10 Uncontrolled reversible logging semantics for Erlang

  δ(L 1 | L 2 ) = δ(L 1 ) | δ(L 2 ) δ((p, p , {v, k })) = (p, p , v)δ( p, w, h, θ, e ) = p, θ, e

  rules of the uncontrolled reversible semantics

			µ = [k1 : P1 | . . . | kn : Pn ; T [j1 : •1, . . . , jm : •m]]
		(B-Scm-Act)	T [j1 : Q1, . . . , jm : Qm] | µ	k1 : P1 | . . . | kn : Pn
		R i	R i
	(B-Scm-Opn)	opn(R0, . . . , R i , . . . , Rn)	opn(R0, . . . , R i , . . . , Rn)

  Below, we give the communication rule of the forward and backward reversible semantics for the HOπ-calculus. The other rules can be found in Appendix A.1. T [j 1 : • 1 , . . . , j m : • m ]], recording the prior state of the configuration and the context with the new fresh keys, is generated. After the communication we obtain the system P {P/X} which we can rewrite as a termT [Q 1 , . . . , Q m ],where Q 1 , . . . , Q m are entities. Using rule (B-Act) the configuration can undo the forward step which produced the memory µ. The prior state of the system is restored from it.

	a P | a(X) P Example 9. (F-Act) k1 : a P | k2 : a(X) P P {P/X}	j1, . . . jm are fresh keys and P {P/X} = T [Q1, . . . , Qm] T [j1 : Q1, . . . , jm : Qm] |
				[k1 : a P | k2 : a(X) P ; T [j1 : •1, . . . , jm : •m]]
			µ = [k1 : a P | k2 : a(X) P ; T [j1 : •1, . . . , jm : •m]]
	(B-Act)	T [j1 : Q1, . . . , jm : Qm] | µ	k1 : a P | k2 : a(X) P
	Using rule schema (F-Act) a configuration can execute a forward step in which the memory
	µ = [k 1 : a P | k 2 : a(X) P ;
	Definition 8 (Uncontrolled reversible semantics). The reduction relation	(resp.	),
	defined as the smallest relation closed under the forward (resp. backward) rules, defines the
	forward (resp. backward) reversible semantics. The semantics, denoted by -→, is the union of
	the forward semantics	and the backward semantics	(i.e. -→= ∪	).

  e 2 are (coinitially) independent, written e 1 ci e 2 , iff there are coinitial transitions t 1 and t 2 such that [t 1 ] = e 1 , [t 2 ] = e 2 and t 1 c t 2 .Given that our reversible semantics satisfies all the axioms, thanks to[31], all instances of our framework satisfy the Parabolic Lemma, Causal Consistency, Causal Safety and Causal Liveness, defined below. Given two coinitial derivations d 1 and d 2 , d 1 ∼ d 2 if and only if d 1 and d 2 are cofinal. Below, we state Causal Safety and Causal Liveness. We present them in a slightly rephrased and more intuitive form w.r.t. [31], whose presentation is however more formal.

	Definition 23 (Causal Safety (CS) and Causal Liveness (CL)).
	Let L = (R, L, -→,

Definition 19 (Coinitial independence respects events (CIRE)). If [t 1 ] ci [t 2 ] and t 1 and t 2 are coinitial, then t 1 c t 2 . Proposition 20. Axioms SP, BTI, WF, CPI and CIRE hold for each instance of our framework. Definition 21 (Parabolic Lemma (PL)). Given a derivation d : R -→ * R , there exists a configuration R such that d : R * R * R and d ∼ d . Also, d is not longer than d. Definition 22 (Causal Consistency (CC)). c ) be a LTSI satisfying SP,BTI,WF and CPI. Take a derivation R µ

  is a strong back and forth barbed bisimulation if R and R -1 are strong back and forth barbed simulations. Strong back and forth barbed bisimilarity is the largest strong back and forth barbed bisimulation. Now we can state the equivalence result between the two semantics.

	Theorem 27. The reversible semantics of Erlang in [29] and our reversible semantics of
	Erlang are strong back and forth barbed bisimilar.

  If an error occurred during the computation message { EXIT , P id, {badarith, Stack}} is received and the function returns atom invalid.

	total(List) -→
	process_flag(trap_exit, true),
	SumPid = spawn_link(?M ODU LE, sumProcess, [self (), List]),
	receiveValue(SumPid).
	sumProcess(P id, List) -→ P id ! sum(List).
	sum([ ]) -→ 0;
	sum([H|T ]) -→ H + sum(T ).
	receiveValue(P id) -→
	receive
	{ EXIT , P id, normal} -→
	receive V alue -→ V alue end;
	{ EXIT , P id, {badarith, Stack}} -→ invalid
	end.

Funding This work has been partially supported by French ANR project DCore ANR-18-CE25-0007. The first author has also been partially supported by INdAM as member of GNCS (Gruppo Nazionale per il Calcolo Scientifico).

Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of

-5_23. Ivan Lanese, Davide Sangiorgi, and Gianluigi Zavattaro. Playing with bisimulation in Erlang. In Models, Languages, and Tools for Concurrent and Distributed Programming -Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, pages 71-91, 2019. doi:10.1007/978-3-030-21485-2_6. Johan Sund Laursen, Ulrik Pagh Schultz, and Lars-Peter Ellekilde. Automatic error recovery in robot assembly operations using reverse execution. In 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2015, Hamburg, Germany, September 28 -October 2, pages 1785-1792. IEEE, 2015. doi:10.1109/IROS.2015.7353609. Christopher Lutz. Janus: a time-reversible language. Letter to R. Landauer., 1986. URL: http://tetsuo.jp/ref/janus.html. James McNellis, Jordi Mola, and Ken Sykes. Time travel debugging: Root causing bugs in commercial scale software. CppCon talk, https://www.youtube.com/watch?v=l1YJTg_A914, 2017. Hernán C. Melgratti, Claudio Antares Mezzina, and Irek Ulidowski. Reversing P/T nets. In Hanne Riis Nielson and Emilio Tuosto, editors, Coordination Models and Languages -21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, Proceedings, volume 11533 of Lecture Notes in Computer Science, pages 19-36. Springer, 2019. doi:10.1007/978-3-030-22397-7_2. Claudio Antares Mezzina. On reversibility and broadcast. In Reversible Computation -10th International Conference, RC 2018, Leicester, UK, September 12-14. Proceedings, volume 11106 of Lecture Notes in Computer Science, pages 67-83. Springer, 2018. doi:10.1007/ 978-3-319-99498-7_5. Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies: a monitors-as-memories approach. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 -11, 2017, pages 127-138. ACM, 2017. doi:10.1145/3131851.3131864. Anna Philippou and Kyriaki Psara. Reversible computation in Petri nets. In Reversible Computation -10th International Conference, RC 2018, Leicester, UK, September 12-14, Proceedings, pages 84-101, 2018. doi:10.1007/978-3-319-99498-7_6. Iain Phillips, Irek Ulidowski, and Shoji Yuen. A reversible process calculus and the modelling of the ERK signalling pathway. In Reversible Computation, 4th International Workshop, RC 2012, Copenhagen, Denmark, July 2-3. Revised Papers, pages 218-232, 2012. doi: 10.1007/978-3-642-36315-3_18. Iain C. C. Phillips and Irek Ulidowski. Reversing algebraic process calculi. J. Log. Algebraic Methods Program., 73(1-2):70-96, 2007. doi:10.1016/j.jlap.2006.11.002. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61:17-139, 2004. Davide Sangiorgi. Bisimulation for higher-order process calculi. Inf. Comput., 131(2):141-178, 1996. doi:10.1006/inco.1996.0096. Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel. Models of concurrency: Towards a classification. Theoretical Computer Science, 170(1-2):297-348, 1996. doi:10.1016/ S0304-3975(96)80710-9. Ulrik Pagh Schultz. Reversible object-oriented programming with region-based memory management -work-in-progress report. In RC, volume 11106 of Lecture Notes in Computer Science, pages 322-328. Springer, 2018. doi:10.1007/978-3-319-99498-7_22. Irek Ulidowski, Iain Phillips, and Shoji Yuen. Reversing event structures. New Generation Comput., 36(3):281-306, 2018. doi:10.1007/s00354-018-0040-8.

A.2 Properties of our reversible framework

This section contains proofs of Theorem 12, Lemma 14 and Proposition 20. Moreover, here can be found further technical material of Section 3.1.

Correspondence between reversible and forward semantics

Theorem 12 is proved by combining two auxiliary lemmata (Lemma 29 and Lemma 30). We start by defining strong bisimilarity between the forward semantics of a reversible system R and the semantics of its projection on the forward model ϕ(R).

Definition 28. A relation R between reversible systems R and forward-only systems N is a strong bisimulation whenever for each (R,

Strong bisimilarity is the largest strong bisimulation.

Notably, only forward actions of the reversible systems need to be matched.

Lemma 29. For each transition R R , there is a transition ϕ(R) ϕ(R ).

Proof. By induction on the derivation of R R . We have three cases: We suppose that R R is obtained by applying rule (F-Scm-Act). Then systems R and R are of the form R = k 1 :

, the thesis follows. We suppose that R R is obtained by applying rule (F-Scm-Opn). Then systems R and R are R = op n (R 1 , . . . , R i , . . . , R n ) and R = op n (R 1 , . . . , R i , . . . , R n ), and R R is obtained with hypothesis R i R i . By using inductive hypothesis, lemma holds for R i R i , therefore we have ϕ(R i ) ϕ(R i ). By applying rule (Scm-Opn) on system ϕ(R) = op n (ϕ(R 1 ), . . . , ϕ(R i ), . . . , ϕ(R n ) with a premise ϕ(R i ) ϕ(R i ), we obtain a system op n (ϕ(R 1 ), . . . , ϕ(R i ), . . . , ϕ(R n ) = ϕ(R ), as desired. We suppose that R R is obtained by applying rule (F-Eqv). Then we have R R with hypothesis R ≡ R 1 , R 1 R 1 and R 1 ≡ R . By using inductive hypothesis we have that R 1 R 1 implies ϕ(R 1 ) ϕ(R 1 ). The thesis follows from the fact that structural congruence is preserved by ϕ.

Lemma 30. For each transition N

N and for all reachable R such that ϕ

Proof. By induction on the derivation of N N . We have three cases: We suppose that N N is obtained thanks to rule (Scm-Act). Then systems N and N can be represented as

We suppose that N N is obtained thanks to rule (Scm-Opn). Then systems N and N can be represented as

The transition N N is then obtained with hypothesis N i N i . By inductive hypothesis the thesis holds for

The thesis follows from the fact that structural congruence is preserved by ϕ and by application of the rule (F-Eqv) to a reachable R such that ϕ

Theorem 12. For each configuration R, its forward semantics and the semantics of ϕ(R) are strong bisimilar.

Proof. We will show that if for reversible systems the forward semantics is considered, then

If R does a forward move, R R , then by Lemma 29, we have a transition ϕ(R) ϕ(R ). If N = ϕ(R) does a forward move N N , then by Lemma 30, we have R R and ϕ(R ) = N .

Concurrency and Causal Consistency

This section contains proofs and further technical material of Section 3.1.

To fit the framework of [31], we re-formulate our framework as a labelled transition system enriched with an independence relation (LTSI) [44,Definition 3.7].

Definition 31. A labelled transition system (LTS) is a structure (R, L, -→), where R is a set of systems, L is the set of action labels and -→⊂ R × L × R is a transition relation.

Definition 32. A labelled transition system with independence (LTSI) is a structure (R, L, -→, ι), where (R, L, -→) is an LTS and ι is the independence relation (an irreflexive symmetric binary relation on transitions).

In our case, R is the set of configurations and L the set of labels of our transitions. The latter include both forward and backward transitions. Also, the notion of independence is defined on coinitial transitions and it coincides with the notion of concurrency, namely ι = c .

In the following we prove Loop Lemma, property stating that each transition is reversible.

Lemma 14 (Loop Lemma). For every reachable configuration R and forward transition t : R µ R , there exists a backward transition t • : R µ R and vice versa.

Proof. The proof follows from the fact that forward and backward rules are symmetric. Let us assume that there is forward transition t : R µ R . We proceed by the induction on the derivation of transition t.

if transition t is obtained by applying rule (F-Scm-Act); then we have

where in memory µ, there is a corresponding operation structure T [j 1 : • 1 , . . . , j m : • m ], we can apply the rule (B-Scm-Act) and obtain R µ R, as desired. if transition t is obtained by applying rule (F-Scm-Opn); then we have systems R =

Now, on the system R , we can apply rule (B-Scm-Opn) with premise R i µi R i and we obtain R µi R, as desired. if transition t is obtained by applying rule (F-Eqv); then we have

Let us assume that there is a backward transition t • : R µ R . We proceed by the induction on the derivation of transition t • .

if transition t • is obtained by applying rule (B-Scm-Act); then on the reachable system

we can apply rule (B-Scm-Act) and restore the system R from the memory µ.

On the system R = k 1 : P 1 | . . . | k n : P n , we can apply rule (F-Scm-Act). Since we are limited to reachable processes, by choosing fresh keys j 1 , . . . , j m , we have transition

if transition t • is obtained by applying rule (B-Eqv); then we have R µ R with premises

Systems R and R i are reachable and by inductive hypothesis,

We proceed by showing the Square Property, stating that two concurrent transitions can be executed in any order.

Property 1. Square Property (SP) holds for each instance of our framework.

Proof. Transitions t 1 and t 2 are coinitial and concurrent, hence from Definition 13, we have key(µ 1 ) ∩ key(µ 2 ) = ∅. From Definition 13 and the memory construction and creation we can notice that the only possibility for two transitions to execute concurrently, is if they involve different entities of the system. Therefore, coinitial transitions t 1 and t 2 are executed on different entities of a system R. As a consequence, entities produced or consumed by transition t 1 do not affect the execution of transition t 2 and vice versa.

In particular, we proceed with the induction on the structure of the process R. As a base case, we shall write process R as a parallel composition of two systems R 1 and R 2 such that t 1 involves entities inside system R 1 , while t 2 consumes entities belonging to system R 2 . Then, we have:

Now from processes R and R , we can have transitions t 2 /t 1 and t 1 /t 2 , respectively.

In the inductive case, we consider a system R 1 and we have two possibilities: R = R 1 | S, where system R 1 is a part of a larger system or we can have operation defined on the system R 1 , i.e. R = op n (R 1 ). Both cases follow by application of rule (F-Scm-Opn) or (B-Scm-Opn) depending whether transitions are forward or backward. Now we prove that our framework satisfies properties (BTI) and (WF).

Property 2. Axiom stating that backward transition are independent (BTI) holds for each instance of our framework.

Proof. Let us suppose that transitions t 1 and t 2 are in conflict. Then by Definition 13, we have that exists a key k such that k ∈ key(µ 1 ) ∩ key(µ 2 ). Since

we have the following possibilities:

∩ key(C 1 ); this case is in the contradiction with the fact that transitions t 1 and t 2 are coinitial (k ∈ key(R 1 ) ∩ key(C 2 ) represents the situation in which transition t 2 can be fired only if transition t 1 is already executed). k ∈ key(R 1 ) ∩ key(R 2 ); this case is impossible since the system R is reachable. Having k ∈ key(R 1 ) ∩ key(R 2 ) would imply that system R has two memories µ 1 and µ 2 created by actions involving the same entity P identified with key k. This cannot be the case, since by design of the framework, when having a system k : P , entity P does not have a parallel composition as the top-level operator. k ∈ key(C 1 ) ∩ key(C 2 ); this case is in contradiction with the fact that system R is reachable and that keys produced by transitions are fresh. We can conclude that transitions t 1 and t 2 are concurrent, as desired.

Property 3. Well-foundedness axiom (WF) holds for each instance of our framework.

Proof. This property follows from the fact that backward transitions consume memory.

Proposition 20. Axioms SP, BTI, WF, CPI and CIRE hold for each instance of our framework.

Proof. The proof that (SP), (BTI) and (WF) hold for each instance of our framework is a direct consequence of Properties 1, 2 and 3, respectively. Regarding axioms (CPI) and (CIRE), the proof follows from [31, Proposition 5.4] and the fact that in LTSI (R, L, -→, c ) the notion of concurrency (relation c ) is defined purely on the labels of transitions.

Given that our reversible semantics satisfies all basic axioms (Proposition 20), thanks to [31], all instances of our framework satisfy the Parabolic Lemma and Causal Consistency.

Lemma 33. The LTSI (R, L, -→, c ) satisfies Parabolic Lemma.

Proof. The proof follows from [31, Proposition 3.4] and Proposition 20 (in particular, by using Properties 1 (Square Property) and 2 (BTI)).

Lemma 34. The LTSI (R, L, -→, c ) satisfies Causal Consistency.

Proof. The proof follows from [31, Proposition 3.6] and Proposition 20 (in particular, by using Property 3 (Well-foundedness) and Lemma 33 (Parabolic Lemma)).

where µ = κ : a P | κ : a(X) P , operation structure T

. . , j m } and δ l = j l , j • t for l ∈ {1, . . . , m} By applying encoding function • on R , we have M ≡ M = R . F-Res then R = νa R 1 and we have νa R 1 νa R 1 with premise R 1 R 1 . When applying encoding function to systems R, we have

By inductive hypothesis we have R 1

M 1 with M 1 ≡ R 1 and we can apply the rule (R.Ctx) on configuration M , then we have

We can apply the rule (R.Eqv) on process M = R . The thesis follows from the fact that encoding function

• preserves structural congruence. Now we separate two cases depending whether process P {P/X} has a parallel operator on the top-level, or not.

• If process P {P/X} does not have a parallel operator on the top-level, then P {P/X} = νã Q 1 . In this case configuration M is

For configuration M there is a normal form

In our reversible HOπ, with premise a P | a(X) P P {P/X} where P {P/X} = νã Q 1 , we can apply rule (F-Act) on process R as:

Now for k = j 1 we have R = M ≡ M , as desired.

• If process P {P/X} has a parallel operator on the top-level, then

For configuration M there is a normal form

where j = {j 1 , . . . , j m }.

In our reversible HOπ, with premise a P | a(X) P P {P/X} where P {P/X} ≡ νã

, we can apply rule (F-Act) on system R, and we obtain:

Now R = M ≡ M as desired. R.Ctx the proof follows by case analysis on the structure of the context.

• empty context; in this case the rule (R.Fw) is applied.

• context is restriction; then we have the system R = νa R 1 and its encoding into ρπ,

, and we can apply rule (F-Res) on system R and obtain a system

By applying encoding function on systems R and R 1 , we obtain configurations M and

where keys k , k and k i are translated into tags κ , κ and κ i for i ∈ {1, . . . , n}. Symbol ũ represents the restricted names b and new keys generated while translating system R.

Past states S j are encoded into ρπ past states µ j and contexts C j are substituted with keys t j . In ρπ we have M M with premise M 1 M 1 , where

By inductive hypothesis, there is transition in reversible HOπ R 1 R 1 with R 1 ≡ M 1 . Now we separate two cases depending whether process P {P/X} has a parallel operator on the top-level or not.

• If process P {P/X} does not have a parallel operator on the top-level, then

It can be extended to the relation l as δ( l ) = →.

Lemma 47. For each transition L l L , there is a transition δ(L) → δ(L ) with δ( l ) = →.

Proof. By induction on the derivation L l L .

Lemma 48. For each transition E → E and for all reachable L such that δ(L) = E, there is a transition L l L with δ(L ) = E and δ( l ) = →.

Proof. By induction on the derivation E → E .

Property 5. For each forward Erlang system E there is a reversible logging system L such that δ(L) = E and L has no backward moves (L is initial process, i.e. L = L i ).

In the following, we give the definition of the erasing function λ(•) which given a reversible system R, generates the simple forward Erlang system E, by deleting past information.

Definition 49. The erasing function λ : R -→ E that maps our reversible system to the forward Erlang system is defined as:

Proof. By induction on the derivation R R .

Lemma 51. For each transition E → E and for all reachable R such that λ(R) = E, there is a transition R R with λ(R ) = E .

Proof. By induction on the derivation E → E .

Property 6. For every forward Erlang system E there is a reversible system R such that λ(R) = E and R has no backward moves (R is an initial system).

In what follows we show that the reversible logging semantics of Erlang and our reversible semantics of Erlang are strong back and forth barbed bisimilar. (Definition 26).

Lemma 52. Given two initial systems L i and R i if δ(L i ) = λ(R i ) then L i and R i are strong back and forth barbed bisimilar.

Proof. We show that R is a strong back and forth barbed simulation, to prove the same result for R -1 is similar. We define the relation R as:

. Now we have to show that R is a strong back and forth barbed equivalence.

Before starting with the proof, we state a few properties of R that we will need: (i) (L, R) ∈ R implies δ(L) = λ(R) (while the opposite might not hold). This property follows from the definition.

The derivation of (L, R) ∈ R is based on two computations of the same length (possibly 0)

From the fact that for every system exists a unique initial system, we have

Now we proceed with the proof of the barbed equivalence. Having an Erlang system E, by Properties 5 and 6, there exist systems L and R such that δ(L) = E = λ(R). By definitions of the erasing functions δ(•) and λ(•) we have that the systems E, L and R have the same barbs.

Let us assume that (L, R) ∈ R and L l L . Thanks to Lemma 47, we have δ(L) → δ(L ) with δ( l ) = →. From the property (i) given above, we have LRR implies δ(L) = λ(R). Now, from δ(L) → δ(L ) and δ(L) = λ(R), by Lemma 51, we have that there exists a transition R R such that λ(R ) = δ(L ). By definition of R we can conclude that (L , R ) ∈ R.

Let us assume now (L, R) ∈ R and L l L . We consider the initial reversible logging system L i and computation L i * L ensuring (L, R) ∈ R. Now, let us consider the computations L i * L l L and L i * L . By the Causal Consistency (Definition 22) we have that two computations differ only for commuting concurrent actions and simplifying reverse actions. Therefore, the backward action L l L can be simplified only with a corresponding forward action in L i * L which commutes with every action after it until it becomes the last one. Then we have the computation L i * L l L. On the other side, from property (ii), given above, we have (L, R) ∈ R implies (L i , R i ) ∈ R. In our reversible semantics, we consider the corresponding initial system R i and computation R i -→ * R ensuring (L, R) ∈ R. Now we can apply the same reasoning as in the reversible logging semantics, since commuting squares are preserved and reflected by functions δ() and λ(). Therefore, we get the computation R i -→ * R R, ensuring that (L , R ) ∈ R. Then by Loop Lemma (Lemma 14) we have R R as desired.

Theorem 27. The reversible semantics of Erlang in [29] and our reversible semantics of Erlang are strong back and forth barbed bisimilar.

Proof. We have to show that for every system in the reversible logging semantics there is a strong back and forth barbed bisimilar system in our reversible semantics and vice versa. We consider a system L, its initial system L i and translation of L i into Erlang, i.e. δ(L i ). Thanks to Property 6 there exists a system R 1 in our semantics, such that λ(R 1 ) = δ(L i ) and R 1 has no backward moves. This implies that R 1 is an initial system and we can denote it as R i , therefore, we have λ(R i ) = δ(L i ). Thanks to Lemma 52, L i and R i are strong back and forth barbed bisimilar. Since L i * L, there exists a system R such that R i -→ * R and L and R are strong back and forth barbed bisimilar. The proof is similar if we start from systems R and R i of our reversible semantics for Erlang.

A.6 Reversible link semantics for Erlang

In this section we give the additional rules of the reversible link semantics for Erlang (Section 4.3), namely system rule (F-Nrm) as well as rules describing the evaluation of functions spawn_link() and process_flag(). In rule (Flag), f is a Boolean value. --------------→ θ, κ (Flag) θ, process_flag(trap_exit, f ) process_flag(κ,trap_exit,f )

-------------------→ θ, κ