# CRIL: A Concurrent Reversible Intermediate Language

Shunya Oguchi Shoji Yuen Graduate School of Informatics, Nagoya University
Furo-cho, Chikusa-ku, Nagoya 464-8601, Japan<EMAIL_ADDRESS>
###### Abstract

We present a reversible intermediate language with concurrency for translating
a high-level concurrent programming language to another lower-level concurrent
programming language, keeping reversibility. Intermediate languages are
commonly used in compiling a source program to an object code program closer
to the machine code, where an intermediate language enables behavioral
analysis and optimization to be decomposed in steps. We propose CRIL
(Concurrent Reversible Intermediate Language) as an extension of RIL used by
Mogensen for a functional reversible language, incorporating a multi-thread
process invocation and the synchronization primitives based on the P-V
operations. We show that the operational semantics of CRIL enjoy the
properties of reversibility, including the causal safety and causal liveness
proposed by Lanese et al., checking the axiomatic properties. The operational
semantics is defined by composing the bidirectional control flow with the
dependency information on updating the memory, called annotation DAG. We show
a simple example of ‘airline ticketing’ to illustrate how CRIL preserves the
causality for reversibility in imperative programs with concurrency.

##  1 Introduction

Reversible programming languages have been proposed to describe reversible
computation where the control flows both forward and backward [25, 5, 24, 7].
They directly describe reversible computation and develop new aspects of
software development since reversibility holds all information at any point of
execution. In forward-only execution, the computation can overwrite the part
of its intermediate history unless it is used in the following computation for
efficiency. In analyzing the behavior, such as debugging, it is common to
replay the execution to the point in focus to recreate the lost part of
history. For a concurrent program, replaying the execution is usually
difficult since updating shared resources among multiple control threads
depends on the runtime environment.

Intermediate languages mediate the translation from the source language to a
low-level machine language for execution. Step-by-step translation via
intermediate languages is a common technique for optimization in compilers.
The intermediate language in LLVM [15] is often used as a behavioral model for
program analysis.

Mogensen uses RIL [17] as an intermediate language with reversibility for a
functional reversible language in the memory usage analysis. RSSA [18] based
on RIL is used for compiling and optimizing Janus programs [10, 4].
Reversibility with concurrency has been studied in process calculi [3, 21, 12,
11], in event structures [19, 20, 22, 16] and recently in programming
languages such as Erlang [13] and a simple imperative programming language [7,
9].

We propose a reversible intermediate language CRIL by extending RIL. CRIL
extends RIL by allowing multiple blocks to run concurrently and the
synchronization primitive based on the P-V operations. In CRIL, concurrent
blocks interact with each other via shared variables. To establish the
reversibility for concurrent programs, the causality among shared variables
has to be preserved. Unlike sequential reversible programs, even if one step
of a program is reversible, the whole program is not reversible in general
since shared variables may not be reversed correctly.

To make a program of CRIL reversible, we give the operational semantics as the
labeled transition system, $\mbox{\it LTSI}_{CRIL}$, as the composition of the
operational semantics with one-step reversibility and a data structure called
‘annotation DAG’. An annotation DAG accumulates the causality of updating
memory in a forward execution and rolls back the causality to control the
reversed flow in the backward execution. We show that $\mbox{\it LTSI}_{CRIL}$
has the basic properties for reversibility proposed in [14]. Using the
approach of [14], it is shown that $\mbox{\it LTSI}_{CRIL}$ enjoys the Causal
Safety and the Causal Liveness, which are important in analyzing CRIL programs
compositionally.

By translating a high-level programming language to CRIL, $\mbox{\it
LTSI}_{CRIL}$ works as a virtual machine, and its behavior is guaranteed to be
reversible. CRIL enables fine-grained behavioral analysis such as optimization
and reversible debugging. In section 4, we present a simple example of airline
ticketing given in [6] to enable reversible debugging.

The paper is organized as follows. Section 2 presents the syntax of CRIL and
the operational semantics for control flow. Section 3 introduces annotation
DAG as a data structure to store the causality of updating memory. We define
$\mbox{\it LTSI}_{CRIL}$ as the operational semantics for CRIL and show the
reversibility of $\mbox{\it LTSI}_{CRIL}$, which is followed by the airline
ticketing example in section 4. Section 5 presents concluding remarks.

##  2 CRIL

Figure 1: The syntax of CRIL

The syntax of CRIL is defined in figure 1. Following RIL [17], a CRIL program
consists of an unordered set of basic blocks. Given a set of labels
$\mathcal{L}$, a block has an entry point followed by a block body and an exit
point with labels. A block body is either a basic instruction or a call
statement.

###  2.1 Basic block

We assume all references to variables have a global scope and there exists a
heap memory M indexed by integers, where $\texttt{M[}x\texttt{]}$ denotes the
$x$-th element in M. An expression $e$ is either an arithmetic expression or a
boolean expression with the usual operators
$\texttt{+},\texttt{-},\texttt{\char
94\relax},\texttt{==},\texttt{!=},\texttt{<},\texttt{<=},\texttt{>},\texttt{>=},\texttt{\&\&},\texttt{||},\texttt{!}$
of the C language, where ^ is the bitwise exclusive OR operation. The boolean
operators and logical connectives treat $0$ as false and any non-$0$ value as
true. An expression can contain integer constants, which are denoted by $k$.

##### Entry/exit point

An entry/exit point of a basic block is the following forms:

Entry point | Exit point
---|---
(1) | $l\ \texttt{<-}$ | (1’) | $\texttt{->}\ l$
(2) | $l_{\\_}1\texttt{;}l_{\\_}2\ \texttt{<-}\ e$ | (2’) | $e\ \texttt{->}\ l_{\\_}1\texttt{;}l_{\\_}2$
(3) | $\texttt{begin}\ l$ | (3’) | $\texttt{end}\ l$

where $l,l_{\\_}1,l_{\\_}2\in\mathcal{L}$. We write $\mathsf{entry}(b)$ for
the entry point of a basic block $b$, and $\mathsf{exit}(b)$ for the exit
point of a basic block $b$.

The informal meaning of each item is explained as follows:

  * (1) and (1’):

$l\ \texttt{<-}$ receives the control at $l$ unconditionally in a forward
execution. In a backward execution, it sends the control to the block that
receives the control at $l$. $\texttt{->}\ l$ dually works in the reversed way
of $l\ \texttt{<-}$.

  * (2) and (2’):

$l_{\\_}1;l_{\\_}2\ \texttt{<-}\ e$ receives the control at $l_{\\_}1$ when
$e$ is evaluated to a non-$0$ value and at $l_{\\_}2$ otherwise in a forward
execution. In a backward execution, it returns the control to the block that
receives the control at $l_{\\_}1$ when $e$ is evaluated to non-0 and at
$l_{\\_}2$ otherwise. $e\ \texttt{->}\ l_{\\_}1\texttt{;}l_{\\_}2$ dually
works in the reversed way of $l_{\\_}1;l_{\\_}2\ \texttt{<-}\ e$.

  * (3) and (3’):

$\texttt{begin}\ l$ receives the control from the call statement labeled by
$l$ in a forward execution. In a backward execution, it returns the control to
the statement labeled by $l$. $\texttt{end}\ l$ dually works in the reversed
way of $\texttt{end}\ l$.

A basic block is either an instruction block or a call statement.

##### Instruction block

Basic instruction is in the forms:

(1) | ${\emph{left}}\oplus\\!\texttt{=}\;e$ | (3) | $\texttt{V}\ x$ | (5) | $\texttt{assert}\ e$
---|---|---|---|---|---
(2) | ${\emph{left}}_{\\_}1\ \texttt{{<->}}\ {\emph{left}}_{\\_}2$ | (4) | $\texttt{P}\ x$ | (6) | skip

We write $\textsf{inst}(b)$ for the basic instruction in $b$. The informal
semantics is explained as follows:

  * (1):

${\emph{left}}\oplus\\!\texttt{=}\;e$ is an update statement where left is a
left-value, and $\oplus\in\\{\texttt{+},\texttt{-},\texttt{\char
94\relax}\\}$. left is relatively updated by $e$ in that +=, -=, and ^= with
the same semantics as in the C language. If $\emph{left}=x$, $x$ must not
appear in $e$. If $\emph{left}=$ M[$x$], heap references must not appear in
$e$.

  * (2):

${\emph{left}}_{\\_}1\ \texttt{{<->}}\ {\emph{left}}_{\\_}2$ is an exchange
where ${\emph{left}}_{\\_}1$ and ${\emph{left}}_{\\_}2$ are left-values. It
swaps the values specified by ${\emph{left}}_{\\_}1$ and
${\emph{left}}_{\\_}2$. The same variable must not appear on both sides of
<->.

  * (3) and (4):

$\texttt{V}\ x$ and $\texttt{P}\ x$ are the P and V operations for
synchronization, which correspond to those commonly used in operating systems.
We assume variables in P and V instruction only appear as the parameters of P
and V. In a forward execution, $\texttt{V}\ x$ is defined when $x$ is 0 and
terminates when $x$ is 1 and $\texttt{P}\ x$ is defined when $x$ is $1$ and
terminates when $x$ is $0$. In a backward execution, $\texttt{V}\ x$ and
$\texttt{P}\ x$ work as $\texttt{P}\ x$ and $\texttt{V}\ x$ of the forward
execution respectively.

  * (5):

$\texttt{assert}\ e$ aborts the execution if $e$ evaluates to $0$, and does
nothing otherwise.

  * (6):

skip does nothing in either direction.

We call $\mathcal{R}=Vars\cup\\{\texttt{M}\\}$ memory resources. Let
$\mathsf{Var}(E)$ be the set of memory resource references appearing in $E$,
where $E$ is one of $entry$, $exit$, or $inst$ in the grammar of figure 1. For
example,
$\mathsf{Var}(\texttt{z-=M[x]+y})=\\{\texttt{M},\texttt{x},\texttt{y},\texttt{z}\\}$.
$\mathsf{read}(b)$ is the memory resources that $b$ uses, and
$\mathsf{write}(b)$ is the memory resources that $b$ updates.

$\begin{array}[]{lll}\begin{array}[]{l}\mathsf{read}(b)=\mathsf{Var}(\mathsf{entry}(b))\\\
\qquad\cup\;\mathsf{Var}(\mathsf{inst}(b))\\\
\qquad\cup\;\mathsf{Var}(\mathsf{exit}(b))\end{array}&&\mathsf{write}(b)=\begin{cases}\\{x\\}&\mbox{If
$\mathsf{inst}(b)=x\oplus\\!\texttt{=}\;e$}\\\ \\{\texttt{M}\\}&\mbox{If
$\mathsf{inst}(b)=\texttt{M[}x\texttt{]}\oplus\\!\texttt{=}\;e$}\\\
\\{x,y\\}&\mbox{If $\mathsf{inst}(b)=x\;\texttt{{<->}}\;y$}\\\
\\{x,\texttt{M}\\}&\mbox{If
$\mathsf{inst}(b)\in\\{x\;\texttt{{<->}}\;\texttt{M[}y\texttt{]},\texttt{M[}y\texttt{]}\;\texttt{{<->}}\;x\\}$}\\\
\\{\texttt{M}\\}&\mbox{If
$\mathsf{inst}(b)=\texttt{M[}x\texttt{]}\;\texttt{{<->}}\;\texttt{M[}y\texttt{]}$}\\\
\\{x\\}&\mbox{If $\mathsf{inst}(b)\in\\{\texttt{P}\ x,\texttt{V}\ x\\}$}\\\
\varnothing&\mbox{Otherwise.}\end{cases}\end{array}$

##### Call statement

A call statement is a basic block in the following form:

$l\;\texttt{<-}\ \texttt{call}\ l_{\\_}1\texttt{,}\cdots\texttt{,}l_{\\_}n\
\texttt{->}\;l^{\prime}$ ($n\geq 1$)

