Ivan Lanese
email: ivan.lanese@gmail.com

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

A General Approach to Derive Uncontrolled Reversible Semantics

Keywords: 2012 ACM Subject Classification Theory of computation → Concurrency; Computing methodologies → Concurrent computing methodologies Reversible computing, causality, process calculi, Erlang Digital Object Identifier 10.4230/LIPIcs.CONCUR.2020.33

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 [START_REF] Landauer | Irreversibility and heat generation in the computing process[END_REF]. Beyond obtaining computing machinery with low heat dissipation, reversible computing found its application in a wide range of fields, from biochemical modelling [START_REF] Cardelli | Reversible structures[END_REF][START_REF] Danos | Formal molecular biology done in CCS-R[END_REF][START_REF] Kuhn | Local reversibility in a calculus of covalent bonding[END_REF][START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF] to simulation [START_REF] Carothers | Efficient optimistic parallel simulations using reverse computation[END_REF], robotics [START_REF] Sund Laursen | Automatic error recovery in robot assembly operations using reverse execution[END_REF], programming [START_REF] Lutz | Janus: a time-reversible language[END_REF][START_REF] Ulrik | Reversible object-oriented programming with region-based memory management -work-in-progress report[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF] and program debugging [START_REF] Boothe | Efficient algorithms for bidirectional debugging[END_REF][START_REF] Giachino | Causal-consistent reversible debugging[END_REF][START_REF] Mcnellis | Time travel debugging: Root causing bugs in commercial scale software[END_REF][START_REF] Lanese | Cauder: A causal-consistent reversible debugger for Erlang[END_REF]. 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 [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Iain | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF], Petri Nets [START_REF] Philippou | Reversible computation in Petri nets[END_REF][START_REF] Hernán | Reversing P/T nets[END_REF], event structures [START_REF] Ulidowski | Reversing event structures[END_REF], 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 [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Iain | Reversing algebraic process calculi[END_REF][START_REF] Lanese | Causal-consistent reversibility[END_REF], 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 [START_REF] Danos | Reversible communicating systems[END_REF]. 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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], 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 [START_REF] Iain | Reversing algebraic process calculi[END_REF], which considers process calculi defined in a specific SOS format [START_REF] Plotkin | A structural approach to operational semantics[END_REF]. Differently from [START_REF] Iain | Reversing algebraic process calculi[END_REF], 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 [START_REF] Iain | Reversing algebraic process calculi[END_REF]. This is the case for both our case studies, namely higher-order π [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] and Core Erlang [START_REF] Carlsson | Core Erlang 1.0.3. Language specification[END_REF].

Given a forward-only system, we aim at building its uncontrolled [START_REF] Lanese | Causal-consistent reversibility[END_REF] 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 [START_REF] Danos | Transactions in RCCS[END_REF][START_REF] Lanese | Controlling reversibility in higher-order pi[END_REF][START_REF] Bacci | On the statistical thermodynamics of reversible communicating processes[END_REF][START_REF] Lanese | Controlled reversibility and compensations[END_REF].

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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], which consists in showing that the system satisfies a few basic axioms.

To show the generality of our method, we apply it to two case studies: higher-order π-calculus [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] (used as a running example) and Core Erlang [START_REF] Carlsson | Core Erlang 1.0.3. Language specification[END_REF] (Section 4.2). After obtaining the corresponding reversible models, we show that, while syntactically different, they have the same behaviour as the ones in the literature [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF][START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]. We also show how our approach can be used to go further than what it is in the literature. As an example, we extend reversible Core Erlang to also support Core Erlang constructs for remote error handling based on links (Section 4.3). Such an extension has never been considered in the reversibility literature.

Due to space limitations, further details are in the Appendix while proofs are in [START_REF] Lanese | A general approach to derive uncontrolled reversible semantics (TR)[END_REF].

Our Approach

In this section we formally introduce our approach. We first define the constraints that the forward-only model we take in input needs to satisfy, and then we describe how to derive the syntax and semantics of the corresponding causal-consistent reversible model.

To give a better intuition about our approach, we will use as a running example its instantiation on the asynchronous Higher-Order π-calculus [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF].

Forward model

We assume a forward model equipped with a reduction semantics. The syntax of the forward model is structured in two levels. The lower level is composed by entities, e.g., processes, messages and resources, ranged over by P, Q. There are no restrictions on the syntax of the lower level. The upper level needs to follow the structure below:

N ::= P | op n (N 1 , . . . , N n ) | 0
Essentially, a system is obtained by composing entities using composition operators op n , where n is the operator arity. Among the composition operators we assume a binary parallel composition operator, thus N 1 | N 2 represents the parallel composition of two systems. Additionally, 0 represents the empty system. Notably, 0 is not an entity.

Below we recall the syntax of HOπ-calculus and show how it fits in our framework.

Example 1. The classical syntax of HOπ-calculus [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] 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.

C O N C U R
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.

(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.

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:

C O N C U R
(F-Eqv) R ≡ R R R1 R1 ≡ R 1 R R 1
Figure 2 Forward rules of the uncontrolled reversible semantics.

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

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. -→= ∪ ).

Example 9. 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. 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 ; 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 term

T [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.

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 [START_REF] Danos | Reversible communicating systems[END_REF].

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. 2 and3.

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

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).

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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], 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, [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF] 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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF] necessary to show Causal Consistency, Safety and Liveness.

First, we re-formulate our framework as a Labelled Transition System with Independence (LTSI, see also [START_REF] Vladimiro Sassone | Models of concurrency: Towards a classification[END_REF]) (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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF] is that each action is reversible, as shown by the following result. 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 [START_REF] Danos | Reversible communicating systems[END_REF], 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.

-→ 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. Given that our reversible semantics satisfies all the axioms, thanks to [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], all instances of our framework satisfy the Parabolic Lemma, Causal Consistency, Causal Safety and Causal Liveness, defined below. Below, we state Causal Safety and Causal Liveness. We present them in a slightly rephrased and more intuitive form w.r.t. [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], whose presentation is however more formal.

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 ,

Definition 23 (Causal Safety (CS) and Causal Liveness (CL)).

Let L = (R, L, -→, c ) be a LTSI satisfying SP,BTI,WF and CPI. Take a derivation R

µ -→ 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 . C O N C U R

Case Studies

In this section we apply our approach to two relevant case studies from the literature, the Higher-Order π-calculus [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] and Core Erlang [START_REF] Carlsson | Core Erlang 1.0.3. Language specification[END_REF]. Causal-consistent reversible semantics for both of them are available in the literature [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF]. 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF]. 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF]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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF], 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF] 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. 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] Carlsson | Core Erlang 1.0.3. Language specification[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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]. As a forward model, we use the logging semantics of Core Erlang [30, Figure 14] (used also in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]) with some minor changes: we use floating messages, as in [START_REF] Lanese | Models, Languages, and Tools for Concurrent and Distributed Programming -Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday[END_REF], instead of a global mailbox Γ and we omit the labels of the relation →. Indeed, labels are used in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] to log the steps of the computation so to be able to replay it from logs [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF][START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]. 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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF], 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 for the others. Since evaluation of expressions is not central for us, we refer to [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] 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. 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 of Appendix A. 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. 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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]. 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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF], 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF]. Here we just discuss the idea, we refer to Appendix A for the technical details.

The notion of conflict for reversible Core Erlang in [30, Definition 12] (which is an instance of the happened-before relation [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] as discussed in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]) 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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]Definition 12] iff they are in conflict according to Definition 13.

We show below that the reversible semantics of Erlang in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] and ours are strong back and forth barbed equivalent [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF]. We let E to stand for a Core Erlang system, L for a reversible Erlang system as in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] and R for one of our reversible Erlang configurations.

Following [START_REF] Lanese | Models, Languages, and Tools for Concurrent and Distributed Programming -Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday[END_REF], 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF] 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: Theorem 27. The reversible semantics of Erlang in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] and our reversible semantics of Erlang are strong back and forth barbed bisimilar.

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 [START_REF] Armstrong | Erlang -software for a concurrent world[END_REF].

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 [30, 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.

C O N C U R 2 0 2 0

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. 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.
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. 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, ---------------→ θ , e p is a fresh pid k1, k2 are fresh keys

k : 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 : •2] (F-Flag)
θ, e process_flag(κ,trap_exit,f )

-------------------→ θ , e k1 is a fresh key 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.