When $n=1$, it behaves as a subroutine call in RIL. If $n\geq 2$, the controls
are simultaneously sent to all basic blocks with $\texttt{begin}\ l_{\\_}i$ in
the forward execution, and to all basic blocks with $\texttt{end}\ l_{\\_}i$
in the backward execution. In a forward execution, $\texttt{call}\
l_{\\_}1\texttt{,}\cdots\texttt{,}l_{\\_}n$ terminates when all controls are
returned to this block. In a backward execution, it sends the controls to the
blocks whose exit points are $\texttt{end}\ l_{\\_}i$.

As in RIL, call appears only in a basic block whose entry and exit parts are
unconditional, and not in any begin and end blocks. CRIL does not have uncall
for a call statement since uncall makes the semantics more complex in that an
uncall nested in multiple calls causes the mixture of forward and backward
execution for process blocks. An uncall can be implemented as a symmetrical
call.

###  2.2 Process

For a basic block $b$, $\mathsf{in}(b)$,$\mathsf{out}(b)\subseteq\mathcal{L}$
are defined as follows:

$\begin{array}[]{ll}\mathsf{in}(b)=\begin{cases}\\{l\\}&\mbox{if}\
\mathsf{entry}(b)=l\;\texttt{<-}\\\ \\{l_{\\_}1,l_{\\_}2\\}&\mbox{if}\
\mathsf{entry}(b)=l_{\\_}1;l_{\\_}2\;\texttt{<-}\;e\\\ \varnothing&\mbox{if}\
\mathsf{entry}(b)=\texttt{begin}\
l\end{cases}&\mathsf{out}(b)=\begin{cases}\\{l\\}&\mbox{if}\
\mathsf{exit}(b)=\texttt{->}\;l\\\ \\{l_{\\_}1,l_{\\_}2\\}&\mbox{if}\
\mathsf{exit}(b)=e\;\texttt{->}\;l_{\\_}1;l_{\\_}2\\\ \varnothing&\mbox{if}\
\mathsf{exit}(b)=\texttt{end}\ l\end{cases}\end{array}$

Basic blocks $b_{\\_}1$ and $b_{\\_}2$ are connected, written as
$b_{\\_}1\bowtie b_{\\_}2$, if
$\mathsf{out}(b_{\\_}1)\cap\mathsf{in}(b_{\\_}2)\not=\varnothing$ or
$\mathsf{in}(b_{\\_}1)\cap\mathsf{out}(b_{\\_}2)\not=\varnothing$. A process
block of $b$ is $\mathsf{PB}(b,Pg)=\\{b^{\prime}\in
Pg\;|\;b^{\prime}\bowtie^{\ast}b\\}$, where $\ast$ stands for reflexive and
transitive closure. No basic block is shared among process blocks since they
are the equivalence classes of $\bowtie^{*}$, which is an equivalence relation
on basic blocks.

Let $L_{\\_}1(B)=\bigcup_{\\_}{b\in B}(\mathsf{in}(b)\cup\mathsf{out}(b))$ and
$L_{\\_}2(B)=\\{l\;|\;\exists b\in
B.\;\mathsf{entry}(b)=\texttt{begin}\;l\lor\mathsf{exit}(b)=\texttt{end}\;l\\}$.
A CRIL program $Pg$ is well-formed when it satisfies the following conditions:

  * (1):

For all $l\in L_{\\_}1(Pg)$, there exists a unique pair $(b_{\\_}1,b_{\\_}2)$
such that $\mathsf{in}(b_{\\_}1)\cap\mathsf{out}(b_{\\_}2)=\\{l\\}$;

  * (2):

For all $l\in L_{\\_}2(Pg)$, there exists a unique pair $(b_{\\_}1,b_{\\_}2)$
such that $\mathsf{entry}(b_{\\_}1)=\texttt{begin}\;l$ and
$\mathsf{exit}(b_{\\_}2)=\texttt{end}\;l$;

  * (3):

$L_{\\_}1(Pg)\cap L_{\\_}2(Pg)=\varnothing$

  * (4):

For all $b\in Pg$, $|L_{\\_}2(\mathsf{PB}(b,Pg))|=1$; and

  * (5):

There is a special label $\texttt{main}\in L_{\\_}2(Pg)$.

The well-formedness ensures that once a control enters into a process block at
$\texttt{begin}\ l$, the control may reach only the matching $\texttt{end}\ l$
in the forward execution and vice versa in the backward execution. A process
block $\mathsf{PB}(b,Pg)$ is labeled by $l$ when it contains the basic block
with $\texttt{begin}\ l$.

A call statement $\texttt{call}\ l_{\\_}1\texttt{,}\cdots\texttt{,}l_{\\_}n$
sends controls to process blocks labeled by $l_{\\_}1,\cdots,l_{\\_}n$. A
process block with control is called a process. A process is executed by
passing the control among the basic blocks in its process block. Since call
can be recursive, a process may have some subprocesses.

In a forward execution, $l\ \texttt{<-}\ \texttt{call}\
l_{\\_}1\texttt{,}\cdots\texttt{,}l_{\\_}n\ \texttt{->}\ l^{\prime}$ receives
a control at $l$, forks $n$ processes, and sends the control to $l^{\prime}$
after merging the processes. In the backward execution, it works in a reversed
manner. In the following, we assume a CRIL program is well-formed.

###  2.3 Basic operational semantics

The set of process identifiers $\mathsf{PID}$ is $(\mathbb{N}_{\\_}+)^{\ast}$
where ${\mathbb{N}_{\\_}+}$ is the set of positive integers.
$p\in\mathsf{PID}$ denotes an identifier uniquely assigned to a process. When
$p$ executes a process block $\mathsf{PB}(b,Pg)$, we also write
$\mathsf{PB}(p)$. If $p$ is labeled by $l$, $\mathsf{PB}(p)=\mathsf{PB}(b,Pg)$
where $\mathsf{entry}(b)=\texttt{begin}\ l$. A special root process has the
identifier of $\varepsilon$. The runtime invokes the root process and sends
the control to a process block labeled by main to start an execution of a CRIL
program. For a process $p$, $p\cdot i$ is assigned to the $i$-th subprocess
invoked by a call statement of process $p$. $\preceq$ is the prefix relation.
A process set $PS$ is a set of process identifiers satisfying (1)
$\varepsilon\in PS$; (2) $p\in PS$ implies $p^{\prime}\in PS$ for
$p^{\prime}\preceq p$; and (3) $p\cdot i$ implies $p\cdot j\in PS$ for $j<i$.
For a process set $PS$ and a process id $p$, $\mathsf{isleaf}(PS,p)$ holds if
for all $p^{\prime}\in PS$, $p\preceq p^{\prime}$ imples $p=p^{\prime}$.

A process configuration is $(l,stage)$, where $l\in\mathcal{L}$ and
$stage\in\\{\texttt{begin},\texttt{run},\texttt{end}\\}$ are the location of
the control in a process block. If $stage=\texttt{begin}$, it is before
executing the process block, if $stage=\texttt{run}$, it is executing the
process block, and if $stage=\texttt{end}$ it terminated the process block.
$\mathsf{PC}$ is the set of process configurations.

A program configuration is $({Pg},\rho,\sigma,{Pr})$, where ${Pg}$ is the
program (which never changes), $\rho:Vars\to\mathbb{Z}$ maps a variable to its
value, $\sigma:\mathbb{N}\to\mathbb{Z}$ maps a heap memory address to its
value. A process map ${Pr}:\mathsf{PID}\to\mathsf{PC}\cup\\{\bot\\}$ maps a
process to a process configuration. We assume $Pr_{\\_}{act}$ is a process set
where $Pr_{\\_}{act}=\\{p\in\mathsf{PID}|Pr(p)\in\mathsf{PC}\\}$.
$\mathcal{C}$ is the set of all program configurations.

A transition relation over program configurations

$(Pg,\rho,\sigma,Pr)\xrightleftharpoons{p,Rd,Wt}_{\mathrm{prog}}(Pg,\rho^{\prime},\sigma^{\prime},Pr^{\prime})$

is defined in figure 2. $(Pg,\rho,\sigma,Pr)$ steps forward to
$(Pg,\rho^{\prime},\sigma^{\prime},Pr^{\prime})$ by the process $p$ with
reading memory resource $Rd$ and updating memory resource $Wt$. And
$(Pg,\rho^{\prime},\sigma^{\prime},Pr^{\prime})$ steps backward to
$(Pg,\rho,\sigma,Pr)$ in the same way.

We explain the SOS rules in figure 2. AssVar and AssArr present the update
behavior. The exchange behavior is presented by SwapVarVar, SwapVarArr,
SwapArrVar, and SwapArrArr. SwapVarArr and SwapArrVar are reversible since $y$
is evaluated to the same value on both sides of
$\mathrel{\mathchoice{\ooalign{$\displaystyle\leftharpoondown$\cr$\displaystyle\rightharpoonup$\cr}}{\ooalign{$\textstyle\leftharpoondown$\cr$\textstyle\rightharpoonup$\cr}}{\ooalign{$\scriptstyle\leftharpoondown$\cr$\scriptstyle\rightharpoonup$\cr}}{\ooalign{$\scriptscriptstyle\leftharpoondown$\cr$\scriptscriptstyle\rightharpoonup$\cr}}}$.
SwapVarVar and SwapArrArr are clearly reversible. Skip presents the skip
behavior. Assert presents the assertion behavior, which stops when $e$ is
evaluated to $0$.

V-op and P-op present the behavior of V $x$ and P $x$ for synchronization by
$x$ shared among concurrent processes. In forward execution, V $x$ sets $x=1$
when $x=0$, and waits otherwise. In backward execution, V $x$ sets $x=0$ when
$x=1$, and waits otherwise. P behaves in a symmetrical fashion. By the pair of
V $x$ and P $x$, $x$ can be used as a semaphore to implement the mutual
exclusion for both directions of execution.

Inst presents the one-step behavior of a basic block. The instruction updates
$\rho$ and $\sigma$ and the entry and exit points give the status of the
process. The process is running if $stage$ is run. the process is at the
initial block or at the final block, if $stage$ is begin or end. The
transition label $Rd$ is $\texttt{read}(b)$ and the transition label $Wt$ is
$\texttt{write}(b)$.

CallFork presents that a call statement forks subprocesses. When $p$ executes
a call statement $\texttt{call}\ l_{\\_}1\texttt{,}\cdots\texttt{,}l_{\\_}n$
forwards, it forks subprocesses labeled by $l_{\\_}1,\cdots,l_{\\_}n$ and $p$
stores the label for returning the controls in $Pr$. Note that the process map
is changed to $Pr^{\prime}$ with subprocesses after forking subprocesses.
Since $\mathsf{isleaf}(Pr^{\prime}_{\\_}{act},p)$ does not hold, $p$ does not
pass the control to the next block until all the subprocesses are merged.
CallMerge works dually to CallFork. In a forward execution, when all
subprocesses reach the end stage, all subprocesses are set to inactive and $p$
resumes to pass the control to the next basic block. In a backward execution,
${\bf CallFork}$ behaves as ${\bf CallMerge}$ of forward execution and vice
versa for ${\bf CallMerge}$.

Figure 2: The basic operational semantics

In a program configuration of CRIL, there is no stack as in RIL to store the
return label for subroutine calls. The process map stores the return label,
which is not available until $\mathsf{isleaf}(Pr_{\\_}{act},p)$ holds, where
it checks if the label is on the stack.

Figure3 shows an example of CRIL program $Pg$. There are four process blocks
$\\{b_{\\_}1,b_{\\_}2,b_{\\_}3\\}$,$\\{b_{\\_}4,b_{\\_}5\\}$,
$\\{b_{\\_}6\\}$, and $\\{b_{\\_}7\\}$. A process map assigns $\varepsilon$ to
$\\{b_{\\_}1,b_{\\_}2,b_{\\_}3\\}$. In the following execution, it assigns 1
to $\\{b_{\\_}4,b_{\\_}5\\}$, 2 to $\\{b_{\\_}6\\}$, and 3 to
$\\{b_{\\_}7\\}$.

An example of the transitions for $Pg$ is as follows:

Figure 3: A CRIL program $Pg$

$\begin{array}[]{l}(Pg,\rho_{\\_}0,\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{main},\texttt{begin})])\\\
\xrightleftharpoons{\varepsilon,\varnothing,\varnothing}_{\mathrm{prog}}(Pg,\rho_{\\_}0,\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{l1},\texttt{run})])\\\
\xrightleftharpoons{\varepsilon,\varnothing,\varnothing}_{\mathrm{prog}}(Pg,\rho_{\\_}0,\sigma_{\\_}0,\begin{array}[]{l}[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{begin},\texttt{sub0}),\\\
2\mapsto(\texttt{sub1},\texttt{begin}),3\mapsto(\texttt{sub2},\texttt{begin})]\end{array})\\\
\xrightleftharpoons{1,\\{\texttt{x}\\},\\{\texttt{x}\\}}_{\mathrm{prog}}(Pg,\rho_{\\_}1,\sigma_{\\_}0,\begin{array}[]{l}[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{l3},\texttt{run}),\\\
2\mapsto(\texttt{sub1},\texttt{begin}),3\mapsto(\texttt{sub2},\texttt{begin})]\end{array})\\\
\qquad\mbox{where}\ \rho_{\\_}1=\rho_{\\_}0[\texttt{x}\mapsto 1]\\\
\xrightleftharpoons{2,\\{\texttt{x},\texttt{y}\\},\\{\texttt{x}\\}}_{\mathrm{prog}}(Pg,\rho_{\\_}2,\sigma_{\\_}0,\begin{array}[]{l}[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{l3},\texttt{run}),\\\
2\mapsto(\texttt{sub1},\texttt{end}),3\mapsto(\texttt{sub2},\texttt{begin})]\end{array})\\\
\qquad\mbox{where}\ \rho_{\\_}2=\rho_{\\_}2[\texttt{y}\mapsto 1]\\\
\xrightleftharpoons{3,\\{\texttt{x},\texttt{z}\\},\\{\texttt{z}\\}}_{\mathrm{prog}}(Pg,\rho_{\\_}3,\sigma_{\\_}0,\begin{array}[]{l}[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{l3},\texttt{run}),\\\
2\mapsto(\texttt{sub1},\texttt{end}),3\mapsto(\texttt{sub2},\texttt{end})]\end{array})\\\
\qquad\mbox{where}\ \rho_{\\_}3=\rho_{\\_}1[\texttt{z}\mapsto 1]\\\
\xrightleftharpoons{1,\\{\texttt{x}\\},\\{\texttt{x}\\}}_{\mathrm{prog}}(Pg,\rho_{\\_}4,\sigma_{\\_}0,\begin{array}[]{l}[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{sub0},\texttt{end}),\\\
2\mapsto(\texttt{sub1},\texttt{end}),3\mapsto(\texttt{sub2},\texttt{end})]\end{array})\\\
\qquad\mbox{where}\ \rho_{\\_}4=\rho_{\\_}3[\texttt{x}\mapsto 2]\\\
\xrightleftharpoons{\varepsilon,\varnothing,\varnothing}_{\mathrm{prog}}(Pg,\rho_{\\_}4,\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{l2},\texttt{run})])\\\
\xrightleftharpoons{\varepsilon,\varnothing,\varnothing}_{\mathrm{prog}}(Pg,\rho_{\\_}4,\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{main},\texttt{end})])\\\
\end{array}$

This forward execution ends with $\texttt{x}=2,\texttt{y}=1,\texttt{z}=1$. The
operational semantics show that the computation may be reversed to
$(Pg,\rho_{\\_}0,\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{main},\texttt{begin})])$.
However, it is possible to reverse to a different configuration such as
$\texttt{x}=0,\texttt{y}=-1,\texttt{z}=-1$ if the call statement is reversed
in a different order. Thus, this operational semantics is not reversible. In
the next section, we will combine an annotation for the dependency information
as DAG to make the basic properties for reversibility as well as Causal Safety
and Causal Liveness.

##  3 Reversibility of CRIL

Table 1 (a) shows the transitions of store $\rho$ by the sequence of basic
blocks in the forward computation of the example in the previous section.
Process $p$ makes the forward (left-to-right) transition of
$\xrightleftharpoons{p,Rd,Wt}_{\mathrm{prog}}$. The program configuration at
the end is $(Pg,[\texttt{x}\mapsto 2,\texttt{y}\mapsto 1,\texttt{z}\mapsto
1],\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{main},\texttt{end})]$. The
configuration may lead to a different store by the backward (right-to-left)
transitions of $\xrightleftharpoons{p,Rd,Wt}_{\mathrm{prog}}$ as shown in
table 1 (b). Although each step of the operational semantics keeps the local
reversibility, it does not preserve the causality of shared memory. The
forward step of $\xrightleftharpoons{p,Rd,Wt}_{\mathrm{prog}}$ updates $Wt$
reading $Rd$ making the causality from $Rd$ to $Wt$. Our idea is to control
processes to keep the causality by observing $Rd$ and $Wt$ being combined with
the operational semantics.

| x | y | z
---|---|---|---
| 0 | 0 | 0
$b_{\\_}1\in\mathsf{PB}(\varepsilon)$ |  |  |
| 0 | 0 | 0
$b_{\\_}2\in\mathsf{PB}(\varepsilon)$ |  |  |
| 0 | 0 | 0
$b_{\\_}4\in\mathsf{PB}(1)$ |  |  |
| 1 | 0 | 0
$b_{\\_}6\in\mathsf{PB}(2)$ |  |  |
| 1 | 1 | 0
$b_{\\_}7\in\mathsf{PB}(3)$ |  |  |
| 1 | 1 | 1
$b_{\\_}5\in\mathsf{PB}(1)$ |  |  |
| 2 | 1 | 1
$b_{\\_}2\in\mathsf{PB}(\varepsilon)$ |  |  |
| 2 | 1 | 1
$b_{\\_}3\in\mathsf{PB}(\varepsilon)$ |  |  |
| 2 | 1 | 1
(a)

| x | y | z
---|---|---|---
| 2 | 1 | 1
$b_{\\_}3\in\mathsf{PB}(\varepsilon)$ |  |  |
| 2 | 1 | 1
$b_{\\_}2\in\mathsf{PB}(\varepsilon)$ |  |  |
| 2 | 1 | 1
$b_{\\_}7\in\mathsf{PB}(3)$ |  |  |
| 2 | $-1$ | 1
$b_{\\_}6\in\mathsf{PB}(2)$ |  |  |
| 2 | $-1$ | $-1$
$b_{\\_}5\in\mathsf{PB}(1)$ |  |  |
| 1 | $-1$ | $-1$
$b_{\\_}4\in\mathsf{PB}(1)$ |  |  |
| 0 | $-1$ | $-1$
$b_{\\_}2\in\mathsf{PB}(\varepsilon)$ |  |  |
| 0 | $-1$ | $-1$
$b_{\\_}1\in\mathsf{PB}(\varepsilon)$ |  |  |
| 0 | $-1$ | $-1$
(b)

Table 1: Store changes in executions

| $\mathsf{read}$ | $\mathsf{write}$
---|---|---
$b_{\\_}1$ | $\varnothing$ | $\varnothing$
$b_{\\_}2$ | $\varnothing$ | $\varnothing$
$b_{\\_}3$ | $\varnothing$ | $\varnothing$
$b_{\\_}4$ | $\\{\mathtt{x}\\}$ | $\\{\mathtt{x}\\}$
$b_{\\_}5$ | $\\{\mathtt{x}\\}$ | $\\{\mathtt{x}\\}$
$b_{\\_}6$ | $\\{\mathtt{x},\mathtt{y}\\}$ | $\\{\mathtt{y}\\}$
$b_{\\_}7$ | $\\{\mathtt{x},\mathtt{z}\\}$ | $\\{\mathtt{z}\\}$
Table 2: $\mathsf{read}$ and $\mathsf{write}$ for basic blocks

Table 2 presents $\mathsf{read}$ and $\mathsf{write}$ for each basic block. In
the backward execution, after reversing $b_{\\_}3b_{\\_}2$, CallMerge works as
a forking of three processes in backward. At this point, $b_{\\_}5$,
$b_{\\_}6$, and $b_{\\_}7$ are possible by using the rule backward. Since
$\mathsf{write}(b_{\\_}5)=\\{\texttt{x}\\}$ and both $\mathsf{read}(b_{\\_}6)$
and $\mathsf{read}(b_{\\_}7)$ contain $x$, the order between $b_{\\_}5$

and $b_{\\_}6$, and the order between $b_{\\_}5$ and $b_{\\_}6$ affect the
causality. We say $b_{\\_}i$ conflicts with $b_{\\_}j$ where $i\not=j$ if
$\mathsf{read}(b_{\\_}i)\cap\mathsf{write}(b_{\\_}j)\not=\varnothing$ or
$\mathsf{read}(b_{\\_}j)\cap\mathsf{write}(b_{\\_}i)\not=\varnothing$. Since
$b_{\\_}6$ and $b_{\\_}7$ do not conflict with each other, the order between
$b_{\\_}6$ and $b_{\\_}7$ does not affect the causality. Thus, for the forward
execution in table 1 (a), the reversed execution
$b_{\\_}3b_{\\_}2b_{\\_}3b_{\\_}6b_{\\_}7b_{\\_}4b_{\\_}2b_{\\_}1$ reaches
$\rho_{\\_}0$ as a legitimate reversed computation.

###  3.1 Annotation DAG

We shall present a data structure called ‘annotation DAG’ (Directed Acyclic
Graph) that keeps the conflicting information in forward execution and
controls the backward execution by matching the causality, observing the
memory $Wt$ updated by reading the memory $Rd$.

######  Definition 1.

An annotation DAG is $A=(V,E_{\\_}R,E_{\\_}W)$ satisfying the following
conditions:

  1. 1.

$V\subseteq(\mathsf{PID}\times\mathbb{N})\cup\\{\bot\\}$ where $\mathbb{N}$ is
the set of natural numbers, $\bot\in V$, and if $(p,n)\in V$ then for all
$n^{\prime}\leq n$, $(p,n^{\prime})\in V$;

  2. 2.

$E_{\\_}R,E_{\\_}W\subseteq V\times\mathcal{R}\times V$ where
$(v^{\prime},r,v),(v^{\prime\prime},r,v)\in E_{\\_}R\cup E_{\\_}W$ implies
$v^{\prime}=v^{\prime\prime}$;

  3. 3.

$E_{\\_}R\cap E_{\\_}W=\varnothing$ and $(V,E_{\\_}R\uplus E_{\\_}W)$ is a DAG
with the finite set of nodes $V$;

  4. 4.

$(v^{\prime},r,v)\in E_{\\_}W$ and $v^{\prime}\not=\bot$ imply
$(v^{\prime\prime},r,v^{\prime})\in E_{\\_}W$; and

  5. 5.

$(v,r,v^{\prime}),(v,r,v^{\prime\prime})\in E_{\\_}W$ implies
$v^{\prime}=v^{\prime\prime}$

$\mathcal{A}$ is the set of all annotation DAGs, and $A_{\\_}{init}$ is
$(\\{\bot\\},\varnothing,\varnothing)$.