k : p, θ, e, l, f k1 : p, θ , e {κ → f }, l, f | [k : p, θ, e, l, f ; k1 : •1] (F-Err) l = {p1, . . . , pm} 1 ≤ i ≤ n ⇒ fi = true ∧ n + 1 ≤ i ≤ m ⇒ fi = false h,
It can be set to the desired value using rule (F-Flag).

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 [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]Figure 11]. Two main changes are needed. First, evaluation of operators may produce either a value or an error: 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.

We are working to integrate the error mechanisms above into Erlang reversible debugger CauDEr [START_REF] Lanese | Cauder: A causal-consistent reversible debugger for Erlang[END_REF]. CauDEr follows the reversible semantics of Core Erlang in [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF], 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 [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF][START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF]. As an illustration that our approach can go beyond the literature, we tackled Core Erlang constructs for remote error handling based on links.

C O N C U R 2 0 2 0

33:16 A General Approach to Derive Uncontrolled Reversible Semantics

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., [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Cristescu | A compositional semantics for the reversible pi-calculus[END_REF][START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF][START_REF] Mezzina | Causally consistent reversible choreographies: a monitors-as-memories approach[END_REF][START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF][START_REF] Antares | On reversibility and broadcast[END_REF][START_REF] Barylska | Reversing transitions in bounded Petri nets[END_REF][START_REF] Graversen | Event structure semantics of (controlled) reversible CCS[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF][START_REF] Hernán | Reversing P/T nets[END_REF]). Indeed, our work can be seen as a generalisation of [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF], 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 [START_REF] Iain | Reversing algebraic process calculi[END_REF], 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 [START_REF] Iain | Reversing algebraic process calculi[END_REF] cannot cope with our two case studies, Higher-Order π-calculus and Core Erlang, since they do not fit their SOS format. Also [START_REF] Bernadet | A modular formalization of reversibility for concurrent models and languages[END_REF], 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 [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF]. 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 [START_REF] Lanese | Controlled reversibility and compensations[END_REF] such as irreversible actions [START_REF] Danos | Transactions in RCCS[END_REF], rollback operators [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF] or energy potentials [START_REF] Bacci | On the statistical thermodynamics of reversible communicating processes[END_REF]. An interesting line for future work is to integrate such approaches in our framework. For rollback, we could follow the ideas in [START_REF] Lanese | From reversible semantics to reversible debugging[END_REF], 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 [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF], since its concurrency model includes read dependencies. In particular, our approach is based on consumed and produced resources, while in [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF] 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 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] (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.

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

(R, N ) ∈ R: if R R , then N N with (R , N ) ∈ R; if N N , then R R with (R , N ) ∈ R.

Strong bisimilarity is the largest strong bisimulation.

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

Concurrency and Causal Consistency.

To fit the framework of [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], we re-formulate our framework as a labelled transition system enriched with an independence relation (LTSI) [ 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 .

Given that our reversible semantics satisfies all the required axioms (Proposition 20), thanks to [START_REF] Lanese | An axiomatic approach to reversible computation[END_REF], all instances of our framework satisfy the Parabolic Lemma, Causal Consistency, Causal Safety and Causal Liveness.

Correspondence between our reversible HOπ and ρπ

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

In the following, we recall the definition of thread normal form from [26, 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 32 (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
We now present an encoding from our reversible HOπ to ρπ. The encoding works in two steps: a first step explores memories in our configurations to find related sets of keys, the second step uses the gathered information to actually perform the translation. The first step is done by function col(R), which computes (possibly annotated) sets of keys, one for each memory [R ; C] in R. 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 possibly annotated 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 configuration 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 ρπ [START_REF] Lanese | Reversibility in the higherorder π-calculus[END_REF] configurations in normal form and with R the set of all configurations obtained by applying our approach to the HOπ-calculus. The encoding function • : R -→ M, is defined as:

R = νK R col(R)
where K = ( 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.

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 = [
The first two deal with keys labelling 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. 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 ).

Classic and reversible semantics for Core Erlang

This section recalls a reduction semantics for Core Erlang [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] 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. Rule (Spawn) adds a new process with a fresh pid p , initialised with an empty environment id, into the system. 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. We refer to [START_REF] Lanese | Causal-consistent replay debugging for message passing programs[END_REF] for a detailed description of the rules.

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.

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.

2 0 2 0 33 : 4 AFigure 1

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

(

  F-Act) a P | a(X) P P {P/X} 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]] (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

Definition 21 (

 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)). Given two coinitial derivations d 1 and d 2 , d 1 ∼ d 2 if and only if d 1 and d 2 are cofinal.

2 0 2 0 33 : 10 A

 3310 General Approach to Derive Uncontrolled Reversible Semantics 4

  ---→ θ , 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 : •2] (F-Rec) θ, e rec(κ,cln) ------→ θ , 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, v) | k : p, θ, e

  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.

  spawn_link(κ,f /n,[vn])

Figure 4

 4 Figure 4Forward rules of the reversible link semantics for Erlang.

  , v1, . . . , vn) = x with x = v ∨ x = r θ, call op(v1, . . . , vn) τ -→ θ, x

Definition 29 .

 29 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 30. 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).

Proposition 31 .

 31 For every instance of our framework, the LTSI (R, L, -→, c ) satisfies the Parabolic Lemma, Causal Consistency, Causal Safety and Causal Liveness.

22 AFigure 6

 226 Figure 6 Function col().

Example 33 .Figure 7

 337 Figure 7 System rules of standard Core Erlang.

2 0 2 0 33:6 A General Approach to Derive Uncontrolled Reversible Semantics

			P1 | . . . | Pn	T [Q1, . . . , Qm]	j1, . . . , jm are fresh keys
	(F-Scm-Act)	k1 : P1 | . . . | kn : Pn	T [j1 : Q1, . . . , jm : Qm] | [k1 : P1 | . . . | kn : Pn ; T [j1 : •1, . . . , jm : •m]]
		Ri	R i (key(R i ) \ key(Ri)) ∩ (key(R0, . . . , Ri-1, Ri+1, . . . , Rn) = ∅
	(F-Scm-Opn)		opn(R0, . . . , Ri, . . . , Rn)	opn(R0, . . . , R i , . . . , Rn)

  Lemma 14 (Loop Lemma). For every reachable configuration R and forward transitionFrom now on we denote with t • the reverse of t. The basic properties required to show causal consistency are as follows.

	t : R
	Definition 15 (Basic axioms).
	Square Property (SP): if t 1 : R transitions, there exist two cofinal transitions t 2 /t 1 : R µ1 µ2 -→ R are two coinitial independent -→ R and t 2 : R µ2 -→ R and t 1 /t 2 : R µ1 -→ R .
	Backward transitions are independent (BTI): any two coinitial backward transitions t 1 :
	R

µ R , there exists a backward transition t • : R µ R and vice versa. µ1 R 1 and t 2 : R µ2 R 2 where t 1 = t 2 are independent. Well-foundedness (WF): there is no infinite backward computation.

  Definition 16 (Causal equivalence). Causal equivalence, ∼, is the least equivalence relation between derivations closed under composition satisfyingt 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). 17 (Coinitial propagation of independence (CPI)). If whenever t 1 : R 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

µ1 -→ R , t 2 : R µ2 -→ R , t 2 : R µ2 -→ R and t 1 : R µ1 -→ 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

  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 . 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.

Vincent Danos, Jean Krivine, and Paweł Sobociński. General reversibility. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, pages 75-86, 2006. doi:10.1016/j.entcs.2006.07.036.

Rolf Drechsler and Robert Wille. From truth tables to programming languages: Progress in the design of reversible circuits. In IEEE International Symposium on Multiple-Valued Logic, ISMVL, pages 78-85, 2011. doi:10.1109/ISMVL.2011.40.

Erlang website. https://www.erlang.org/. C O N C U R 2 0 2 0

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

A Further Technical Material Higher-Order π-calculus and reversible HOπ-calculus

This section recalls the semantics of the HOπ-calculus [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF], 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:

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. Rule (Alpha) is α-conversion while rule (ResF) deals with scope extrusion. The semantics of HOπ is given by the reduction relation below:

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.

Figure 5 Forward and backward rules of the reversible semantics for the Higher-Order π-calculus.

Properties

This section contains further technical material related to Section 3. We start by defining strong bisimilarity between the forward semantics of a reversible configuration R and the semantics of its projection on the original model ϕ(R). (F-Nrm) ---------------→ θ, κ (Flag) θ, process_flag(trap_exit, f ) process_flag(κ,trap_exit,f )

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


Doriana Medić

Claudio Antares Mezzina

Iain Phillips

Nobuko Yoshida

Towards a formal account for software transactional memory

Keywords: STM, Transactions, Concurrency

Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.