We write $v\stackrel{{\scriptstyle r}}{{\rightarrow}}v^{\prime}$ for
$(v,r,v^{\prime})\in E_{\\_}W$ and $v\stackrel{{\scriptstyle
r}}{{\dashrightarrow}}v^{\prime}$ for $(v,r,v^{\prime})\in E_{\\_}R$.
Condition 5 with conditions 3 and 2 ensures that when
$v^{\prime}\stackrel{{\scriptstyle r}}{{\rightarrow}}v$, there is a unique
sequence of $E_{\\_}W$ with the label of $r$ from $\bot$ to $v$:
$\bot\stackrel{{\scriptstyle r}}{{\rightarrow}}v_{\\_}1\stackrel{{\scriptstyle
r}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle r}}{{\rightarrow}}v_{\\_}n=v$.
$\mathsf{last}(r,E_{\\_}W)$ denotes the last node $v$ of such sequence. When
$\mathsf{last}(r,E_{\\_}W)=v\neq\bot$, $v^{\prime}\stackrel{{\scriptstyle
r}}{{\rightarrow}}v$ for a unique $v^{\prime}$ and $v\stackrel{{\scriptstyle
r}}{{\not\rightarrow}}v^{\prime\prime}$ for all $v^{\prime\prime}$.
$\mathsf{last}(r,\varnothing)=\bot$ for all $r\in\mathcal{R}$. Since $V$ is
finite, for $(p,n)\in V$ there is the maximum number for process $p$ if such
$(p,n)$ exists. Given $V\subseteq\mathsf{PID}\times\mathbb{N}\cup\\{\bot\\}$,
we write $\mathsf{max}_{\\_}p(V)$ for $max_{\\_}{(p,n)\in V}\;n$ for some
$(p,n)\in V$. $\mathsf{max}_{\\_}p(V)=-1$ when $(p,n)\notin V$ for all $n$.

######  Definition 2.

For $A_{\\_}1,A_{\\_}2\in\mathcal{A}$,
$A_{\\_}1=(V_{\\_}1,{E_{\\_}R}_{\\_}1,{E_{\\_}W}_{\\_}1)\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}A_{\\_}2=(V_{\\_}2,{E_{\\_}R}_{\\_}2,{E_{\\_}W}_{\\_}2)$
if

  1. 1.

$V_{\\_}2=V_{\\_}1\cup\\{v\\}$;

  2. 2.

${E_{\\_}R}_{\\_}2={E_{\\_}R}_{\\_}1\cup\\{\mathsf{newedge}(r,{E_{\\_}W}_{\\_}1,v)\;|\;r\in
Rd-Wt\\}$;and

  3. 3.

${E_{\\_}W}_{\\_}2={E_{\\_}W}_{\\_}1\cup\\{\mathsf{newedge}(r,{E_{\\_}W}_{\\_}1,v)\;|\;r\in
Wt\\}$

where $v=(p,\mathsf{max}_{\\_}p(V_{\\_}1)+1)$ and
$\mathsf{newedge}(r,E_{\\_}W,v)=(\mathsf{last}(r,E_{\\_}W),r,v)$.

Given $O\subseteq\mathsf{PID}\times 2^{\mathcal{R}}\times 2^{\mathcal{R}}$,
$A\xrightleftharpoons{O}_{\mathrm{ann}}^{+}A^{\prime}$ when for some
$(p_{\\_}i,Rd_{\\_}i,Wt_{\\_}i)\in O$, there exists a sequence of $A_{\\_}i$
such that
$A_{\\_}0\xrightleftharpoons{p_{\\_}1,Rd_{\\_}1,Wt_{\\_}1}_{\mathrm{ann}}A_{\\_}1\cdots\xrightleftharpoons{p_{\\_}n,Rd_{\\_}n,Wt_{\\_}n}_{\mathrm{ann}}A_{\\_}n=A^{\prime}$.
We write $A\xrightleftharpoons{O}_{\mathrm{ann}}^{\ast}A^{\prime}$ if
$A=A^{\prime}$ or $A\xrightleftharpoons{O}_{\mathrm{ann}}^{+}A^{\prime}$.

Intuitively, the forward (left-to-right) relation of
$A_{\\_}1=(V_{\\_}1,E_{\\_}{R1},{E_{\\_}W}_{\\_}1)\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}A_{\\_}2$
is to add a fresh node $v$ and edges $\mathsf{newedge}(r,{E_{\\_}W}_{\\_}1,v)$
for $r\in Rd\cup Wt$ to $A_{\\_}1$ for process $p$ to execute forwards a basic
block $b\in\mathsf{PB}(p)$ with $\mathsf{read}(b)=Rd$ and
$\mathsf{write}(b)=Wt$. $v$ presents the new causality created by executing
process $p$ in the forward direction. The new node has the causality to update
$Wt$ from $(p,\mathsf{max}_{\\_}p(V_{\\_}1))$ that presents the newest
causality in $A_{\\_}1$ by $p$ in forward. To update the causality, the edges
$\mathsf{newedge}(r,{E_{\\_}W}_{\\_}1,v)$ for $r\in Wt$ are added to
${E_{\\_}W}_{\\_}1$. The edges $\mathsf{newedge}(r,{E_{\\_}W}_{\\_}1,v)$ for
$r\in Rd-Wt$ from the newest causality for $r$ at that moment are added to
${E_{\\_}R}_{\\_}1$ to show that the update for $v$ depends on such $r$.

The backward (right-to-left) relation is to remove a node and edges from
$A_{\\_}2$. The node $v$ to be removed has to be the newest causality of a
process and does not depend on other causalities. It is shown that such a node
always exists in an annotation DAG in
$\\{A\;|\;A_{\\_}{init}\xrightleftharpoons{O}_{\mathrm{ann}}^{+}A\\}$ as
below.

######  Proposition 1.

For
$(V,E_{\\_}R,E_{\\_}W)\in\\{A\;|\;A_{\\_}{init}\xrightleftharpoons{\quad}_{\mathrm{ann}}^{+}A\\}$,
there exists a node $v\in V$ such that $v^{\prime}\stackrel{{\scriptstyle
r}}{{\dashrightarrow}}v$ implies $v^{\prime}=\mathsf{last}(r,E_{\\_}W)$; and
no outgoing edge from $v$.

Moreover,
$\mathcal{A}^{O}_{\\_}{comp}=\\{A\;|\;A_{\\_}{init}\xrightleftharpoons{O}_{\mathrm{ann}}^{\ast}A\\}$
is closed by $\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}$ where $(p,Rd,Wt)\in
O$. Obviously, $A\in\mathcal{A}_{\\_}{comp}$ implies
$A^{\prime}\in\mathcal{A}^{O}_{\\_}{comp}$ when
$A\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}A^{\prime}$ for some
$(p,Rd,Wt)\in O$ by definition.

######  Proposition 2.

For
$A\in\\{A^{\prime}\;|\;A_{\\_}{init}\xrightleftharpoons{O}_{\mathrm{ann}}^{+}A^{\prime}\\}$,
there exists $A^{\prime\prime}\in\mathcal{A}^{O}_{\\_}{comp}$ such that
$A^{\prime\prime}\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}A$ with
$(p,Rd,Wt)$ $\in O$.

###  3.2 Operational semantics controlled by Annotation DAG

######  Definition 3.

The operational semantics controlled by annotation DAG over program
configurations $(C,A)\xrightleftharpoons{p,Rd,Wt}(C^{\prime},A^{\prime})$ is
defined by:

$C\xrightleftharpoons{p,Rd,Wt}_{\mathrm{{prog}}}C^{\prime}$
$A\xrightleftharpoons{p,Rd,Wt}_{\mathrm{{ann}}}A^{\prime}$ ProgAnn
$(C,A)\xrightleftharpoons{p,Rd,Wt}(C^{\prime},A^{\prime})$

where $p\in\mathsf{PID}$ and $Rd,Wt\subseteq\mathcal{R}$.

The program computation with annotation is a sequence of
$(C_{\\_}i,A_{\\_}i)\xrightleftharpoons{p_{\\_}i,Rd_{\\_}i,Wt_{\\_}i}_{\mathrm{\quad}}(C_{\\_}{i+1},A_{\\_}{i+1})$
($i\geq 0$) beginning with
$(C_{\\_}0,A_{\\_}0)=(C_{\\_}{init},A_{\\_}{init})$.

We illustrate the behavior controlled by the annotation DAG for the simple
example of the previous section. Starting from the initial
configuration,$(C_{\\_}0,A_{\\_}0)=((Pg,\rho_{\\_}0,\sigma_{\\_}0,[(\varepsilon\mapsto(\texttt{main},\texttt{begin}))]),(\\{\bot\\},\varnothing,\\\
\varnothing))$, it ends up with $(C_{\\_}8,A_{\\_}8)=(P_{\\_}g,[x,y,z\mapsto
2,1,1],\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{main},\texttt{end})])$.

##### Forward accumulation of causality

We present the construction of annotation DAGs as follows:

  * (F1)

After process $\varepsilon$ executes $b_{\\_}1$ and $b_{\\_}2$,
$A_{\\_}2=(\\{\bot,(\varepsilon,0),(\varepsilon,1)\\},\varnothing,\varnothing)$;

  * (F2)

The call statement in $b_{\\_}2$ forks three subprocesses. Then, process $1$
executes $b_{\\_}4$, $(1,0)$ is added to $V$ and
$\bot\stackrel{{\scriptstyle\texttt{x}}}{{\rightarrow}}(1,0)$ is added since
$\mathsf{read}(b_{\\_}4)=\mathsf{write}(b_{\\_}4)=\\{\texttt{x}\\}$ to make
$A_{\\_}3$, meaning x is updated by the initial x, and the store is updated as
$[\texttt{x},\texttt{y},\texttt{z}\mapsto 1,0,0]$.

  * (F3)

Next, process $2$ executes $b_{\\_}6$ where
$\mathsf{read}(b_{\\_}6)=\\{\texttt{x},\texttt{y}\\}$ and
$\mathsf{write}(b_{\\_}6)=\\{\texttt{y}\\}$.
$\xrightleftharpoons{2,\\{\texttt{x},\texttt{y}\\},\\{\texttt{y}\\}}_{\mathrm{ann}}$
adds a fresh node $(2,0)$,
$\bot\stackrel{{\scriptstyle\texttt{y}}}{{\rightarrow}}(2,0)$, and
$(1,0)\stackrel{{\scriptstyle\texttt{x}}}{{\dashrightarrow}}(2,0)$. The
causality of $(2,0)$ means $y$ is updated by the initial y and x of $(1,0)$ to
make $A_{\\_}4$.

  * (F4)

Then, process $3$ executes $b_{\\_}7$ where
$\mathsf{read}(b_{\\_}7)=\\{\texttt{x},\texttt{z}\\}$ and
$\mathsf{write}(b_{\\_}7)=\\{\texttt{z}\\}$.
$\xrightleftharpoons{3,\\{\texttt{x},\texttt{z}\\},\\{\texttt{z}\\}}_{\mathrm{ann}}$
adds $(3,0)$, $\bot\stackrel{{\scriptstyle\texttt{z}}}{{\rightarrow}}(3,0)$,
and $(1,0)\stackrel{{\scriptstyle\texttt{x}}}{{\dashrightarrow}}(3,0)$, to
make $A_{\\_}5$ shown in figure 4 (a), meaning the causality at $(3,0)$ to
update the initial z using the initial z and x of $(1,0)$.

  * (F5)

At last, process $1$ executes $b_{\\_}5$ where
$\mathsf{read}(b_{\\_}5)=\mathsf{write}(b_{\\_}5)=\\{\texttt{x}\\}$.
$\xrightleftharpoons{1,\\{\texttt{x}\\},\\{\texttt{x}\\}}_{\mathrm{ann}}$ just
adds $(1,1)$ and
$(1,0)\stackrel{{\scriptstyle\texttt{x}}}{{\rightarrow}}(1,1)$ to form
$A_{\\_}6$ shown in figure 4 (b), meaning x is updated by x of $(1,0)$.

  * (F6)

No more causality is created after merging the subprocesses. Just the relation
adds $(\varepsilon,2)$ and $(\varepsilon,3)$ with no edges to form $A_{\\_}8$
shown in figure 4 (c).

(a)  (b)

(c)  (d)

(e)

Figure 4: Annotation DAGs along with forward execution

##### Backward rollback of causality

The following is the summary of the corresponding backward execution.

  * (B1)