Introduction

Starting from the 1960s, reversible computing has been studied in several contexts ranging from quantum computing [START_REF] Grattage | A functional quantum programming language[END_REF], biochemical modelling [START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF], programming [START_REF] Lutz | Janus: a time-reversible language[END_REF][START_REF] Yokoyama | Principles of a reversible programming language[END_REF], and program debugging [START_REF] Giachino | Causal-Consistent Reversible Debugging[END_REF][START_REF] Lanese | Cauder: A causal-consistent reversible debugger for Erlang[END_REF]. Distributed reversible actions can be seen as defeasible partial agreements: the building blocks for different transactional models and recovery techniques. The work of Danos and Krivine on reversible CCS (RCCS) [START_REF] Danos | Transactions in RCCS[END_REF] provides a good example: they show how notions of reversible and irreversible actions in a process calculus can model a primitive form of transaction, an abstraction that has been found useful, in different guises, in reliable concurrent and distributed programming. Since the seminal work of [START_REF] Danos | Transactions in RCCS[END_REF], other works have investigated the interplay between transactions and reversibility [START_REF] Lanese | Concurrent Flexible Reversibility[END_REF][START_REF] Vries | Communicating Transactions[END_REF] in the area of message passing systems. On the shared memory side, we just recall the work of [START_REF] Acciai | A Concurrent Calculus with Atomic Transactions[END_REF] where a CCS endowed with a mechanism for software transactional memories (STMs) is presented. Another work about reversibility and a high-level abstraction of shared memory (tuple spaces) is presented in [START_REF] Giachino | Causal-consistent rollback in a tuple-based language[END_REF].

Software Transactional Memory [START_REF] Herlihy | Transactional Memory: Architectural Support for Lock-Free Data Structures[END_REF][START_REF] Shavit | Software transactional memory[END_REF] is an elegant way to address the problem of concurrent programming, by relieving the programmer from the burden of dealing with locks. The lock-based approach is error prone and usually leads to deadlocks when the complexity of the system grows. Opposite to the lock-based approach, STM uses transactions. A transaction is a block of code accessing shared data which is meant to be executed atomically with an "all or nothing" policy: that is either all the effects of a transaction have to be visible when it commits, or none of them has to be visible in case of abortion. This abstraction allows for multiple transactions to be executed "at the same time". The programmer just needs to specify the sequences of operations to be enclosed in transactions, while the system is in charge of the interleaving between the concurrent transactions. A transaction can either commit and update the system permanently or abort and discard all the changes done by its execution.

In this work, we are interested in the interplay between reversible computing and the STM approach to control the concurrent executions. Therefore, we present a formal framework for describing STMs in a simple shared memory context. In particular, when a transaction aborts, it is necessary to discard all the updates that it made and we need to bring the system back to the state before the execution of the transaction. To accomplish the behaviour above, we implement a rollback operator following the approach given in [START_REF] Lanese | Controlling Reversibility in Higher-Order Pi[END_REF]. A transaction can access a shared variable either in read or in write mode. Given this, different policies can be used to regulate the transactions which are accessing the same value in the shared memory. According to the implemented policy, some transactions will succeed and some will be aborted. We will show how it is possible to model writer and reader preference [START_REF] Courtois | Concurrent Control with "Readers" and "Writers[END_REF] in our framework. Consider the following C-like code where two functions/threads access the same shared variables:

int x = 0 ; int y = 5 ; int z = 0 ; void t 1 ( ) { z = y+x ; } void t 2 ( ) { x = z +1; } t 1 ; t 2 t 2 ; t 1 t 1 | t 2 z = 5 z = 6 z = 5 x = 6 x = 1 x = 1
All the possible executions of the two functions are reported above: either the two functions are executed sequentially or are interleaved (leading to an unwanted state). If we wrap the two functions into two atomic blocks then the third behaviour would be automatically ruled out by the system as one of the two transactions will be aborted depending on the implemented policy.

Syntax

In this section we give the syntax of our calculus. Let us assume the existence of the mutually disjoint sets V (a set of variables) and I (a set of transaction identifiers), ranged over by x, y, z and t, h, respectively. The syntax of the calculus is given in Figure 1. Write and read access to the variable x are represented with actions wr(x) and rd(x). The sequential execution of the actions wr(x) and rd(x) together with the choice operator + build the processes, given with A, B productions. The term t : A Γ represents a transaction, where t is a unique identifier, A is the body of the transaction and Γ is the set recording the identifiers of the transactions which have the write access to the variable that transaction t has to read. The idea behind the set Γ is to allow transaction t to have read access to any variable, but to record the write access to them. In this way if the transaction that writes on the variable fails, the transaction that reads the same variable has to fail too. More explanations will be given in Section 3.

Transactions, together with processes, build expressions. An expression can be prefixed with the actions wr(x) and rd(x) and we denote it as α.X. Two expressions X and Y can be executed in parallel, X | Y , or in sequential order X; Y . We can note that the expression X can be the process that is not inside of the transaction, and that operation ; allows us to have a transaction followed by an action (for example t : A Γ ; wr(x)). The whole system, called configuration, is denoted with C and it represents the expressions together with the shared memory. The shared memory M is made of triples of the form x, W, R for every variable in the system. In x, W, R , x is the variable name, W and R are the sets recording transactions which had write and read access to x, respectively. Let us note that we abstract away from the value contained by variables, since this is not relevant for our framework. We just need to record whether a variable is read (a transaction reads its value) or modified (a transaction changes its value).

In order to write expressions in a more compact way, we define the notion of history context. For instance, having a transaction t : wr(x).rd(x 1 )rd(y).A + B Γ we can write it as t : H[rd(x 1 )rd(y).A] Γ where H = wr(x). • +B. Formally: Definition 1 (History context). A history context H is a process with a hole •, defined by the following grammar:

H ::= • | α. • +A.

Semantics

The semantics of our calculus is presented in two steps. First, we give the basic rules of the framework (common to all the policies) and then, we present the extra rules, necessary to model reader or writer preference. With reader preference, we intend that reading the value of a variable is always possible, i.e. no read access should be suspended, unless the write access already took place. Writer preference, on the other side, allows the write access to the value of a variable x even if some read access already took place. In this case, all the executing transactions with the read access to a value x need to be aborted and brought back to their initial state.

In what follows we provide the auxiliary functions necessary for the semantics of the calculus: the function which computes the set of the transaction identifiers of a given expression and the operation which removes transaction identifiers from the system. Definition 2 (Set of the transaction identifiers). The set of the transaction identifiers of a given expression X, written id(X), is inductively defined as:

id(Y | Y ) = id(Y ) ∪ id(Y ) id(α.Y ) = id(Y ) id(A) = ∅ id(Y ; Y ) = id(Y ) ∪ id(Y ) id(t : A Γ ) = {t}
Definition 3 (Removing of identifiers). The operation of deleting transaction identifier t from the configuration C, denoted as C @t , is defined as follows:

(X M ) @t = X @t M @t (α.X) @t = α.(X @t ) (X | Y ) @t = X @t | Y @t (t : A Γ ) @t = t : A Γ \t (X; Y ) @t = X @t ; Y @t ( x, W, R M ) @t = x, W \ t, R \ t M @t
When a transaction fails, the effects of the internal computation are undone and the entire transaction is restarted, that is, brought back to its initial state. As a consequence, the transactions depending on it are also rolled back. Dependency between transactions changes with the chosen preference. We shall see more information about the preferences by the end of this section.

To be able to identify the state of the internal computation of a transaction, we mark it with symbol ∧ . For instance, if we consider transaction t : rd(x).rd(y). ∧ wr(z).wr(x ) Γ , the actions rd(x) and rd(y) represent the past of the transaction and the action wr(z) is the next action to be executed. Now we define our rollback operator which brings a transaction back to its initial state i.e. the symbol ∧ is placed in the beginning of the transaction and its set Γ is empty. For instance, if we roll back transaction t : rd(x).rd(y). ∧ wr(z).wr(x ) Γ , we obtain t : ∧ rd(x).rd(y).wr(z).wr(x ) ∅ . Formally, we have: Definition 4 (Rollback operator). The rollback operator on the transaction t : A Γ , written roll(t), is defined as:

roll(t) = t : ∧ A ∅ .
In what follows, we give the semantics of our calculus. We shall start by introducing semantics rules representing the base of our framework (rules that are common for both models) and then we show the additional rules for each preference.