The removable nodes of $A_{\\_}8$ are $\\{(\varepsilon,3),(1,1)\\}$. Here,
$C_{\\_}8$ specifies $\varepsilon$ to remove $(\varepsilon,3)$ followed by
removing $(\varepsilon,2)$ back to $(C_{\\_}6,A_{\\_}6)$, where
$C_{\\_}6=(Pg,[\texttt{x},\texttt{y},\texttt{z}\mapsto
2,1,1],\sigma_{\\_}0,[\varepsilon\mapsto(\texttt{l2},\texttt{run}),1\mapsto(\texttt{sub0},\texttt{end}),2\\\
\mapsto(\texttt{sub1},\texttt{end}),3\mapsto(\texttt{sub2},\texttt{end})])$

  * (B2)

$C_{\\_}6$ may reverse any subprocess, but $A_{\\_}6$ allows only to remove
$(1,1)$ by $\xrightleftharpoons{p,Rd,Wt}_{\mathrm{ann}}$ to obtain $A_{\\_}5$.

  * (B3)

After removing $(1,1)$ and
$(1,0)\stackrel{{\scriptstyle\texttt{x}}}{{\rightarrow}}(1,1)$ from
$A_{\\_}6$, we obtain $A_{\\_}5$ whose removable nodes are $(2,0)$ and
$(3,0)$. $(1,0)$ is not removable since $(1,0)$ has two outgoing edges,
although $(1,0)=\mathsf{last}(\texttt{x},E_{\\_}W)$.

  * (B4)

$C_{\\_}5$ may reverse either process $2$ or process $3$, and let process $2$
reverse to become $C^{\prime}_{\\_}4$. Then, remove
$\bot\stackrel{{\scriptstyle y}}{{\rightarrow}}(2,0)$ and
$(1,0)\stackrel{{\scriptstyle x}}{{\dashrightarrow}}(2,0)$ to obtain
$A^{\prime}_{\\_}4$ and $[x,y,z\mapsto 1,0,1]$ as the store $\rho$. Note that
$(C^{\prime}_{\\_}4,A^{\prime}_{\\_}4)$ did not appear in the forward
execution.

  * (B5)

From $(C^{\prime}_{\\_}4,A^{\prime}_{\\_}4)$, process $3$ is reversed to
remove $(3,0)$, $\bot\stackrel{{\scriptstyle\texttt{z}}}{{\rightarrow}}(3,0)$,
and $(1,0)\stackrel{{\scriptstyle\texttt{x}}}{{\dashrightarrow}}(3,0)$ to
obtain $A_{\\_}3$ and $[\texttt{x},\texttt{y},\texttt{z}\mapsto 1,0,0]$.

  * (B6)

Then, process $1$ is reversed by removing $(1,0)$ and
$\bot\stackrel{{\scriptstyle\texttt{x}}}{{\rightarrow}}(1,0)$ to obtain
$A_{\\_}2=(\\{\bot,(\varepsilon,0),(\varepsilon,1)\\},\varnothing,\\\
\varnothing)$.

  * (B7)

At last, process $\varepsilon$ reverses $b_{\\_}2$ and $b_{\\_}1$ to obtain
$(C_{\\_}{init},A_{\\_}{init})$.

Figure 5: Annotation DAGs in backward execution

In (B4) step, there are two possibilities of reversing process 3 or process 2.
In the above, $A_{\\_}5$ is reversed by process 2 to $A^{\prime}_{\\_}4$
followed by process 3.

For a CRIL program $Pg$, let $B$ be the basic blocks in $Pg$. Let
$O=\mathsf{PID}\times\bigcup_{\\_}{b\in
B}\mathsf{read}(b)\times\bigcup_{\\_}{b\in B}\mathsf{write}(b)$. Proposition 2
ensures there is always a removable node along with removable edges.

###  3.3 Properties for reversibility

We show that the operational semantics controlled by annotation DAG has proper
properties for reversibility. We focus on the following two properties that
are considered fundamental properties for reversibility [14].

Causal Safety (CS):

An action can not be reversed until any actions caused by it have been
reversed.

Causal Liveness (CL):

We should allow actions to reverse in any order compatible with Causal Safety,
not necessarily the exact inverse of the forward order.

[14] shows that those properties hold in an LTSI (LTS with Independence)
provided that a small number of axioms are valid in the LTSI. We shall follow
this approach by defining LTS from
$\xrightleftharpoons{p,Rd,Wt}_{\mathrm{\quad}}$ and add the independence
relation to have the LTSI for the CRIL behavior. We will then show that the
axioms for CS and CL hold.

######  Definition 4.

$(\mathcal{C}\times\mathcal{A},\mathsf{Lab},\rightharpoonup)$ is the forward
LTS for CRIL where:

  * •

$\mathsf{Lab}=\mathsf{PID}\times 2^{\mathcal{R}}\times 2^{\mathcal{R}}$; and

  * •

$(C,A)\xrightharpoonup{(p,Rd,Wt)}(C^{\prime},A^{\prime})$ if
$(C,A)\xrightleftharpoons{p,Rd,Wt}_{\mathrm{\quad}}(C^{\prime},A^{\prime})$

######  Definition 5.

The (combined) LTS for CRIL is
$(\mathcal{C}\times\mathcal{A},\mathsf{Lab}\uplus\underline{\mathsf{Lab}},\rightarrow)$
where:

  * •

$\underline{\mathsf{Lab}}=\\{\underline{(p,Rd,Wt)}\;|\;(p,Rd,Wt)\in\mathsf{Lab}\\}$;
and

  * •

For $a\in\mathsf{Lab}$, $(C,A)\stackrel{{\scriptstyle
a}}{{\rightarrow}}(C^{\prime},A^{\prime})$ iff
$(C,A)\xrightharpoonup{a}(C^{\prime},A^{\prime})$, and
$(C,A)\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}(C^{\prime},A^{\prime})$
iff $(C^{\prime},A^{\prime})\stackrel{{\scriptstyle a}}{{\rightarrow}}(C,A)$.

$\mathsf{Lab}\uplus\underline{\mathsf{Lab}}$ is ranged over by
$\alpha,\beta,\cdots$, and $\mathsf{Lab}$ by $a,b,\cdots$.
$\mathsf{und}:\mathsf{Lab}\uplus\underline{\mathsf{Lab}}\rightarrow\mathsf{Lab}$
where $\mathsf{und}({a})=a$ and $\mathsf{und}({\underline{a}})=a$.
$\underline{\underline{a}}=a$. Given $t:P\stackrel{{\scriptstyle
a}}{{\rightarrow}}Q$, $\underline{t}$ is for
$Q\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}P$.

For CRIL, the independence of transitions is defined as the independent memory
update among concurrent processes. The processes running concurrently are not
in the subprocess relation. Note that as pid $p\cdot 1$, $p\cdot 2$, $\cdots$
are assigned to the subprocesses of the process with pid of $p$. The process
with the pid of $p$ is concurrent to the process with the pid of $q$ if
$p\not\preceq q$ and $q\not\preceq p$. Hence, we give the dependence relation
for labels as follows.

######  Definition 6.

For $\alpha,\beta\in\mathsf{Lab}\uplus\underline{\mathsf{Lab}}$ such that
$\mathsf{und}({\alpha})=(p_{\\_}1,Rd_{\\_}1,Wt_{\\_}1)$ and
$\mathsf{und}({\beta})=(p_{\\_}2,Rd_{\\_}2,Wt_{\\_}2)$, $\alpha\
\mathrel{\iota}_{\mathrm{lab}}\ \beta$ iff

$p_{\\_}1\not\preceq p_{\\_}2\ \wedge\ p_{\\_}2\not\preceq p_{\\_}1\ \wedge\
Rd_{\\_}1\cap Wt_{\\_}2=\varnothing\ \wedge Rd_{\\_}2\cap
Wt_{\\_}1=\varnothing$

The independence of transitions in LTS is defined as the transitions with
independent labels. We define the Labeled Transition System with Independent
transitions as the operational semantics of CRIL.

######  Definition 7.

For
$t:(C_{\\_}1,A_{\\_}1)\xrightarrow{\alpha}(C_{\\_}1^{\prime},A_{\\_}1^{\prime})$
and
$u:(C_{\\_}2,A_{\\_}2)\xrightarrow{\beta}(C_{\\_}2^{\prime},A_{\\_}2^{\prime})$
in the combined LTS for CRIL, $t$ and $u$ are independent of each other,
written as $t\ \mathrel{\iota}\ u$ if $\alpha\ \mathrel{\iota}_{\mathrm{lab}}\
\beta$.

$(\mathcal{C}\times\mathcal{A},\mathsf{Lab}\uplus\underline{\mathsf{Lab}},\rightarrow,\mathrel{\iota})$
is the LTS of CRIL with independence.

In the sequel, we write ‘$\mbox{\it LTSI}_{CRIL}$’ for the LTS of CRIL with
independence.

####  3.3.1 Basic properties for reversibility

We take the axiomatic approach of [14], where the combination of the basic
properties gives the proper reversibility. The first step is to show that the
$\mbox{\it LTSI}_{CRIL}$ is pre-reversible. For this purpose, we show
$\mbox{\it LTSI}_{CRIL}$ satisfies the following axioms: “Square Property
(SP)”, “Backward Transitions are Independent (BTI)”, “Well-Foundedness (WF)”,
and “Coinitial Propagation of Independence (CPI)”.

##### Square Property(SP)

For $a\in\mathsf{Lab}$, when $C\xrightleftharpoons{\ \ a\ \
}_{\mathrm{\mathrm{{\ prog\ }}}}C^{\prime}$, we write
$C\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\\_}{\mathrm{\ prog\
}}C^{\prime}$ and
$C^{\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\\_}{\mathrm{\
prog\ }}C$. Similarly, when $A\xrightleftharpoons{\ \ a\ \
}_{\mathrm{\mathrm{\ ann\ }}}A^{\prime}$, we write $A\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\\_}{\mathrm{\ ann\ }}A^{\prime}$ and
$A^{\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\\_}{\mathrm{\
ann\ }}A$.

By the definition of the independence transitions, the square property of the
$\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\\_}{\mathrm{\ prog\ }}$ is
immediately shown.

######  Proposition 3.

Suppose $C\xrightarrow{\alpha}_{\\_}{\mathrm{{prog}}}C^{\prime}$,
$C\xrightarrow{\beta}_{\\_}{\mathrm{{prog}}}C^{\prime\prime}$, and
$\alpha\mathrel{\iota}_{\mathrm{lab}}\beta$. Then there are the cofinal
transitions
$C^{\prime}\xrightarrow{\beta}_{\\_}{\mathrm{{prog}}}C^{\prime\prime\prime}$
and
$C^{\prime\prime}\xrightarrow{\alpha}_{\\_}{\mathrm{{prog}}}C^{\prime\prime\prime}$.

For annotation DAGs, we need to trace the difference of nodes and edges added
or deleted by $\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}$
to show the square property. We use the following notation to present
differences in annotation DAGs:

  * For $o:(V,E_{\\_}R,E_{\\_}W)\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}(V^{\prime},E^{\prime}_{\\_}R,E^{\prime}_{\\_}W)$, $\mathsf{diff}(o)=\begin{cases}(V^{\prime}-V,E^{\prime}_{\\_}R-E_{\\_}R,E^{\prime}_{\\_}W-E_{\\_}W)&\mbox{if }\alpha\in\mathsf{Lab},\\\ (V-V^{\prime},E_{\\_}R-E^{\prime}_{\\_}R,E_{\\_}W-E^{\prime}_{\\_}W)&\mbox{if }\alpha\in\underline{\mathsf{Lab}}\end{cases}$

  * $(V,E_{\\_}R,E_{\\_}W)\odot^{\alpha}(\Delta V,{\Delta E_{\\_}R},{\Delta E_{\\_}W})=\begin{cases}(V\cup\Delta V,E_{\\_}R\cup{\Delta E_{\\_}R},E_{\\_}W\cup{\Delta E_{\\_}W})&\mbox{if }\alpha\in\mathsf{Lab},\\\ (V-\Delta V,E_{\\_}R-{\Delta E_{\\_}R},E_{\\_}W-{\Delta E_{\\_}W})&\mbox{if }\alpha\in\underline{\mathsf{Lab}}\end{cases}$