The common rules are given in Figure 2. An action executed outside a transaction can be seen as an atomic step in which the action is discarded after the (WriteP) wr(x).A + B x, ∅, ∅ → A x, ∅, ∅ (ReadP) rd(x).A + B x, ∅, ∅ → A x, ∅, ∅ (Write)

(W ⊆ {t} ∧ R ⊆ {t}) t : H[ ∧ wr(x).A + B] Γ x, W, R M → t : H[wr(x). ∧ A + B] Γ x, W ∪ t, R M (Read) t : H[ ∧ rd(x).A + B] Γ x, W, R M → t : H[rd(x). ∧ A + B] Γ ∪(W \t) x, W, R ∪ t M (Par) X M → X M id(X) ∩ id(Y ) = ∅ X | Y M → X | Y M (Commit) t : A ∧ Γ ; Y | X M ∧ Γ = ∅ t : A ∧ Γ ; Y | X M → Y | X @t M @t (RollR) t : A Γ M → roll(t) M @t ∀ti ti : Ai Γ i ∪{t} t : A Γ | i ti : Ai Γ i M → roll(t) | i roll(ti) (M @t ) @t i
Fig. 2. Common rules for both models execution (rules WriteP and ReadP). Therefore, there is no need to keep track of its access to the variable. The only constraint is that they cannot access the variable while some transaction has read or write access to it. Rule Write describes when a transaction can modify the content of a variable. To do so, there should not be another transaction which has already accessed the variable in either writing or reading mode. After the execution, the identifier t is added to the write access set W of the variable x and the symbol ∧ is moved to the next computational step. Rule Read allows the transaction t to execute the action rd(x) at any moment. Then the identifier t is added to the set R of the variable x and the set W \ t is added to the set Γ (if write and read access to the variable x are in the same transaction t, then it is not necessary to save the identifier t into a set Γ ).

To have a better intuition about these two rules, we give a simple example. Consider the transaction t with a corresponding shared memory t : ∧ wr(x).rd(y) ∅

x, ∅, ∅ y, ∅, ∅

After executing the write access to the variable x, we obtain the system

t : wr(x). ∧ rd(y) ∅ x, {t}, ∅ y, ∅, ∅
where the pointer ∧ is moved to the next action and the identifier t is added to the write set of the variable x. Now we can perform the read access to variable y and we have:

t : wr(x).rd(y) ∧ ∅ x, {t}, ∅ y, ∅, {t}
where the identifier t is added to the read set of the variable y. The set Γ of the transaction t remains empty since there is no transaction which had write access to variable y. Rule Par allows expressions to execute in parallel (in an interleaving fashion) ensuring the uniqueness of the identifier t. By executing its last action, the transaction t can commit if the set Γ is empty, by applying the rule Commit. After it commits, the execution proceeds with the continuation Y and the identifier t is deleted from the remaining system. The intuition is that transaction t can commit if the other transactions, having a write access to the variables that transaction t read, have been committed. The rollback of the transaction t can be done with the rule RollR. It will force every transaction in parallel having the identifier t in their set Γ to roll back too. The intuition is that when the transaction with wr(x) rolls back, every transaction which has read access to x should roll back as well. For instance, let us consider the system containing following transactions:

t : A Γ | t1 : A1 {t} | t2 : A2 Γ 2 such that rd(x) ∈ A1 and t / ∈ Γ2
and that transaction t needs to be rolled back. Then, by applying the rule RollR, we obtain the system:

roll(t) | roll(t1) | t2 : A2 Γ 2
in which transaction t 1 is rolled back too since t ∈ Γ 1 while t 2 remains the same. Now we can give the rules necessary to model reader and writer preference. To give a better intuition about the differences between the two models, we use the example from the introduction as a running example.

Reader preference. To model the reader preference we use the rules from Figure 2 and the rule given below.

(R-RollW)

(W ⊆ {t} ∨ R ⊆ {t}) t : H[ ∧ wr(x).A] Γ x, W, R M → roll(t) x, W, R @t M @t
The rollback operator is triggered when the transaction t cannot write on the variable x (this happens when W ⊆ {t} or R ⊆ {t}). With the rule R-RollW the transaction t goes to the state roll(t), i.e. the initial state of the transaction. Additionally, the identifier t is removed from every triple of the shared memory.