######  Proposition 4.

Let
$\mathsf{diff}(A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=(\Delta
V^{\alpha},\Delta E_{\\_}R^{\alpha},\Delta E_{\\_}W^{\alpha})$ and
$\mathsf{diff}(A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime})=(\Delta
V^{\beta},\Delta E_{\\_}R^{\beta},\Delta E_{\\_}W^{\beta})$ with
$\alpha\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Then, $\Delta
V^{\alpha}\cap\Delta V^{\beta}=\Delta E_{\\_}{R}^{\alpha}\cap\Delta
E^{\beta}_{\\_}{R}=\Delta E^{\alpha}_{\\_}{W}\cap\Delta
E^{\beta}_{\\_}{W}=\varnothing$.

###### Proof.

For some $v_{\\_}\alpha$ and $v_{\\_}\beta$, $\Delta
V^{\alpha}=\\{v_{\\_}\alpha\\}$ and $\Delta V^{\beta}=\\{v_{\\_}\beta\\}$.
$\alpha\mathrel{\iota}_{\\_}\mathrm{lab}\beta$ implies $v_{\\_}\alpha\neq
v_{\\_}\beta$. All the edges of $\Delta E_{\\_}{R}^{\alpha}\uplus\Delta
E^{\alpha}_{\\_}{W}$ come into $v_{\\_}\alpha$ and all the edges of $\Delta
E_{\\_}{R}^{\beta}\uplus\Delta E^{\beta}_{\\_}{W}$ come into $v_{\\_}\beta$.
Therefore, $\Delta V^{\alpha}\cap\Delta V^{\beta}=\Delta
E_{\\_}{R}^{\alpha}\cap\Delta E^{\beta}_{\\_}{R}=\Delta
E^{\alpha}_{\\_}{W}\cap\Delta E^{\beta}_{\\_}{W}=\varnothing$. ∎

######  Proposition 5.

Suppose $A\stackrel{{\scriptstyle a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}$
and
$A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime}$
with $a\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Then there is
$A^{\prime\prime\prime}$ such that $A^{\prime\prime}\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$ and
$\mathsf{diff}(A\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=\mathsf{diff}(A^{\prime\prime}\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime})$.

###### Proof.

Assume $A=(V,E_{\\_}R,E_{\\_}W)$,
$A^{\prime\prime}=(V^{\prime\prime},E^{\prime\prime}_{\\_}R,E^{\prime\prime}_{\\_}W)$,
and $a=(p_{\\_}a,Rd_{\\_}a,Wt_{\\_}a)$.
$A^{\prime\prime}\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$ for some
$A^{\prime\prime\prime}$ since $a\in\mathsf{Lab}$.
$a\mathrel{\iota}_{\\_}\mathrm{lab}\beta$ implies that
$\mathsf{max}_{\\_}{p_{\\_}a}(A)=\mathsf{max}_{\\_}{p_{\\_}a}(A^{\prime\prime})$
and $\mathsf{last}(r,E_{\\_}W)=\mathsf{last}(r,E^{\prime\prime}_{\\_}W)$ for
$r\in Rd_{\\_}a$. Therefore, $\mathsf{diff}(A\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=\mathsf{diff}(A^{\prime\prime}\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime})$. ∎

######  Proposition 6.

Suppose
$A\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}$
and
$A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime}$
with $\underline{a}\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Then there is
$A^{\prime\prime\prime}$ such that
$A^{\prime\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$
and
$\mathsf{diff}(A\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=\mathsf{diff}(A^{\prime\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime})$.

###### Proof.

Assume
$\mathsf{diff}(A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime})=(\Delta
V^{\beta},\Delta E_{\\_}R^{\beta},\Delta E_{\\_}W^{\beta})$, and
$a=(p_{\\_}a,Rd_{\\_}a,Wt_{\\_}a)$. Let
$v=(p_{\\_}a,\mathsf{max}_{\\_}{p_{\\_}a}(V))$.
$\underline{a}\mathrel{\iota}_{\\_}\mathrm{lab}\beta$ implies that no edges in
$\Delta E^{\beta}_{\\_}R\uplus\Delta E^{\beta}_{\\_}W$ go out from $v$ and
$v^{\prime}$ such that $v^{\prime}\stackrel{{\scriptstyle
r}}{{\dashrightarrow}}v$ in $A$. Therefore,
$A^{\prime\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$
for some $A^{\prime\prime\prime}$.
$\underline{a}\mathrel{\iota}_{\\_}\mathrm{lab}\beta$ and
$\underline{a}\in\underline{\mathsf{Lab}}$ derive
$\mathsf{diff}(A\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=\mathsf{diff}(A^{\prime\prime}\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime})$.
∎

######  Proposition 7.

Suppose
$A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}$ and
$A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime}$
with $\alpha\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Then
$A^{\prime\prime}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$,
where
$A^{\prime\prime\prime}=A^{\prime\prime}\odot^{\alpha}\mathsf{diff}(A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})$.

###### Proof.

Proposition 5 and 6 derive
$A^{\prime\prime}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$.
∎

######  Proposition 8.

Suppose $A\xrightarrow{\alpha}_{\\_}{\mathrm{ann}}A^{\prime}$,
$A\xrightarrow{\beta}_{\\_}{\mathrm{ann}}A^{\prime\prime}$, and
$\alpha\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Then there are the cofinal
transitions
$A^{\prime}\xrightarrow{\beta}_{\\_}{\mathrm{ann}}A^{\prime\prime\prime}$ and
$A^{\prime\prime}\xrightarrow{\alpha}_{\\_}{\mathrm{ann}}A^{\prime\prime\prime}$.

###### Proof.

By proposition 4,
$\mathsf{diff}(A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})$
and
$\mathsf{diff}(A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime})$
are disjoint if $\alpha\mathrel{\iota}_{\\_}\mathrm{lab}\beta$. Hence, the
order of addition and deletion to/from $A$ does not affect the result.
Therefore,
$(A\odot^{\alpha}\mathsf{diff}(A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}))\odot^{\beta}\mathsf{diff}(A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime})=(A\odot^{\beta}\mathsf{diff}(A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime}))\odot^{\alpha}\mathsf{diff}(A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime})=A^{\prime\prime\prime}$.
By proposition 7, we have
$A\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$
and
$A\stackrel{{\scriptstyle\beta}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime\prime\prime}$
hold for such $A^{\prime\prime\prime}$. ∎

Combining proposition 3 with proposition 8 by ProgAnn, the square property
holds.

######  Lemma 1 (Square Property).

Whenever $t:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\alpha}{(C_{\\_}Q,A_{\\_}Q)}$,
$u:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\beta}{(C_{\\_}R,A_{\\_}R)}$, and
$t\mathrel{\iota}u$, then there are cofinal transitions
$u^{\prime}:{(C_{\\_}Q,A_{\\_}Q)}\xrightarrow{\beta}{(C_{\\_}S,A_{\\_}S)}$,
and
$t^{\prime}:{(C_{\\_}R,A_{\\_}R)}\xrightarrow{\alpha}{(C_{\\_}S,A_{\\_}S)}$.

##### Backward Transitions are Independent (BTI)

BTI is useful for reversibility because an available backward transition does
not depend on any other backward transition. In CRIL, a label of $\mbox{\it
LTSI}_{CRIL}$ gives the information to establish BTI.

######  Lemma 2 (Backward Transitions are Independent).

Whenever
$t:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\underline{a}}{(C_{\\_}Q,A_{\\_}Q)}$,
$u:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\underline{b}}{(C_{\\_}R,A_{\\_}R)}$, and
$t\neq u$, then $t\mathrel{\iota}u$.

###### Proof.

Assume $A_{\\_}P=(V,E_{\\_}R,E_{\\_}W)$, $a=(p_{\\_}a,Rd_{\\_}a,Wt_{\\_}a)$,
and $b=(p_{\\_}b,Rd_{\\_}b,Wt_{\\_}b)$. Let
$v_{\\_}a=(p_{\\_}a,\mathsf{max}_{\\_}{p_{\\_}a}(V))$ and
$v_{\\_}b=(p_{\\_}b,\mathsf{max}_{\\_}{p_{\\_}b}(V))$.

Assume $p_{\\_}a\preceq p_{\\_}b$. Then $p_{\\_}a=p_{\\_}b$ holds from the
operational semantics. $p_{\\_}a=p_{\\_}b$ derives $t=u$, which contradicts
$t\neq u$. Therefore, $p_{\\_}a\not\preceq p_{\\_}b$ holds. Similarly,
$p_{\\_}b\not\preceq p_{\\_}a$ also holds.

Assume $Rd_{\\_}a\cap Wt_{\\_}b\neq\varnothing$. There exists $r\in
Rd_{\\_}a\cap Wt_{\\_}b$. If $r\in Wt_{\\_}a$, then
$\mathsf{last}(r,E_{\\_}W)=v_{\\_}a$ and $\mathsf{last}(r,E_{\\_}W)=v_{\\_}b$.
Therefore $p_{\\_}a=p_{\\_}b$, however it contradicts $p_{\\_}a\not\preceq
p_{\\_}b$. If $r\not\in Wt_{\\_}a$, then
$\mathsf{last}(r,E_{\\_}W)\stackrel{{\scriptstyle
r}}{{\dashrightarrow}}v_{\\_}a\in E_{\\_}R$. $r\in Wt_{\\_}b$ derives
$\mathsf{last}(r,E_{\\_}W)=v_{\\_}b$. Therefore
$v_{\\_}b\stackrel{{\scriptstyle r}}{{\dashrightarrow}}v_{\\_}a\in E_{\\_}R$,
however it contradicts that no edges go out from $v_{\\_}b$ derived from $u$.
Therefore $Rd_{\\_}a\cap Wt_{\\_}b=\varnothing$. Similarly, $Rd_{\\_}b\cap
Wt_{\\_}a=\varnothing$ also holds. ∎

##### Well-Foundedness (WF)

For a backward transition
$(C,A)\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}(C^{\prime},A^{\prime})$,
the number of nodes of $A^{\prime}$ is strictly less than that of $A$. Since
the number of vertices of annotation DAG is finite, it is not possible to
remove vertices infinitely.

##### Coinitial Propagation of Independence (CPI)

Given a commuting square with independence at one corner, CPI allows us to
deduce independence between coinitial transitions at the other three corners.

######  Lemma 3 (Coinitial Propagation of Independence).

Suppose $t:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\alpha}{(C_{\\_}Q,A_{\\_}Q)}$,
$u:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\beta}{(C_{\\_}R,A_{\\_}R)}$,
$u^{\prime}:{(C_{\\_}Q,A_{\\_}Q)}\xrightarrow{\beta}{(C_{\\_}S,A_{\\_}S)}$,
$t^{\prime}:{(C_{\\_}R,A_{\\_}R)}\xrightarrow{\alpha}{(C_{\\_}S,A_{\\_}S)}$,
and $t\mathrel{\iota}u$. Then $u^{\prime}\mathrel{\iota}\underline{t}$.

###### Proof.

$t\mathrel{\iota}u$ implies $\alpha\mathrel{\iota}_{\mathrm{lab}}\beta$. Since
$\beta\mathrel{\iota}_{\mathrm{lab}}\underline{\alpha}$,
$u^{\prime}\mathrel{\iota}\underline{t}$. ∎

####  3.3.2 Events

The properties above make $\mbox{\it LTSI}_{CRIL}$ pre-reversible. Next, we
check if $\mbox{\it LTSI}_{CRIL}$ can derive events for establishing
reversibility. Following [14], events in $\mbox{\it LTSI}_{CRIL}$ are derived
as an equivalence over transitions.

######  Definition 8.

Let $\sim$ be the smallest equivalence relation on transitions satisfying: if
$t:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\alpha}{(C_{\\_}Q,A_{\\_}Q)}$,
$u:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\beta}{(C_{\\_}R,A_{\\_}R)}$,
$u^{\prime}:{(C_{\\_}Q,A_{\\_}Q)}\xrightarrow{\beta}{(C_{\\_}S,A_{\\_}S)}$,
$t^{\prime}:{(C_{\\_}R,A_{\\_}R)}\xrightarrow{\alpha}{(C_{\\_}S,A_{\\_}S)}$,
and $t\mathrel{\iota}u$, then $t\sim t^{\prime}$. The equivalence classes of
forward transitions $[(C_{\\_}P,A_{\\_}P)\stackrel{{\scriptstyle
a}}{{\rightarrow}}(C_{\\_}Q,A_{\\_}Q)]$, are the events. The equivalence
classes of backward transitions
$[(C_{\\_}P,A_{\\_}P)\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}(C_{\\_}Q,A_{\\_}Q)]$,
are the reverse events.

Given
$\gamma=\alpha_{\\_}1\cdots\alpha_{\\_}n\in(\mathsf{Lab}\uplus\underline{\mathsf{Lab}})^{\ast}$,
a sequence of transitions
$(C_{\\_}0,A_{\\_}0)\stackrel{{\scriptstyle\alpha_{\\_}1}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle\alpha_{\\_}n}}{{\rightarrow}}(C_{\\_}n,A_{\\_}n)$
is written as
$s:(C_{\\_}0,A_{\\_}0)\stackrel{{\scriptstyle\gamma}}{{\rightarrow}}_{\\_}\ast(C_{\\_}n,A_{\\_}n)$.

Since the transitions of program configurations in $\mbox{\it LTSI}_{CRIL}$
$\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\\_}{\mathrm{prog}}$ have no
control for reversibility, events are substantially derived from the
operations of annotation DAGs.

######  Definition 9.

Let $\sim_{\\_}{\mathrm{ann}}$ be the smallest equivalence relation over
operations of annotation DAGs satisfying: if
$o_{\\_}1:A_{\\_}P\xrightarrow{\alpha}_{\\_}{\mathrm{ann}}A_{\\_}Q$,
$o_{\\_}2:A_{\\_}P\xrightarrow{\beta}_{\\_}{\mathrm{ann}}A_{\\_}R$,
$o_{\\_}2^{\prime}:A_{\\_}Q\xrightarrow{\beta}_{\\_}{\mathrm{ann}}A_{\\_}S$,
$o_{\\_}1^{\prime}:A_{\\_}R\xrightarrow{\alpha}_{\\_}{\mathrm{ann}}A_{\\_}S$,
and $\alpha\mathrel{\iota}_{\mathrm{lab}}\beta$, then $o_{\\_}1\sim
o^{\prime}_{\\_}1$. $[A\stackrel{{\scriptstyle
a}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}]_{\\_}{\mathrm{ann}}$ and
$[A\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}_{\mathrm{ann}}A^{\prime}]_{\\_}{\mathrm{ann}}$
are the forward and backward equivalence classes by
$\sim_{\\_}{\mathrm{ann}}$.

######  Proposition 9.

For $t:{(C_{\\_}P,A_{\\_}P)}\xrightarrow{\alpha}{(C_{\\_}Q,A_{\\_}Q)}$ and
$t^{\prime}:{(C_{\\_}R,A_{\\_}R)}\xrightarrow{\alpha}{(C_{\\_}S,A_{\\_}S)}$,
the following holds.
$t\sim t^{\prime}$ iff $o\sim_{\\_}{\mathrm{ann}}o^{\prime}$ and
$\exists\gamma.(C_{\\_}P,A_{\\_}P)\stackrel{{\scriptstyle\gamma}}{{\rightarrow}}_{\\_}\ast(C_{\\_}R,A_{\\_}R)$
where
$o:A_{\\_}P\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A_{\\_}Q$
and
$o^{\prime}:A_{\\_}R\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{\mathrm{ann}}A_{\\_}S$.

Intuitively, operations for annotation DAGs are independent if they add or
remove nodes and edges at unrelated places. If
$o_{\\_}1\sim_{\\_}{\mathrm{ann}}o_{\\_}2$, then $o_{\\_}1$ and $o_{\\_}2$ add
or remove the same fragment of annotation DAGs to or from the nodes of the
same causality. In $\mbox{\it LTSI}_{CRIL}$, the equivalence over operations
of annotation DAGs is considered as an event. This shows that events for
reversibility are consistently defined over $\mbox{\it LTSI}_{CRIL}$, meaning
the operational semantics is detailed enough to give the IRE property as
follows, which is necessary for our objectives.

##### Independence Respects Events (IRE)

######  Lemma 4 (Independence Respects Events).

Suppose $t\sim t^{\prime}\mathrel{\iota}u$. Then $t\mathrel{\iota}u$.

###### Proof.

If $t\sim t^{\prime}$, $t$ has the same label as $t^{\prime}$. Then,
$t\mathrel{\iota}u$. ∎

####  3.3.3 Causal Safety and Causal Liveness

Let $\sharp(s,[A\stackrel{{\scriptstyle
a}}{{\rightarrow}}A^{\prime}]_{\\_}{\mathrm{ann}})$ be the number of
occurrences of transitions $t$ in $s$ such that
$t\in[(C,A)\stackrel{{\scriptstyle
a}}{{\rightarrow}}(C^{\prime},A^{\prime})]$, minus the number of occurrences
of transitions $t$ in $s$ such that
$t\in[(C,A)\stackrel{{\scriptstyle\underline{a}}}{{\rightarrow}}(C^{\prime},A^{\prime})]$.

Using the result of [14], the properties of SP(Lemma 1), BTI(Lemma 2), WF,
CPI(Lemma 3), and IRE (Lemma 4) make Causal Safety (CS) and Causal Liveness
(CL) hold. Due to the fact that the causality is stored in the annotation
DAGs, the properties can be stated in $\mbox{\it LTSI}_{CRIL}$ as below.

######  Theorem 1 (Causal Safety).

Whenever $(C_{\\_}P,A_{\\_}P)\xrightarrow{a}(C_{\\_}Q,A_{\\_}Q)$,
$s:(C_{\\_}Q,A_{\\_}Q)\xrightarrow{\gamma}_{\\_}*(C_{\\_}R,A_{\\_}R)$ with
$\sharp(s,[A_{\\_}P\stackrel{{\scriptstyle
a}}{{\rightarrow}}A_{\\_}Q]_{\\_}{\mathrm{ann}})=0$, and
$(C_{\\_}S,A_{\\_}S)\xrightarrow{a}(C_{\\_}R,A_{\\_}R)$ then
$(C_{\\_}P,A_{\\_}P)\stackrel{{\scriptstyle
a}}{{\rightarrow}}(C_{\\_}Q,A_{\\_}Q)\mathrel{\iota}t$ for all $t$ in $s$ such
that $\sharp(s,[A_{\\_}P\stackrel{{\scriptstyle
a}}{{\rightarrow}}A_{\\_}Q]_{\\_}{\mathrm{ann}})>0$.

######  Theorem 2 (Causal Liveness).

Whenever ${(C_{\\_}P,A_{\\_}P)}\xrightarrow{a}{(C_{\\_}Q,A_{\\_}Q)}$,
$s:{(C_{\\_}Q,A_{\\_}Q)}\xrightarrow{\gamma}_{\\_}*{(C_{\\_}R,A_{\\_}R)}$,
$\sharp(s,[A_{\\_}P\stackrel{{\scriptstyle a}}{{\rightarrow}}A_{\\_}Q])=0$,
and ${(C_{\\_}P,A_{\\_}P)}\stackrel{{\scriptstyle
a}}{{\rightarrow}}{(C_{\\_}Q,A_{\\_}Q)}\mathrel{\iota}t:(C,A)\stackrel{{\scriptstyle
b}}{{\rightarrow}}(C^{\prime},A^{\prime})$ for all $t$ in $s$ such that
$\sharp(s,[A\stackrel{{\scriptstyle a}}{{\rightarrow}}A^{\prime}])>0$ with
${(C_{\\_}P,A_{\\_}P)}\stackrel{{\scriptstyle
a}}{{\rightarrow}}{(C_{\\_}Q,A_{\\_}Q)}\sim{(C_{\\_}S,A_{\\_}S)}\stackrel{{\scriptstyle
a}}{{\rightarrow}}{(C_{\\_}R,A_{\\_}R)}$, then we have
${(C_{\\_}S,A_{\\_}S)}\xrightarrow{a}{(C_{\\_}R,A_{\\_}R)}$ with
${(C_{\\_}P,A_{\\_}P)}\stackrel{{\scriptstyle
a}}{{\rightarrow}}{(C_{\\_}Q,A_{\\_}Q)}\sim{(C_{\\_}S,A_{\\_}S)}\stackrel{{\scriptstyle
a}}{{\rightarrow}}{(C_{\\_}R,A_{\\_}R)}$.

Based on these properties, $\mbox{\it LTSI}_{CRIL}$ can be implemented
correctly with the pointers for processes managed by a process map along with
annotation DAGs as the operational semantics of CRIL.

##  4 Example: Airline ticketing

We show a version of the airline ticketing program [6] in CRIL in figure 6.
Two agents attempt to sell three seats of an airline. This program has a data
race for variable seats of

the remaining seats because two agents may check the remaining seats
simultaneously before making sales. Since the data race does not always
happen, it is useful to roll back to the point where checking remaining seats
is insufficient. Here, agent1 and agent2 are used to record the number of
tickets sold by each agent.

Figure 6: An airline ticketing program in CRIL

basic block |  seats |  agent1 |  agent2
---|---|---|---
$(\varepsilon,0)$ |  $b_{\\_}1$ |  3 |  0 |  0
$(\varepsilon,1)$ |  $b_{\\_}2$ |  3 |  0 |  0
$(1,0)$ |  $b_{\\_}4$ |  3 |  0 |  0
$(2,0)$ |  $b_{\\_}9$ |  3 |  0 |  0
$(1,1)$ |  $b_{\\_}5$ |  3 |  0 |  0
$(1,2)$ |  $b_{\\_}6$ |  2 |  0 |  0
$(1,3)$ |  $b_{\\_}7$ |  2 |  1 |  0
$(2,1)$ |  $b_{\\_}{10}$ |  2 |  1 |  0
$(2,2)$ |  $\mathbf{b_{\\_}{11}}$ |  1 |  1 |  0
$(2,3)$ |  $b_{\\_}{12}$ |  1 |  1 |  1
$(2,4)$ |  $\mathbf{b_{\\_}{10}}$ |  1 |  1 |  1
$(1,4)$ |  $\mathbf{b_{\\_}5}$ |  1 |  1 |  1
$(2,5)$ |  $b_{\\_}{11}$ |  0 |  1 |  1
$(1,5)$ |  $b_{\\_}6$ |  -1 |  1 |  1
$(2,6)$ |  $b_{\\_}{12}$ |  -1 |  1 |  2
$(2,7)$ |  $b_{\\_}{10}$ |  -1 |  1 |  2
$(2,8)$ |  $b_{\\_}{13}$ |  -1 |  1 |  2
$(1,6)$ |  $b_{\\_}7$ |  -1 |  2 |  2
$(1,7)$ |  $b_{\\_}5$ |  -1 |  2 |  2
$(1,8)$ |  $b_{\\_}8$ |  -1 |  2 |  2
$(\varepsilon,2)$ |  $b_{\\_}2$ |  -1 |  2 |  2
$(\varepsilon,3)$ |  $b_{\\_}3$ |  -1 |  2 |  2
Table 3: A faulty execution