To illustrate it, we use the example from the introduction, abstracting away from the read and write values contained in variables and representing accesses of two threads to the shared memory in our framework with transactions t 1 and t 2 . Transaction t 1 has read accesses to variables y and x and then writes on variable z, while t 2 has read access to variables z and then writes on x. We have the following system t1 : ∧ rd(y).rd(x).wr(z)] ∅ | t2 : ∧ rd(z).wr(x)] ∅

x, ∅, ∅ y, ∅, ∅ z, ∅, ∅

We assume that read accesses are executed in parallel and the obtained system is

t1 : rd(y).rd(x). ∧ wr(z)] ∅ | t2 : rd(z). ∧ wr(x)] ∅ x, ∅, {t1} y, ∅, {t1} z, ∅, {t2}
Now transaction t 1 is executing write access to variable z but since in the memory for variable z we have R ⊆ {t 1 } (R = {t 2 }), the transaction t 1 needs to roll back according to the rule R-RollW, and we have

roll(t1) | t2 : rd(z). ∧ wr(x)] ∅ x, ∅, ∅ y, ∅, ∅ z, ∅, {t2}
where roll(t 1 ) = t 1 : ∧ rd(y).rd(x).wr(z)] ∅ .

Writer preference. To model the writer preference we use the rules from Figure 2 and the rules given below.

(W-Pref)

W ⊆ {t} ∧ R ⊆ {t} ∧ R = R \ t t : H[ ∧ wr(x).A + B] Γ | t i ∈R ti : Ai Γ i x, W, R M → t : H[wr(x). ∧ A + B] Γ | t i ∈R roll(ti) x, W ∪ t, R @t i M @t i (W-RollW) (W ⊆ {t}) t : H[ ∧ wr(x).A] Γ x, W, R M → roll(t) x, W, R @t M @t
The rollback is triggered by the writer only in the case when another transaction has write access to the same variable. Therefore the condition on the rule W-RollW is simply W ⊆ {t}. The additional rule, with respect to the reader preference is the rule W-Pref. It allows a transaction to modify the value of a variable x if other transactions have read access to it. At the same time, all transactions executing in parallel whose identifiers belong to the set R, are requested to roll back.

To illustrate it, we use the same example as for the reader preference where read accesses are executed already. Therefore, we have the system t1 : rd(y).rd(x). ∧ wr(z) ∅ | t2 : rd(z). ∧ wr(x)] ∅

x, ∅, {t1} y, ∅, {t1} z, ∅, {t2}

Now we can execute the write access to variable z, since in the rule W-Pref the condition for the read set R allows a transaction to perform the write access, and in that case all transactions in parallel having read access to variable z need to be rolled back. Therefore, transaction t 1 executes write access, while t 2 will be rolled back, and we have: where roll(t 2 ) = t 2 : ∧ rd(z).wr(x)] ∅ .

Conclusion and Future Work

We have presented a framework to express the STM mechanism in a simple shared memory context. The framework is able to model two different policies for the execution of the concurrent transactions: writer and reader preference.

Our intention is to start from a simple calculus and then to add in a modular way: nested transactions, data structures (e.g., C structures) and more complex scheduling policies. Nested transactions will require to record for each transaction a list of its children transactions. These children inherit the access of the parent transaction. There exist different policies to deal with nested transactions: closed nested transactions [START_REF] Gray | Transaction Processing: Concepts and Techniques[END_REF] and open nested transactions [START_REF] Moss | Open Nested Transactions: Semantics and Support[END_REF]. The difference is that in the first case the parent does not execute till all the children have committed, while in the second case the parent can commit even before its children. This may lead to inconsistencies which have to be dealt with compensations.

Our ultimate goal is then to prove that the modular framework satisfies the opacity [START_REF] Guerraoui | On the correctness of transactional memory[END_REF] property, that is, all the execution traces of our semantics, where the transactional bodies are interleaved, are equivalent to executions in which transactional blocks are executed as a whole (in a lock-based fashion) without being interleaved with other transactions.

(Fig. 1 .

 1 Fig. 1. Syntax

t1:

  rd(y).rd(x).wr(z) ∧ ∅ | roll(t2) x, ∅, {t1} y, ∅, {t1} z, {t1}, ∅

This work has been partially supported by French ANR project DCore ANR-18-CE25-0007 and by the Italian INdAM -GNCS project 2020 Reversible Concurrent Systems: from Models to Languages. We also acknowledge partial support from the following projects: EPSRC EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833, EP/N028201/1, and EP/T006544/1.