Table 3 shows a forward execution that ends $\mathtt{seats}=-1$. Figure 7 is
the annotation DAG when terminated at ‘end main’ in $b_{\\_}3$. To investigate
the cause of the data race, we focus on the edges labeled with seats. The
solid edges indicate that seats is written in $(\varepsilon,0)$, $(1,2)$,
$(2,2)$, $(2,5)$, and $(1,5)$.

Figure 7: The annotation DAG after the forward execution with the data race

In particular, seats defined at $(2,2)$ is used to update by processes 2 and 3
to cause the data race. (The steps in bold are involved in the problem.) To
resolve the data race, each value of seats should be checked exactly once,
except for the last value of seats.

Figure 8 shows the airline program where sub1 and sub2 are replaced by those
with the V-P operations. The parameter of the V-P operations works as a
semaphore to check and update seats as a critical region. Figure 9 is the
annotation DAG by the forward execution with sub1 done first once and then
sub2 done twice. Process 1 executes $b^{\prime}_{\\_}5$ setting
$\texttt{semaphore}=1$ at $(1,1)$ first. (sem is for semaphore in the figure.)
This prevents process 2 executing $b^{\prime}_{\\_}{10}$ at $(2,1)$ since
semaphore must be 0. Backwards, $b^{\prime}_{\\_}{14}$ and
$b^{\prime}_{\\_}{15}$ work as V semaphore. In the backward execution, the
order of basic blocks is stored in the annotation DAG. It works as follows:

  * •

The sequence of $\stackrel{{\scriptstyle\texttt{sem}}}{{\rightarrow}}$ is
alternatively from V and P operations in the forward execution.
$\bot\xrightarrow{\texttt{sem}}(1,1)$ is by $b^{\prime}_{\\_}5$ and
$(1,1)\xrightarrow{\texttt{sem}}(1,3)$ by $b^{\prime}_{\\_}{14}$, $\cdots$,
$(1,3)\xrightarrow{\texttt{sem}}(2,1)$ by $b^{\prime}_{\\_}{10}$,
$(2,1)\xrightarrow{\texttt{sem}}(2,3)$ by $b^{\prime}_{\\_}{15}$,$\cdots$.

  * •

When $\texttt{seats}=0$, semaphore is released with no operation.
$(2,7)\xrightarrow{\texttt{sem}}(1,5)\xrightarrow{\texttt{sem}}(1,6)$ by
$b^{\prime}_{\\_}5$ and $b^{\prime}_{\\_}8$ and
$(1,6)\xrightarrow{\texttt{sem}}(2,9)\xrightarrow{\texttt{sem}}(2,10)$ by
$b^{\prime}_{\\_}{10}$ and $b^{\prime}_{\\_}{13}$.

  * •

In backward, sub2 is ready since $(2,10)$ is
$\mathsf{last}(E_{\\_}W,\texttt{sem})$.

  * •

Then, sub1 is done with no operation and $(2,7)$ is P in sub2. The order of V
and P is kept until reaching $\bot$.

Figure 8: An airline ticketing with semaphore

Figure 9: The annotation DAG after the forward execution with semaphore

##  5 Concluding remarks

We have proposed CRIL as a reversible concurrent intermediate language. CRIL
is an extension of RIL [17] to enable running multiple subroutines as
processes running in parallel. CRIL is intended to be fairly low-level in that
each instruction is at a level similar to the three-address codes to mediate
the translation from a high-level program to a machine-oriented code. The
operational semantics of CRIL defined as $\mbox{\it LTSI}_{CRIL}$ is shown to
have the properties of Causal Safety and Causal Liveness under the
independence of concurrent processes and shared memory update. By the result
of [14], $\mbox{\it LTSI}_{CRIL}$ also satisfies other properties: Parabolic
lemma, Causal Consistency, Unique Transition, and Independence of Diamonds.

As related work, [2] provides a compiler from ROOPL++ to PISA [23] with no
intermediate language, where the translation from an object-oriented source
program to the low-level PISA code is a big task. [7] proposes an annotation
to a concurrent imperative program while executing forward, where the
annotation is attached directly to the source program for reversing the
execution. [8] investigates its properties of reversibility. CRIL uses a
similar idea as Hoey’s, but CRIL is at a rather lower level to provide a finer
granularity for detailed analysis in translation, such as optimization. [9]
presents a collection of simple stack machines with a fork and merge
mechanism, where the causality is embedded in the runtime.

For future work, we have focused only on the fundamental properties. We will
investigate further how more properties in reversibility contribute to
behavioral analysis for concurrent programs. Currently, the dependency of the
heap memory M is treated as one memory resource. More detailed dependency is
necessary for practical use. Deriving the optimization technique in the front-
end part of compilers is future work via the reversible version of SSA, such
as RSSA [18] for concurrent imperative programs. CRIL is based on the shared
memory model. Incorporating channel-based communications is also future work
to use for the message-passing model like Erlang [13].

##### Acknowledgement

We thank Dr. Irek Ulidowski of the University of Leicester for giving valuable
suggestions to the draft. We also thank Prof. Nobuko Yoshida of the University
of Oxford, Prof. Hiroyuki Seki, Prof. Koji Nakazawa, and Prof. Yuichi Kaji of
Nagoya University for fruitful discussions. We thank the anonymous reviewers
for providing fruitful comments. This work is supported by JSPS Kakenhi
21H03415.

## References

  * [1]
  * [2] Martin Holm Cservenka, Robert Glück, Tue Haulund & Torben Ægidius Mogensen (2018): _Data Structures and Dynamic Memory Management in Reversible Languages_.  In: Reversible Computation - 10th International Conference, RC 2018, Leicester, UK, September 12-14, 2018, Proceedings, Lecture Notes in Computer Science 11106, Springer, pp. 269–285, 10.1007/978-3-319-99498-7_19.
  * [3] Vincent Danos & Jean Krivine (2004): _Reversible Communicating Systems_.  In: CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, Lecture Notes in Computer Science 3170, Springer, pp. 292–307, 10.1007/978-3-540-28644-8_19.
  * [4] Niklas Deworetzki, Martin Kutrib, Uwe Meyer & Pia-Doreen Ritzke (2022): _Optimizing Reversible Programs_.  In: RC 2022, Lecture Notes in Computer Science 13354, Springer, pp. 224–238, 10.1007/978-3-031-09005-9_16.
  * [5] Lasse Hay-Schmidt, Robert Glück, Martin Holm Cservenka & Tue Haulund (2021): _Towards a Unified Language Architecture for Reversible Object-Oriented Programming_.  In: Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings, Lecture Notes in Computer Science 12805, Springer, pp. 96–106, 10.1007/978-3-030-79837-6_6.
  * [6] James Hoey, Ivan Lanese, Naoki Nishida, Irek Ulidowski & Germán Vidal (2020): _A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs_.  In: Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC1405, Lecture Notes in Computer Science 12070, Springer, pp. 108–127, 10.1007/978-3-030-47361-7_5.
  * [7] James Hoey & Irek Ulidowski (2022): _Reversing an imperative concurrent programming language_.  Sci. Comput. Program. 223, p. 102873, 10.1016/j.scico.2022.102873.
  * [8] James Hoey & Irek Ulidowski (2022): _Towards Causal-Consistent Reversibility of Imperative Concurrent Programs_.  In: Reversible Computation - 14th International Conference, RC 2022, Urbino, Italy, July 5-6, 2022, Proceedings, Lecture Notes in Computer Science 13354, Springer, pp. 213–223, 10.1007/978-3-031-09005-9_15.
  * [9] Takashi Ikeda & Shoji Yuen (2020): _A Reversible Runtime Environment for Parallel Programs_.  In: RC 2020, Lecture Notes in Computer Science 12227, Springer, pp. 272–279, 10.1007/978-3-030-52482-1_18.
  * [10] Martin Kutrib, Uwe Meyer, Niklas Deworetzki & Marc Schuster (2021): _Compiling Janus to RSSA_.  In: Reversible Computation - 13th International Conference, RC 2021, Virtual Event, July 7-8, 2021, Proceedings, Lecture Notes in Computer Science 12805, Springer, pp. 64–78, 10.1007/978-3-030-79837-6_4.
  * [11] Ivan Lanese, Doriana Medic & Claudio Antares Mezzina (2021): _Static versus dynamic reversibility in CCS_.  Acta Informatica 58(1-2), pp. 1–34, 10.1007/s00236-019-00346-6.
  * [12] Ivan Lanese, Claudio Antares Mezzina & Jean-Bernard Stefani (2010): _Reversing Higher-Order Pi_.  In: CONCUR 2010, Lecture Notes in Computer Science 6269, Springer, pp. 478–493, 10.1007/978-3-642-15375-4_33.
  * [13] Ivan Lanese, Naoki Nishida, Adrián Palacios & Germán Vidal (2018): _A theory of reversibility for Erlang_.  J. Log. Algebraic Methods Program. 100, pp. 71–97, 10.1016/j.jlamp.2018.06.004.
  * [14] Ivan Lanese, Iain C. C. Phillips & Irek Ulidowski (2020): _An Axiomatic Approach to Reversible Computation_.  In: Proceedings of FOSSACS 2020, Lecture Notes in Computer Science 12077, Springer, pp. 442–461, 10.1007/978-3-030-45231-5_23.  (The full version is at https://arxiv.org/abs/2307.13360.).
  * [15] Chris Lattner & Vikram S. Adve (2004): _LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation_.  In: 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA, IEEE Computer Society, pp. 75–88, 10.1109/CGO.2004.1281665.
  * [16] Hernán C. Melgratti, Claudio Antares Mezzina & G. Michele Pinna (2021): _A distributed operational view of Reversible Prime Event Structures_.  In: 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, IEEE, pp. 1–13, 10.1109/LICS52264.2021.9470623.
  * [17] Torben Ægidius Mogensen (2015): _Garbage Collection for Reversible Functional Languages_.  In: Reversible Computation - 7th International Conference, RC 2015, Grenoble, France, July 16-17, 2015, Proceedings, Lecture Notes in Computer Science 9138, Springer, pp. 79–94, 10.1007/978-3-319-20860-2_5.
  * [18] Torben Ægidius Mogensen (2015): _RSSA: A Reversible SSA Form_.  In: Perspectives of System Informatics \- 10th International Andrei Ershov Informatics Conference, PSI 2015, Lecture Notes in Computer Science 9609, Springer, pp. 203–217, 10.1007/978-3-319-41579-6_16.
  * [19] Iain Phillips & Irek Ulidowski (2014): _Event Identifier Logic_.  Math. Struct. Comput. Sci. 24(2), 10.1017/S0960129513000510.
  * [20] Iain Phillips & Irek Ulidowski (2015): _Reversibility and asymmetric conflict in event structures_.  J. Log. Algebraic Methods Program. 84(6), pp. 781–805, 10.1016/j.jlamp.2015.07.004.
  * [21] Iain C. C. Phillips & Irek Ulidowski (2007): _Reversing algebraic process calculi_.  J. Log. Algebraic Methods Program. 73(1-2), pp. 70–96, 10.1016/j.jlap.2006.11.002.
  * [22] Irek Ulidowski, Iain Phillips & Shoji Yuen (2018): _Reversing Event Structures_.  New Gener. Comput. 36(3), pp. 281–306, 10.1007/s00354-018-0040-8.
  * [23] Carlin Vieri (1999): _Reversible computer engineering and architecture_.  Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, USA.  Available at https://hdl.handle.net/1721.1/80144.
  * [24] Tetsuo Yokoyama (2010): _Reversible Computation and Reversible Programming Languages_.  Electron. Notes Theor. Comput. Sci. 253(6), pp. 71–81, 10.1016/j.entcs.2010.02.007.
  * [25] Tetsuo Yokoyama, Holger Bock Axelsen & Robert Glück (2011): _Towards a Reversible Functional Language_.  In: RC 2011, Lecture Notes in Computer Science 7165, Springer, pp. 14–29, 10.1007/978-3-642-29517-1_2.