# Reversing an Imperative Concurrent Programming Language

James Hoey, Irek Ulidowski
School of Computing and Mathematical Sciences, University of Leicester,
Leicester, UK

###### Abstract

We introduce a method of reversing the execution of imperative concurrent
programs. Given an irreversible program, we describe the process of producing
two versions. The first performs forward execution and saves information
necessary for reversal. The second uses this saved information to simulate
reversal. We propose using identifiers to overcome challenges of reversing
concurrent programs. We prove this reversibility to be correct, showing that
the initial program state is restored and that all saved information is used
(garbage-free).
Keywords:  Reversible computation, inverse concurrent execution, correct
reversal of execution

##  1 Introduction

Traditional computation is fundamentally irreversible, starting in an initial
state and reaching a final state. Typically the initial store cannot be
restored as the computation cannot be performed in reverse due to the loss of
information throughout forward execution. Reversible computation, an
interesting and advancing field of research, aims to propose solutions to this
challenge and allow computation from a final state back to the corresponding
initial state.

Executions of traditional programming languages are irreversible. Widely used
languages such as C or Java execute correctly and efficiently in the
traditional forward direction, but do not directly support reversal. Consider
a simple program that contains only the destructive assignment X = 5, where X
is initially 2. Forward execution of this program overwrites the value of the
variable, discarding the previous value 2 (typically this lost information is
dissipated as heat [27]). Now imagine we wish to reverse this execution (a
possible reason being we optimistically performed this execution under
assumptions that are no longer true). To correctly restore to the previous
state, the variable must hold its previous value. With no way of re-
calculating this old value, reversal of this execution is not possible. Had
the assignment been X += 5, a constructive update that increments the value of
a variable, the previous value can easily be re-calculated via a decrement of
5. Therefore constructive assignments are reversible provided the expression
evaluates during reversal to the same value.

There are a number of motivations for continued research into reversible
computation. Traditional execution loses information as energy, as shown by
the Landauer principle that states that erasing 1 bit of information costs at
least $kT\ln 2$ in energy (where $K$ is the Boltzmann constant and $T$ is the
temperature of the heat sink) [27]. With reversibility requiring no
information to be lost, there is the potential for more energy efficient
computation. In 2018, Frank corrected some common misconceptions regarding
this principle [12]. Reversible computation is also desirable due to the
potential applications it supports. This includes to debugging, where
reversing an execution experiencing a bug can avoid the difficultly of
reproducing a bug in a concurrent, or multi-threaded, program [30, 23, 10],
and optimistic Parallel Discrete Event Simulation (PDES), where events can be
optimistically executed as soon as they are possible and rolled back, or
reversed, if this is later found to be incorrect [44, 53, 5, 6]. Additional
detail is given in Section 2. More recent work has discussed the link between
reversibility and robotics [34], and reversible circuits and logic gates [52].
Important background and further information regarding all applications of
reversible computation can be found through the European Cooperation in
Science and Technology (COST) project IC1405 Reversible Computation -
Extending Horizons of Computing [49].

Previous research into reversible execution is broadly focused on two key
areas; introducing reversible programming languages or semantics, and adding
reversibility to irreversible programming languages or semantics. Reversible
programming languages [35, 19] ensure that any valid program written is
executable in both the forward and reverse direction. This elegant solution to
reversibility is described in Section 2, where several examples of such
languages are given. As we will describe later, some of the components of
reversible languages (such as post-conditions for reverse control flow) are
difficult to automatically generate. This means work is required to transform
an irreversible program into an equivalent reversible version. The second
category aims to avoid this challenge by adding reversible capabilities
directly into an irreversible program. This removes the need for conversion of
traditional programs into reversible equivalents, and instead makes each
statement reversible by saving lost information needed for reversal. Section 2
details examples of this approach, including checkpointing, which typically
requires the program state to be saved regularly and then used to restore to a
previous position, and source-to-source translation [39], which takes an
original program and produces a version that is now capable of saving all
information needed for reverse execution.

One example of the source-to-source translation approach is the Reverse C
Compiler (RCC for short) [39], a tool capable of taking a (sequential) C
program and modifying this with state saving statements. To the best of our
knowledge, RCC has not been released publicly. More detail is given in Section
2. We follow closely to this, but focus on supporting a language containing
interleaving parallelism (concurrency). Our approach is also semantics-driven,
we do not insert extra statements into the code of the original program, but
define operational semantics that perform both the expected forward execution,
and the necessary saving of lost information. A second operational semantics
is defined for reverse execution, where this saved information is used. A
major motivation of this work is to produce an approach proved formally to be
correct, showing that reverse execution does indeed produce exactly the
initial program state.

Original execution $\displaystyle(\texttt{P},\square)$
$\displaystyle\rightarrow(\texttt{skip},\square^{\prime})$ Annotated execution
$\displaystyle(\texttt{P${}^{a}$},\square,\delta)$
$\displaystyle\rightarrow(\texttt{skip},\square^{\prime},\delta^{\prime})$
Inverted execution
$\displaystyle(\texttt{P${}^{r}$},\square^{\prime},\delta^{\prime})$
$\displaystyle\stackrel{{\scriptstyle}}{{\rightsquigarrow}}(\texttt{skip},\square^{\prime\prime},\delta)$
Figure 1: An original, annotated and inverted execution. The program states
$\square$ (the original state) and $\square^{\prime\prime}$ (the state
produced after inverted execution) are equivalent.

In this paper we propose a source to source translator approach, outlined in
Figure 1, to reversing imperative concurrent programs. Consider a program P, a
program state $\square$ and the original execution shown in Figure 1. We
produce a modified version Pa, named the _annotated version_ , that performs
forward execution and saves _reversal information_ that would otherwise have
been lost. Let $\delta$ be the initially empty store used to record this
additional information. Execution of this annotated program produces the same
final state $\square^{\prime}$ as traditional execution, and some reversal
information $\delta^{\prime}$. We next produce Pr, named the _inverted
version_. This is a forward-executing program (with inverted statement order)
that simulates reversal by undoing each statement, using (and removing)
reversal information from $\delta^{\prime}$ to do so. This inverted execution
begins in the final program state $\square^{\prime}$ with the reversal
information $\delta^{\prime}$, and produces a final program state
$\square^{\prime\prime}$. Later we prove that this reversal is correct meaning
that $\square^{\prime\prime}$ is equivalent to $\square$. All reversal
information is used, producing the original $\delta$ and thus showing that our
reversal is garbage-free. To ensure we achieve our aim of proving this method
to be correct, reversibility is defined using basic structures such as stacks.
We note that some of these choices may impact the overall efficiency, with
future optimisations offering potential improvements. We also note here that
our approach does not currently support floating point numbers. Adding such
support is an interesting and challenging area of potential future work. Other
examples include adding support for pointers, user defined data types and
division.

Our main contribution here is to introduce a method of reversing the execution
of imperative concurrent programs. A common issue with much of the current
literature is that such approaches are not formally proved correct. We have
addressed this via a detailed proof of correctness, confirming that our
approach reverses concurrent program execution as intended. We expand on our
work published previously [21] by introducing support for arrays. Our first
data structure increases the complexity of the language supported, and allows
for more interesting programs to be reversed. This required the definition of
operational semantics for array operations, including the saving and using of
necessary information lost as these execute. The correctness of our method of
reversibility has also been maintained and now includes the new constructs
introduced to support arrays.

##  2 Related Work

Perumalla describes important background research into reversible computation
[39], including multiple potential paradigms of reversal. Some examples
include _Forward-Reverse-Commit_ , where programs are reversibly executed
until a point at which reversibility is no longer required (and the execution
is committed), _Compute-Copy-Uncompute_ , where a modified forward execution
is performed and the result stored, before the execution is reversed.

Bennett stated in 1973 that a program execution can be reversed by saving a
history of the information lost as it is executed forwards and using this to
undo the program execution [2]. There are two types of reversibility, namely
_physical reversibility_ and _logical reversibility_. Physical reversibility
focuses on producing executions that do not lose information, including
reversible hardware such as circuits [49]. We focus on logical reversibility,
that is the ability to reproduce a previous execution state from some later
position.

Reversible programming languages is one way of implementing this. Unlike
traditional languages, any valid program written in a reversible language is
executable both forwards and backwards, without the need to save any other
information. One example of a reversible imperative programming language is
Janus [35, 55]. Only reversible statements are supported in Janus. For
example, destructive assignments (those that overwrite a value of a variable)
are not valid, with only constructive assignments (an increment or decrement,
each of which have an obvious inverse) supported. Conditional statements and
while loops each contain a post-condition, a boolean expression that is used
to determine reverse control flow. Other examples of reversible imperative
programming languages include R-WHILE [16], R-CORE [17] and R [13].

Several object-oriented reversible programming languages have also been
proposed, such as Joule proposed by Schultz [46, 45]. Haulund et al introduced
ROOPL [19, 8]. More recently, a web interface for ROOPL was introduced [20] as
part of working towards a unified language architecture.

Reversible functional programming languages include that defined by Yokoyama
et al [54], and Rfun from Thomsen et al [48]. CoreFun is a typed functional
language from Jacobsen et al [26]. Lanese et al presented an approach for
reversible execution of Erlang, a functional and concurrent programming
language, by defining reversible semantics [31]. Alongside working on
functional languages, Mogensen has also discussed a reversible version of the
Static Single Assignment, named RSSA [37], and reversible functional array
programming [38].

An alternative implementation of logical reversibility is to add reversibility
to irreversible languages. An obvious approach is named _full checkpointing_
[39], where the entire state is saved after each step. Previous execution
positions can be restored simply by reverting to the saved state. This faces
multiple challenges including the time and memory required for saving. Reduced
checkpointing approaches, such as _periodic_ or _incremental_ , decrease the
frequency or size of each checkpoint, but typically require forward re-
execution to reach the majority of states [39]. Such re-execution takes time
(depending on the frequency of checkpoints) and suffers possible concurrency
problems.

The Reverse C Compiler (RCC) is a source-to-source translator for a subset of
the programming language C [39, 4]. Given an original program, RCC produces
two versions of it. The first version contains inserted ‘SAVE’ commands to
record lost information. The assignment statement X = 2 becomes SAVE(X); X =
2. The second version, containing all original statements but in inverted
order, includes ‘RESTORE’ commands that use saved information to correctly
reverse each statement. The assignment statement X = 2 becomes RESTORE(X) for
reversal. Conditional statements save the result of evaluating the boolean
condition, whereas while loops use a loop counter. While supporting other
statement types, there is no support for parallel (or concurrent) programs.

Backstroke is a framework developed to support automatic generation of reverse
code for functions written in C++ [53]. Schordan et al continue this work of
applying this to PDES [44, 7], as have others [47]. Using the Execute-Reverse-
Commit paradigm, Backstroke takes an original code fragment, an event E, and
produces three versions. Backstroke produces Eforward (that performs forward
execution and saves necessary information), Ereverse (that uses this saved
information to reverse all effects), and Ecommit (that performs actions that
are irreversible or that should not be undone). Optimistic PDES [14] can then
be performed, with any events executed in the wrong order corrected via
reversal [4, 5, 6].

Schordan et al describe an approach using transformation based on recording
pairs of the form (address,value) [43, 44]. Code is instrumented in such a way
that these pairs are recorded, while no information regarding the executed
program path (or interleaving) is required. This approach of recording only
data on the heap is sufficient for implementing reversibility at a function-
level, a granularity that suits its application to PDES. The work in [53] is
slightly different to this and instead generates reverse code (a similar
notion to that presented in this work).

Reversible process calculi is the subject of previous research. Danos and
Krivine proposed a reversible version of the Calculus of Communicating Systems
(CCS), named RCCS [9]. Processes are extended to contain memories that help
identify processes used within actions. Phillips and Ulidowski introduced an
alternative approach to reversing CCS, named CCS with Communication Keys
(CCSK) [40]. All actions are annotated with an identifier (communication key),
with the two parties of a communication using the same identifier. Both RCCS
and CCSK allows actions to be reversed in any order that respects all causal
dependencies. This is named _causal-consistent reversibility_ , and differs to
_backtracking reversibility_ [3], where actions (or steps) must be reversed in
exactly the inverted forward order. Properties of reversible systems are
described [33], as is out of causal order reversibility [41]. Medić et al have
compared the two previously mentioned reversible versions of CCS [36, 28].

Debugging, the process of finding and fixing the underlying cause of a
software defect, is a possible application of reversible computation [10, 22,
56]. _Cyclic debugging_ repeatedly executes a program experiencing a bug with
small code changes each time. This suits sequential programs, where re-
execution is guaranteed to produce the same behaviour. Two executions of a
concurrent program can behave differently, with a bug potentially only
occurring under a specific interleaving (named a ‘Heisenbug’). Whether a fix
has worked is therefore difficult to judge. Engblom reviews reversible
debuggers [10], with an example of a commercially available reversible
debugger being UndoDB [51, 50].

The previous debuggers follow backtracking order. Giachino et al introduced
the causal-consistent debugger CaReDeb for the language $\mu$Oz [15]. Lanese
et al. defined a causal-consistent reversible debugger for Erlang named Cauder
[29, 30] with support for distributed programs [11].

##  3 Imperative Concurrent Programming Language and Program State

We begin by introducing our imperative concurrent programming language, and
the necessary program state.

###  3.1 Syntax

The syntax of our programming language is shown in Figure 2. The constructs
supported include constructive assignments (increment or decrement of variable
values), destructive assignments (overwriting of variable values), conditional
branching, while loops, blocks, declaration and removal of local variables or
arrays, and potentially recursive procedures. Let $\mathbb{P}$ be the set of
programs ranged over using P, Q, etc, and $\mathbb{S}$ be the set of
statements ranged over using S, T, etc. Let $\mathbb{X}$ be the set of
variables ranged over by X, Y, etc, and $\mathbb{Z}$ be the set of integers
such that n $\in\mathbb{Z}$. The set of arithmetic expressions $\mathbb{E}$ is
such that $\texttt{E}\in\mathbb{E}$, while the set of boolean expressions
$\mathbb{B}$ is such that $\texttt{B}\in\mathbb{B}$.

P $\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{S}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{P};\texttt{P}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{P par
P}$ S $\displaystyle::=\texttt{skip}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{X = E pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{name[E] =
E pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{X += E
pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{X -= E
pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{name[E] += E
pa}\leavevmode\nobreak\ |$
$\displaystyle\phantom{\texttt{::==}}\texttt{name[E] -= E
pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{if In B then P else Q
end pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{while Wn B do P end
pa}\leavevmode\nobreak\ |$ $\displaystyle\phantom{\texttt{::==}}\texttt{begin
Bn BB end}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{call Cn n
pa}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{runc Cn P end}$ E
$\displaystyle::=\texttt{X}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{n}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{Arr[n]}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{(E)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E Op
E}\qquad\texttt{B}::=\texttt{T}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{F}\leavevmode\nobreak\ |\leavevmode\nobreak\
\lnot\texttt{B}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{(B)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E ==
E}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E >
E}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{B $\land$ B}$ BB
$\displaystyle::=\texttt{DV};\texttt{DA};\texttt{DP};\texttt{P};\texttt{RP};\texttt{RA};\texttt{RV}$
DV $\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{var X = E
pa};\texttt{DV}\qquad\texttt{RV}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove X = E pa};\texttt{RV}$ DP
$\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{proc Pn name is P end
pa};\texttt{DP}\qquad\texttt{RP}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove Pn name is P end pa};\texttt{RP}$ DA
$\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{arr[n] name
pa};\texttt{DA}\qquad\texttt{RA}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove arr[n] name pa};\texttt{RA}$ Figure 2:
Imperative concurrent programming language syntax, where Op = {+, -, +=, -=}.

Our language syntax follows closely to other while languages, including that
of Hüttel [25]. We do however introduce several notions not seen in common
while languages. Firstly, we support concurrent execution through our parallel
composition operator, and represent two programs P and Q in parallel as P par
Q. We note here we also write this as par {P} {Q} in several examples for
presentation purposes. Support for arrays is also first introduced here and
was not part of our previous work [21]. An array name acts as a pointer to the
beginning of a block of memory for array elements. This increases the
complexity of the language and allows for more interesting example programs.
Secondly, constructs are uniquely named to aid identification of a specific
construct during reversal (explained later). This is achieved using elements
of the set of _construct identifiers_ $\mathbb{C}$. Construct identifiers In,
Wn, Bn, Pn and Cn ($\in\mathbb{C}$) are used to name conditionals, loops,
blocks, procedures and procedure calls respectively. Thirdly, the majority of
statements have a _statement path_ associated to them that is used to
determine the scope of local variables. For correct evaluation of a local
variable, we must first determine in which block this local variable was
declared. Given a statement, its statement path is the ordered sequence of all
(including nested) block names in which it exists. The set of statement paths
Pa is such that $\texttt{pa}\in\texttt{Pa}$. Statements that do not require
any evaluation, such as a block statement, do not require a statement path.
Fourthly, we include _removal statements_ and the runc construct. For reversal
purposes and to avoid garbage, any local declarations within a block are also
removed at the end of that block. For example, a local variable is declared
and exists for the execution of that block body, before being removed prior to
the closure of the block. The runc construct exists to distinguish between the
procedure call that has not yet been executed, and the execution of a
procedure body.

Finally, we make several key assumptions about programs written in our syntax.
Local variables, arrays and procedures are only declared within blocks, those
in the same block are named uniquely, and local declarations are removed in
exactly the inverted order. The runc construct is not allowed to appear in an
original program, and is instead only introduced as a result of executing a
procedure call.

###  3.2 Program State

We now introduce the program state. As in [25], the program state contains a
_variable environment_ and a _data store_.

Variable Environment $\gamma$. Each version of a variable
($\texttt{X}\in\mathbb{V}$) and parent block name (Bn) is mapped to a unique
memory location ($\texttt{l}\in\mathbb{L}$). The notation
$\gamma[\texttt{(X,Bn)}\Rightarrow\texttt{l}]$ maps X declared within Bn to l,
while $\gamma[\texttt{(X,Bn)}]$ removes this. All global variables are assumed
to exist each with a distinct memory location.

Data Store $\sigma$. Each memory location l is mapped to the value v it
currently holds. The notation $\sigma[\texttt{l}\mapsto\texttt{v}]$ updates
$\sigma$ such that l now holds v, while $\sigma(\texttt{l})$ returns the
current integer value at memory location l. Expression
$\sigma[\\{\texttt{l1},\cdots,\texttt{ll+n}\\}\mapsto\texttt{v}]$ represents
multiple modifications to memory locations performed in a single step. Each
memory location in the range l1 up to l1+n is updated to hold some value v.
All required memory locations exist initially and contain 0. The function
$\emph{nextLoc}(\sigma\emph{})$ returns the next available memory location,
while $\emph{nextLocBlock}(\sigma,\texttt{n}\emph{})$ reserves a consecutive
block of n locations, returning the first.

We further introduce the _while environment_ and the _procedure environment_ ,
both of which are initially empty and help with reversal.

While Environment $\beta$. The unique construct identifier Wn of each
currently active while loop is mapped to a copy of that loop. The notation
$\beta$[Wn $\Rightarrow$ P] inserts a mapping into $\beta$ between the loop
uniquely named Wn and the copy P of the loop body, while $\beta$[Wn] removes
this.

Procedure Environment $\mu$. A construct identifier Pn of each procedure is
mapped to a copy of the procedure body. Expression
$\mu[\texttt{Pn}\Rightarrow\texttt{(n,P)}]$ maps the identifier Pn to the
procedure name n and copy of the body P, while $\mu[\texttt{Pn}]$ removes
this.

The program state consists of four environments that we have introduced so
far. We use $\square$ to represent the tuple
($\gamma$,$\sigma$,$\beta$,$\mu$). By abuse of notation, we use $\square$ to
represent any subset of this tuple in the following semantics.

Given our syntax and program state, we can now present the operational
semantics of traditional (and irreversible) execution, following closely to
that of Hüttel [25]. To save space we do not show this here (though it can be
seen in [21]), as there is similarity with semantics shown in Section 4.4.
Ignoring any use of $\delta$ and stacks A (both of which are introduced later)
in the semantics in Section 4.4 gives the traditional semantics.

###  3.3 Odd-Even Transposition Sort

We shall use a program that implements a sorting algorithm throughout the rest
of the paper to explain and illustrate our method for reversing execution.
More specifically, the program is an implementation of an Odd-even
Transposition Sort, a concurrent version of a bubble sort which was originally
introduced by Habermann [18]. It is shown in Figure 3, with statement paths
omitted as these can be read from the code. For example, the assignment on
line 14 has the path b2.0;b1:0 since this statement is within the block b2.0,
which is within block b1.0. Block names will be modified for each iteration as
part of the process to keep construct identifiers unique (meaning paths also
change). For example, block b2.0 becomes b2.1 during the second iteration. We
omit empty false branches of conditional statements.

Each pass of the algorithm contains an even and an odd phase. During even
phases (lines 8–27), each element at an even index is compared with their
neighbour and potentially switched. Each comparison is performed in parallel
and can be interleaved in any order. During odd phases (lines 28–47), each
element at an odd index is compared and potentially swapped with its neighbour
again in parallel. As for a bubble sort, the worst case scenario requires $n$
complete loop iterations for an array of length $n$. After all required loop
iterations, the array will be sorted into ascending order. Example 1 describes
the traditional (irreversible) execution of our program.

⬇

1begin b1.0

2 arr[5] l;

3 l[0] = 7; l[1] = 3; l[2] = 4;

4 l[3] = 1; l[4] = 6;

5 count = 0;

6

7 while w1.0 (count1 < 4) do

8 //even phase

9 par {

10 if i2.0 (l[0] > l[1]) then

11 begin b2.0

12 var temp = 0;

13 temp = l[0]; l[0] = l[1];

14 l[1] = temp;

15 remove temp = 0

16 end

17 end

18 } {

19 if i3.0 (l[2] > l[3]) then

20 begin b3.0

21 var temp = 0;

22 temp = l[2]; l[2] = l[3];

23 l[3] = temp;

24 remove temp = 0

25 end

26 end

27 };

28 //odd phase

29 par {

30 if i4.0 (l[1] > l[2]) then

31 begin b4.0

32 var temp = 0;

33 temp = l[1]; l[1] = l[2];

34 l[2] = temp;

35 remove temp = 0

36 end

37 end

38 } {

39 if i5.0 (l[3] > l[4]) then

40 begin b5.0

41 var temp = 0

42 temp = l[3]; l[3] = l[4];

43 l[4] = temp;

44 remove temp = 0

45 end

46 end

47 };

48 count += 1

49 end;

50

51 //array removal

52 remove arr[5] l

53end

Figure 3: Odd-even transposition sort. Empty else branches and paths are
omitted.

######  Example 1.

Let l be the array [7,3,4,1,6] as on lines 2–4 of Figure 3. This is the array
that we wish to sort via the odd-even transposition sort. Assuming ascending
order, the first even phase will produce the array [3,7,1,4,6], before the
first odd phase produces [3,1,7,4,6]. After all required passes, the resulting
array is [1,3,4,6,7]. We shall describe the annotated forward execution in
Example 5 and the reverse execution in Example 7. $\hfill\blacksquare$

##  4 Annotation

AP $\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{AS}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{AP};\texttt{AP}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{AP
par AP}$ AS $\displaystyle::=\texttt{skip I}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{X = E (pa,A)}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{name[E] = E (pa,A)}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{X += E (pa,A)}\leavevmode\nobreak\ |$
$\displaystyle\phantom{\texttt{::==}}\texttt{X -= E
(pa,A)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{name[E] += E
(pa,A)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{name[E] -= E
(pa,A)}\leavevmode\nobreak\ |$ $\displaystyle\phantom{\texttt{::==}}\texttt{if
In B then AP else AP end (pa,A)}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{while Wn B do AP end (pa,A)}\leavevmode\nobreak\ |$
$\displaystyle\phantom{\texttt{::==}}\texttt{begin Bn ABB
end}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{call Cn n
(pa,A)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{runc Cn AP end}$ E
$\displaystyle::=\texttt{X}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{n}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{Arr[n]}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{(E)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E Op
E}\qquad\texttt{B}::=\texttt{T}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{F}\leavevmode\nobreak\ |\leavevmode\nobreak\
\lnot\texttt{B}\leavevmode\nobreak\ |\leavevmode\nobreak\
\texttt{(B)}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E ==
E}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{E >
E}\leavevmode\nobreak\ |\leavevmode\nobreak\ \texttt{B $\land$ B}$ ABB
$\displaystyle::=\texttt{ADV};\texttt{ADA};\texttt{ADP};\texttt{AP};\texttt{ARP};\texttt{ARA};\texttt{ARV}$
ADV $\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{var X = E
(pa,A)};\texttt{ADV}\qquad\texttt{ARV}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove X = E (pa,A);ARV}$ ADP
$\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{proc Pn name is AP end
(pa,A)};\texttt{ADP}\quad\texttt{ARP}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove Pn name is AP end (pa,A)};\texttt{ARP}$
ADA $\displaystyle::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{arr[n] name
(pa,A)};\texttt{ADA}\qquad\texttt{ARA}::=\texttt{$\varepsilon$}\leavevmode\nobreak\
|\leavevmode\nobreak\ \texttt{remove arr[n] name (pa,A)};\texttt{ARA}$ Figure
4: Annotated programming syntax, where Op = {+, -, +=, -=}.

Annotation is the process of producing a version of a given program that both
performs the expected forward execution and saves reversal information. This
reversal information consists of two parts; the interleaving order and
unrecoverable information lost during statement execution. To save this we
define the semantics of annotated execution. We first introduce the syntax of
annotated programs.

###  4.1 Annotated Syntax

We modify an original program P such that it is capable of recording both lost
information and the interleaving order. The resulting program AP, an element
of the set of all annotated programs $\mathbb{AP}$, is of the syntax in Figure
4. Compared to Figure 2, we use AP and AS in place of P and S respectively,
and introduce stack names A, which we define in Section 4.2. Now each path pa
has a stack associated to it via the notation $(\texttt{pa},\texttt{A})$. An
annotated version of a program is produced via the function _ann_ :
$\mathbb{P}\rightarrow\mathbb{AP}$ in Figure 5.

$\displaystyle ann(\texttt{$\varepsilon$})=\texttt{$\varepsilon$}$
$\displaystyle ann(\texttt{S;P})=ann(\texttt{S});ann(\texttt{P})$
$\displaystyle ann(\texttt{P par Q})=ann(\texttt{P})\texttt{ par
}ann(\texttt{Q})$ $\displaystyle ann(\texttt{skip})=\texttt{skip I}$
$\displaystyle ann(\texttt{X = e pa})=\texttt{X = e (pa,A)}$ $\displaystyle
ann(\texttt{if In b then P else Q end pa})=$ if In b then $ann($P$)$ else
$ann($Q$)$ end (pa,A) $\displaystyle ann(\texttt{while Wn b do P end
pa})=\texttt{while Wn b do $ann($P$)$ end (pa,A)}$ $\displaystyle
ann(\texttt{begin Bn P end})=\texttt{begin Bn $ann($P$)$ end}$ $\displaystyle
ann(\texttt{var X = E pa})=\texttt{var X = E (pa,A)}$ $\displaystyle
ann(\texttt{arr[n] name pa})=\texttt{arr[n] name (pa,A)}$ $\displaystyle
ann(\texttt{proc Pn n is P end pa})=\texttt{proc Pn n is $ann($P$)$ end
(pa,A)}$ $\displaystyle ann(\texttt{call Cn n pa})=\texttt{call Cn n (pa,A)}$
$\displaystyle ann(\texttt{runc Cn P end})=\texttt{runc Cn AP end A}$
$\displaystyle ann(\texttt{remove X = E pa})=\texttt{remove X = E (pa,A)}$
$\displaystyle ann(\texttt{remove arr[n] name pa})=\texttt{remove arr[n] name
(pa,A)}$ $\displaystyle ann(\texttt{remove Pn n is P end pa})=\texttt{remove
Pn n is $ann($P$)$ end (pa,A)}$ Figure 5: Partial definition of the Annotation
function $ann$, where I indicates a potential stack A (as some skip steps,
including those produced when closing a block, will not have a stack) and
shown in full in Appendix A.1. All statements omitted follow the instance of X
= e pa, where pa becomes (pa,A).

###  4.2 Capturing Interleaving Order

The specific execution path of a forward concurrent program is crucial for
correct reversal. This is the order in which the statements of a program are
executed forwards. Due to the potential for data races, two forward executions
with different interleaving orders may produce different program states.
Reversing statements in a different order to that of the inverted forward
order may lead to incorrect program states (a state not reached during forward
execution). Such incorrect reversal is a problem for any possible application
of reversible execution. Consider reversible debugging where restoring program
states correctly is vital to help detect (and fix) software bugs. The
following two scenarios illustrate some negative consequences of incorrect
reversal order.

######  Example 2.

Figure LABEL:sub@ex:order-assign contains a race between two assignments to
the same variable X, where X is initially 1. The left assignment executes
first (overwriting 1) and is followed by the right assignment (overwriting 3).
Assume reverse execution incorrectly reverses the left assignment first,
restoring the value (it held before this assignment) to 1. The right
assignment is then reversed restoring X to 3. This reversal is incorrect as it
does not match the initial state. $\hfill\blacksquare$

######  Example 3.

Consider Figure LABEL:sub@ex:order-cond, and an execution where the left
conditional executes the true branch (overwriting Z) and the right conditional
executes the false branch (also overwriting Z). Assume an inverse execution
that reverses the incorrect branch of each conditional. Both conditionals now
reverse assignments to Y that were not performed forwards, meaning old values
were not saved and will lead to a state not reached during forward execution.
$\hfill\blacksquare$

⬇ 1X = 3 par X = 5

(a) Racing assignments

⬇ 1if i1 (Z > 3) then if i2 (Y > 3) then 2 Z = 2 Y = 4 3else par else 4 Y = 6
Z = 5 5end end

(b) Conditional statements

Figure 6: Programs that reverse incorrectly under specific interleavings.
Initially X = 1, Y = 2 and Z = 4. After the executions discussed in Examples 2
and 3, X = 5, Y = 2 and Z = 2. Statement paths and identifier stacks are
omitted.

Such problems are overcome by recording the order in which statements are
executed forwards with the help of _identifiers_ as in [40, 41]. Identifiers,
which are consecutive natural numbers and are ranged over using m and n (where
both are elements of the set of all identifiers $\mathbb{K}$), are used in
ascending order to capture the order in which statements execute. At each
interleaving decision point the next unused available identifier is associated
with the statement that is executing. An annotated version of a program must
be capable of storing potentially many identifiers associated to each
statement. Identifiers are maintained as an ordered sequence, with the
function _next_(__) returning the next unused identifier, and _previous_(__)
returning the previously used identifier.

In order to save identifiers as they are used, the syntax111The identifier
stacks would in practise be saved in a separate environment, named the
identifier environment. Each statement would then include the stack name,
meaning the stack of identifiers outlives the execution. To keep both the
proof and examples concise, we display all stacks as part of the statement and
omit use of the identifier environment. of each statement that requires
identifiers is expanded to include an _identifier stack_. Each is uniquely
named and represented as Ai. The stack notation m:Ai represents an identifier
m and the remaining stack Ai. Example 4 demonstrates forward identifier use on
a small program.

⬇

1${\color[rgb]{150,0,150}\texttt{while w1 }}\texttt{(X >
3)}{\color[rgb]{150,0,150}\texttt{ do}}\hskip
28.45274pt\phantom{\texttt{par}}\hskip 24.18501pt\texttt{Y =
2}\quad{\color[rgb]{0,0,1}\langle\texttt{5}\rangle}\texttt{;}$

2 $\texttt{X = X -
1}\quad{\color[rgb]{0,0,1}\langle\texttt{1,3,7}\rangle}\texttt{}\hskip
16.21828pt\texttt{par}\hskip 27.31483pt\texttt{X = X -
Y}\quad{\color[rgb]{0,0,1}\langle\texttt{6}\rangle}\texttt{;}$

3${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\langle\texttt{0,2,4,8}\rangle}\texttt{}\hskip
54.06006pt\phantom{\texttt{par}}\hskip 22.76228pt\texttt{Y =
X}\quad{\color[rgb]{0,0,1}\langle\texttt{9}\rangle}\texttt{}$

Figure 7: Example use of identifiers to capture interleaving order. Let X =
10, Y = 1 and Z = 3 initially. Statement paths and identifier stacks are
omitted.

######  Example 4.

Figure 7 contains a while loop in parallel with three assignment statements.
The notation ${\color[rgb]{0,0,1}\langle\phantom{\texttt{3}}\rangle}$
represents a stack used to store identifiers for each statement, with the left
most element being the head. The interleaving order of this program is
captured via the identifiers shown. $\hfill\blacksquare$

###  4.3 Capturing Unrecoverable Information

Some data lost as statements execute forwards is unrecoverable. The simplest
example of this is a destructive assignment, where the current value of the
variable in question is overwritten and lost. Correct reversal requires this
variable to be restored to this lost value, with no way of re-calculation. We
must therefore save such lost information, including control flow information
(see Section 4.4). Therefore we introduce the _auxiliary store_ $\delta$ for
this purpose. The store $\delta$ is separate to the program state and consists
of stacks (ideal for reversibility due to their Last-In, First-Out (LIFO)
nature).

There exists a single stack in $\sigma$ for each variable within the program.
There is also a single stack B and a single stack W in $\sigma$, each used to
store the result of evaluating all conditional statement or while loop boolean
expressions respectively. The stacks WI and Pr are used to store identifiers
associated to renamed copies of loop or procedure bodies prior to their
removal. The store $\delta$ is defined as
$\delta:(\mathbb{X}\rightarrow(\mathbb{K}\times\mathbb{Z}))\cup(\texttt{B}\rightarrow(\mathbb{K}\times\mathbb{B}))\cup(\texttt{W}\rightarrow(\mathbb{K}\times\mathbb{B}))\cup(\texttt{WI}\rightarrow(\mathbb{K}\times\mathbb{C}))\cup(\texttt{Pr}\rightarrow(\mathbb{K}\times\mathbb{C}))$,
where $\mathbb{C}$ is the set of identifier sequences retrieved from a loop or
procedure copy prior to its removal. Each stack within $\delta$ stores pairs
of natural numbers, with the first element being an identifier and the second
being an old value or boolean. We note that throughout we use T and F to
represent 1 and 0 (boolean values) respectively.

The notation $\delta$[el $\rightharpoonup$ St] represents pushing the element
el to the stack St, and $\delta$[St/St′] represents popping the head of stack
St, leaving the tail St′. Correspondingly,
$\delta[\texttt{\\{({m},$\sigma$({el1}),\ldots,({m},$\sigma$({el1+n}))\\}
$\rightharpoonup$ X}]$ is used to represent pushing many pairs onto a single
stack X. Each pair contains the identifier m, but with the contents of memory
locations ranging from el1 to el1+n, in order. Finally,
$\delta(\texttt{name},\texttt{m})$ is used to represent continually popping
the stack name while the top element contains the identifier m, returning each
of the old values saved there.

By abuse of notation, we update $\square$ to now also contain $\delta$. The
following defines when two program states are equivalent.

######  Definition 1.

(Equivalent states) Let $\square$ be the environment tuple
{$\sigma$,$\gamma$,$\mu$,$\beta$,$\delta$} and $\square_{1}$ be the tuple of
annotated environments
{$\sigma_{1}$,$\gamma_{1}$,$\mu_{1}$,$\beta_{1}$,$\delta_{1}$}. Let
_d_($\gamma$__) be the domain of $\gamma$. We say that $\square$ is
_equivalent_ to $\square_{1}$, written $\square\approx\square_{1}$, if and
only if:

  1. 1.

_d_($\gamma$__) =_d_($\gamma_{1}$__) and
$\sigma(\gamma(\textup{{X}},\textup{{Bn}}))$ =
$\sigma_{1}(\gamma_{1}(\textup{{X}},\textup{{Bn}}))$ for all X $\in$
_d_($\gamma$__) and block names Bn;

  2. 2.

_d_($\mu$__) =_d_($\mu_{1}$__); $\mu(\textup{{Pn}})$ = (n,P),
$\mu_{1}(\textup{{Pn}})$ = (n,AP) and AP = $ann($P$)$ for all Pn $\in$
_d_($\mu$__);

  3. 3.

_d_($\beta$__) =_d_($\beta_{1}$__); $\beta(\textup{{Wn}})$ = P,
$\beta_{1}(\textup{{Wn}})$ = AP and AP = $ann($P$)$ for all Wn $\in$
_d_($\beta$__).

###  4.4 Operational Semantics of Annotated Programs

To define the behaviour of our programming language, we now use _Structural
Operational Semantics_ (SOS) [42] to define a _transition system_. A
transition system is a directed graph, with each vertex a _configuration_ and
each edge a _transition_. A _configuration_ represents a snapshot of an
execution and is composed of a program P and program state $\square$, written
as $(\texttt{P}\mid\square)$. Two configurations can be linked together as a
transition, where the second configuration can be reached from the first via a
single step of an execution. Each such transition is a member of the
_transition relation_ $\stackrel{{\scriptstyle}}{{\rightarrow}}$ (annotated
execution), which is defined as the least relation generated by the set of
_transition rules_ contained within this section. Each transition rule
consists of a _conclusion_ (the transition this rule represents), potentially
many _premises_ (other transitions or claims that must hold for the conclusion
to be valid) and an optional _side condition_ (constraints placed on
components of the rule). Each transition rule that has no premises is called
an _axiom_. Let $\stackrel{{\scriptstyle}}{{\rightarrow}}^{*}$ be the
reflexive and transitive closure of
$\stackrel{{\scriptstyle}}{{\rightarrow}}$. We note that ignoring all use of
$\delta$ and identifiers gives the traditional operational semantics of our
language.

We now give a syntax-directed, _small step semantics_ that defines annotated
execution. Each transition rule represents a single step of a larger
execution, meaning the resulting configuration need not be _terminal_ (no
further transitions from this configuration are possible), and instead can be
_intermediate_. We use $\hookrightarrow^{*}_{\texttt{a}}$ and
$\hookrightarrow^{*}_{\texttt{b}}$ to represent a step of arithmetic and
boolean expression evaluation respectively. As previously described, some
transition rules will use identifiers. Such steps are called _identifier
steps_ and are represented as $\stackrel{{\scriptstyle m}}{{\rightarrow}}$,
where m is the identifier used. Transition rules that do not use identifiers
are called _skip steps_ and are represented as $\rightarrow_{s}$. In some
cases, such as the execution of a loop body, a step may or may not use an
identifier depending on what the body does. Such transitions are represented
as $\stackrel{{\scriptstyle\circ}}{{\rightarrow}}$. All components of the
following rules that are included for reversibility are indicated using the
colour blue. The removal of all blue components from the following rules gives
the semantics of traditional (and irreversible) execution.

Assignment Destructive assignments overwrite the value of a given variable
(rule [D1a] below) or array element (rule [D2a]), with the old value being
saved to $\delta$ with $\delta[\texttt{(m,$\sigma($l$)$) $\rightharpoonup$
X}]$ and $\delta[\texttt{(m,$\sigma$($\sigma$({l})+{n})) $\rightharpoonup$
name)}]$ respectively. The given variable is evaluated via the function
$evalV($X,pa,$\gamma)$, taking the variable name X, the statement path pa and
variable environment $\gamma$, and producing the memory location l.
Constructive assignments increment ([C1a]/[C3a]) or decrement ([C2a]/[C4a]) a
variable or array element (e.g.
$\sigma[\texttt{l}\mapsto\sigma(\texttt{l})+\texttt{v}]$) with no reversal
information saved.

$\displaystyle\text{[D1a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
= e
(pa,A)}\mid{\color[rgb]{0,0,1}\delta},\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,$\sigma($l$)$)
$\rightharpoonup$ X}]},\sigma[\texttt{l}\mapsto\texttt{v}],\gamma,\square)}$
$\displaystyle\text{[D2a]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad(\texttt{e${}^{\prime}$
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto\texttt{v}]\quad{\color[rgb]{0,0,1}\delta^{\prime}=\delta[\texttt{(m,$\sigma$($\sigma$({l})+{n}))
$\rightharpoonup$ name)}]}\end{aligned}}{(\texttt{name[e] = e${}^{\prime}$
(pa,A)}\mid\sigma,\gamma,\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma^{\prime},\gamma,\delta^{\prime},\square)}$
$\displaystyle\text{[C1a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
+= e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma[\texttt{l}\mapsto\sigma(\texttt{l})+\texttt{v}],\gamma,\square)}$
$\displaystyle\text{[C2a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
-= e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma[\texttt{l}\mapsto\sigma(\texttt{l})-\texttt{v}],\gamma,\square)}$
$\displaystyle\text{[C3a]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad(\texttt{e${}^{\prime}$
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto(\sigma(\texttt{l})+\texttt{n})+\texttt{v}]\end{aligned}}{(\texttt{name[e]
+= e${}^{\prime}$ (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma^{\prime},\gamma,\square)}$
$\displaystyle\text{[C4a]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad(\texttt{e${}^{\prime}$
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto(\sigma(\texttt{l})+\texttt{n})-\texttt{v}]\end{aligned}}{(\texttt{name[e]
-= e${}^{\prime}$ (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma^{\prime},\gamma,\square)}$

Conditional Statement A conditional statement begins with evaluation of the
condition ($(\texttt{b
pa}\mid\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{T}\mid\square)$) to
true ([I1aT] or false [I1aF]). The true ([I2a]) or false ([I3a]) branch is
then executed. Finally, the conditional closes by saving a true ([I4a]) or
false ([I5a]) boolean value to $\delta$ indicating the executed branch (e.g.
$\delta[\texttt{(m,T) $\rightharpoonup$ B}]$).

$\displaystyle\text{[I1aT]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{b
pa}\mid\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{T}\mid\square)}{(\texttt{if
In b then AP else AQ end (pa,A)}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{if In T then AP else AQ end
(pa,{\color[rgb]{0,0,1}m:A})}\mid\square)}$
$\displaystyle\text{[I1aF]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{b
pa}\mid\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{F}\mid\square)}{(\texttt{if
In b then AP else AQ end (pa,A)}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{if In F then AP else AQ end
(pa,{\color[rgb]{0,0,1}m:A})}\mid\square)}$
$\displaystyle\text{[I2a]}\quad\frac{(\texttt{AP}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$}\mid\square^{\prime})}{(\texttt{if
In T then AP else AQ end
(pa,A)}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{if In
T then AP${}^{\prime}$ else AQ end (pa,A)}\mid\square^{\prime})}$
$\displaystyle\text{[I3a]}\quad\frac{(\texttt{AQ}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AQ${}^{\prime}$}\mid\square^{\prime})}{(\texttt{if
In F then AP else AQ end
(pa,A)}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{if In
F then AP else AQ${}^{\prime}$ end (pa,A)}\mid\square^{\prime})}$
$\displaystyle\text{[I4a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}}{(\texttt{if
In T then skip I else AQ end (pa,A)}\mid\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,T)
$\rightharpoonup$ B}]},\square)}$
$\displaystyle\text{[I5a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}}{(\texttt{if
In F then AP else skip I end (pa,A)}\mid\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,F)
$\rightharpoonup$ B}]},\square)}$

While Loop While loops allow a varying number of iterations (with the
condition not guaranteed to be invariant). To reverse a loop we record a
sequence of pairs onto stack W, with an element for each iteration. Each pair
consists of an identifier and a boolean value that reflects the evaluation of
the condition. This sequence is used to determine reverse control flow,
meaning these pairs are accessed in reverse order. As the first forward
iteration will be the last reverse iteration (the place to stop), we save a
false boolean during the first iteration ($\delta[\texttt{(m,F)
$\rightharpoonup$ W}]$) and then true for all others ($\delta[\texttt{(m,T)
$\rightharpoonup$ W}]$).

A loop not yet executed will have an undefined (_und_) mapping in $\beta$.
Loops have zero iterations ([W1a]), or begin with a first iteration ([W3a]).
This first iteration defines a mapping (_def_) in the while environment
($\beta[\texttt{Wn $\Rightarrow$ AR}]$) for this loop. Any further iteration
([W4a]) requires a true boolean value to be saved. The body of a loop is
executed for each iteration ([W5a], where each identifier used is reflected
into the while environment via _refW_(Wn,AP′ __) to ensure they outline the
execution) before this completes ([W6a]). A loop body is renamed prior to
every iteration via the function ($\emph{reL}(\texttt{AP}\emph{})$), which
takes the loop body AP and updates each construct identifier to ensure they
remain unique. Finally, the loop itself completes ([W2a]), saving all
identifiers used by this loop (retrieved via the function
_getAI_($\beta$(Wn)__) .

$\displaystyle\text{[W1a]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\beta($Wn$)$}=\emph{und}\quad(\texttt{b
pa}\mid\beta,\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{F}\mid\beta,\square)}{(\texttt{while
Wn b do AP end (pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,F)
$\rightharpoonup$ W}]},\beta,\square)}$ $\displaystyle\text{[W2a]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\beta($Wn$)$}=\emph{def}\quad(\texttt{b
pa}\mid\beta,\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{F}\mid\beta,\square)}{(\texttt{while
Wn b do AP end (pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,T)
$\rightharpoonup$ W},\texttt{(m,C) $\rightharpoonup$
WI}]},\beta[\texttt{Wn}],\square)}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where
}{\color[rgb]{0,0,1}\texttt{C}=\emph{getAI}(\beta(\texttt{Wn})\emph{}))}$

$\displaystyle\text{[W3a]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\beta($Wn$)$}=\emph{und}\quad(\texttt{b
pa}\mid\beta,\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{T}\mid\beta,\square)}{(\texttt{S}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{while Wn T do AP${}^{\prime}$ end
(pa,{\color[rgb]{0,0,1}m:A})}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,F)
$\rightharpoonup$ W}]},\beta[\texttt{Wn $\Rightarrow$ AR}],\square)}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where }\texttt{S}=\texttt{while
Wn b do AP end (pa,A)}\text{,
}\texttt{AP${}^{\prime}$}=\emph{reL}(\texttt{AP}\emph{})$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{and }\texttt{AR}=\texttt{while
Wn b do AP${}^{\prime}$ end (pa,m:A)}$ $\displaystyle\text{[W4a]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\beta($Wn$)$}=\emph{def}\quad(\texttt{b
pa}\mid\beta,\square)\hookrightarrow^{*}_{\texttt{b}}(\texttt{T}\mid\beta,\square)}{(\texttt{S}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{while Wn T do AP${}^{\prime}$ end
(pa,{\color[rgb]{0,0,1}m:A})}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,T)
$\rightharpoonup$ W}]},\beta[\texttt{Wn $\Rightarrow$ AR}],\square)}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where }\texttt{S}=\texttt{while
Wn b do AP end (pa,A)}\text{,
}\texttt{AP${}^{\prime}$}=\emph{reL}(\texttt{AP}\emph{})$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{and }\texttt{AR}=\texttt{while
Wn b do AP${}^{\prime}$ end (pa,m:A)}$ $\displaystyle\text{[W5a]}\hskip
2.84544pt\frac{\texttt{$\beta($Wn$)$}=\emph{def}\quad(\texttt{AP}\mid\delta,\beta,\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$}\mid\delta^{\prime},\beta^{\prime},\square^{\prime})}{(\texttt{while
Wn T do AP end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{while
Wn T do AP${}^{\prime}$ end
(pa,A)}\mid\delta^{\prime},\beta^{\prime\prime},\square^{\prime})}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where
}\beta^{\prime\prime}=\beta^{\prime}[\emph{refW}(\texttt{Wn},\texttt{AP${}^{\prime}$}\emph{})]$
$\displaystyle\text{[W6a]}\hskip
2.84544pt\frac{\texttt{$\beta($Wn$)$}=\texttt{while Wn b do AP end
(pa,A)}}{(\texttt{while Wn T do skip I end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}(\texttt{while
Wn b do AP end (pa,A)}\mid\delta,\beta,\square)}$

Block The body of a block executes ([B1a]) before this reaches skip and the
block closes ([B2a]) without saving any reversal information.

$\displaystyle\text{[B1a]}\quad\frac{(\texttt{AP}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$}\mid\square^{\prime})}{(\texttt{begin
b1 AP
end}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{begin b1
AP${}^{\prime}$ end}\mid\square^{\prime})}$
$\displaystyle\text{[B2a]}\quad\frac{}{(\texttt{begin b1 skip I
end}\mid\square)\rightarrow_{s}(\texttt{skip}\mid\square)}$

Variable, Procedure and Array Declaration Variable declaration ([L1a]) creates
a corresponding mapping in the variable environment
($\gamma[(\texttt{X},\texttt{Bn})\Rightarrow\texttt{l}]$) and data store
($\sigma[\texttt{l}\mapsto\texttt{v}]$). Procedure declaration ([L2a]) inserts
a mapping into the procedure environment
($\mu[\texttt{Pn}\Rightarrow\texttt{(n,AP)}]$). Array declaration ([L3a])
creates a mapping in the variable environment
($\gamma[(\texttt{name},\texttt{Bn})\Rightarrow\texttt{l}]$), and initialises
a block of consecutive memory locations for its elements
($\sigma[\texttt{l}\mapsto\texttt{l1},\\{\texttt{l1},\cdots,\texttt{l1}\texttt{+n}\\}\mapsto
0]$). In each case, no reversal information is required.

$\displaystyle\text{[L1a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\emph{nextLoc}(\sigma\emph{})=\texttt{l}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}}{(\texttt{var
X = e (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma[\texttt{l}\mapsto\texttt{v}],\gamma[(\texttt{X},\texttt{Bn})\Rightarrow\texttt{l}],\square)}$
$\displaystyle\text{[L2a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}}{(\texttt{proc
Pn n is AP (pa,A)}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\mu[\texttt{Pn}\Rightarrow\texttt{(n,AP)}],\square)}$
$\displaystyle\text{[L3a]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\emph{nextLoc}(\sigma\emph{})=\texttt{l}\quad\emph{nextLocBlock}(\sigma,n\emph{})=\texttt{l1}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}\\\\[-3.0pt]
&\sigma^{\prime}=\sigma[\texttt{l}\mapsto\texttt{l1},\\{\texttt{l1},\ldots,\texttt{l1}\texttt{+n}\\}\mapsto
0]\quad\gamma^{\prime}=\gamma[(\texttt{name},\texttt{Bn})\Rightarrow\texttt{l}]\end{aligned}}{(\texttt{arr[n]
name (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\sigma^{\prime},\gamma^{\prime},\square)}$

Variable, Procedure and Array Removal Variable removal ([H1a]) erases the
mapping for this version of a variable ($\gamma[(\texttt{X},\texttt{Bn})]$),
losing the final value it holds. We therefore save this value and the next
identifier onto $\delta$ via $\delta[\texttt{(m,$\sigma($l$)$)
$\rightharpoonup$ X}]$. Procedure removal ([H2a]) deletes the mapping from the
procedure environment ($\mu[\texttt{Pn}]$), though this can be recovered
completely from the inverse version and only an identifier is required. Array
removal ([H3a]) destroys the mapping between this array and the memory
locations it has used
($\sigma[\texttt{l}\mapsto\texttt{0},\\{\texttt{l1},\cdots,\texttt{l1}\texttt{+n}\\}\mapsto
0]$), and loses each of the final values held by the array elements. Each
final value is saved onto $\delta$ alongside the same identifier
($\delta[\texttt{\\{({m},$\sigma$({l1}),\ldots,({m},$\sigma(\texttt{l1}\texttt{+n})$\\}
$\rightharpoonup$ X}]$).

$\displaystyle\text{[H1a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}\quad\texttt{$\gamma($X,Bn$)$}=\texttt{l}}{(\texttt{remove
X = e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,$\sigma($l$)$)
$\rightharpoonup$
X}]},\sigma[\texttt{l}\mapsto\texttt{0}],\gamma[(\texttt{X},\texttt{Bn})],\square)}$
$\displaystyle\text{[H2a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\mu$(Pn)}=\emph{def}}{(\texttt{remove
Pn n is AP (pa,A)}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\mu[\texttt{Pn}],\square)}$
$\displaystyle\text{[H3a]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}\quad\texttt{$\gamma($name,Bn$)$}=\texttt{l}\quad\texttt{l1}=\sigma(\texttt{l})\\\\[-3.0pt]
&{\color[rgb]{0,0,1}\delta^{\prime}=\delta[\texttt{\\{({m},$\sigma$({l1}),\ldots,({m},$\sigma(\texttt{l1}\texttt{+n})$\\}
$\rightharpoonup$
X}]}\quad\sigma^{\prime}=\sigma[\texttt{l}\mapsto\texttt{0},\\{\texttt{l1},\cdots,\texttt{l1}\texttt{+n}\\}\mapsto
0]\quad\gamma^{\prime}=\gamma[(\texttt{name},\texttt{Bn})]\end{aligned}}{(\texttt{remove
arr[n] name (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
(pa,{\color[rgb]{0,0,1}m:A})}\mid\delta^{\prime},\sigma^{\prime},\gamma^{\prime},\square)}$

Procedure Call The opening ([G1a]) and closing ([G3a]) of a procedure call do
not lose any information that is not recoverable, meaning only an identifier
is required in each case. A renamed version of the procedure body (with
construct identifiers and stack names renamed to remain unique, and produced
by the function _reP_(__)) is stored into $\mu$ when opening
($\mu[\texttt{Cn}\Rightarrow\texttt{(n,AP${}^{\prime}$)}]$), and is removed
when closed ($\mu[\texttt{Cn}]$). Procedures are evaluated to a unique
construct identifier via the function _evalP_(n,pa __), which takes the
procedure name n used in the code and the statement path pa. To ensure
identifiers are not lost when the mapping is removed, these are reflected to
the procedure environment (via the function _refC_(Cn,AP′ __)) and then saved
to $\delta$ with $\delta[(\texttt{m,$getAI(\mu($Cn$)))$ $\rightharpoonup$
Pr}]$).

$\displaystyle\text{[G1a]}\quad\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\emph{evalP}(\texttt{n,pa}\emph{})=\texttt{Pn}\quad\mu(\texttt{Pn})=\texttt{(n,AP)}\quad\emph{reP}(\texttt{AP},\texttt{Cn}\emph{})=\texttt{AP${}^{\prime}$}}{(\texttt{call
Cn n (pa,A)}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{runc Cn AP${}^{\prime}$ end
{\color[rgb]{0,0,1}m:A}}\mid\mu[\texttt{Cn}\Rightarrow\texttt{(n,AP${}^{\prime}$)}],\square)}$
$\displaystyle\text{[G2a]}\quad\frac{(\texttt{AP}\mid\mu,\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$}\mid\mu^{\prime},\square^{\prime})}{(\texttt{runc
Cn AP end
A}\mid\mu,\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{runc
Cn AP${}^{\prime}$ end
A}\mid\mu^{\prime}[\emph{refC}(\texttt{Cn},\texttt{AP${}^{\prime}$})],\square^{\prime})}$
$\displaystyle\text{[G3a]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{next}(\emph{})}\quad\texttt{$\mu$(Cn)}=\emph{def}}{(\texttt{runc
Cn skip I end A}\mid\delta,\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid{\color[rgb]{0,0,1}\delta[\texttt{(m,$getAI(\mu($Cn$)))$
$\rightharpoonup$ Pr}]},\mu[\texttt{Cn}],\square)}$

Sequential and Parallel Composition A sequentially composed statement executes
([S1a]) until it reaches skip, before this skip statement is removed ([S2a])
(I represents a potential identifier stack). Programs in parallel interleave
their execution, with a step made via the left ([P1a]) or the right ([P2a])
program, before both are skip and the composition can close ([P3a]).

$\displaystyle\text{[S1a]}\quad\frac{(\texttt{AS}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AS${}^{\prime}$}\mid\square^{\prime})}{(\texttt{AS;
AP}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AS${}^{\prime}$;
AP}\mid\square^{\prime})}$ [S2a] $\displaystyle\quad\frac{}{(\texttt{skip I;
AP}\mid\square)\rightarrow_{s}(\texttt{AP}\mid\square)}$
$\displaystyle\text{[P1a]}\hskip
5.69046pt\frac{(\texttt{AP}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$}\mid\square^{\prime})}{(\texttt{AP
par
AQ}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP${}^{\prime}$
par AQ}\mid\square^{\prime})}$ [P2a] $\displaystyle\hskip
5.69046pt\frac{(\texttt{AQ}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AQ${}^{\prime}$}\mid\square^{\prime})}{(\texttt{AP
par AQ}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}(\texttt{AP
par AQ${}^{\prime}$}\mid\square^{\prime})}$ $\displaystyle\text{[P3a]}\hskip
5.69046pt\frac{}{(\texttt{skip I${}_{1}$ par skip
I${}_{2}$}\mid\square)\rightarrow_{s}(\texttt{skip}\mid\square)}$

###  4.5 Annotated Odd-Even Transposition Sort

⬇

1begin b1.0

2 ${\color[rgb]{150,0,150}\texttt{arr[5]}}\leavevmode\nobreak\
\texttt{l}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 0\rangle};$

3 $\texttt{l[0] = 7}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
1\rangle};$ $\texttt{l[1] = 3}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 2\rangle};$

4 $\texttt{l[2] = 4}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
3\rangle};$ $\texttt{l[3] = 1}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 4\rangle};$

5 $\texttt{l[4] = 6}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
5\rangle};$

6 $\texttt{count = 0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
6\rangle};$

7 while w1.0 (count1 < 4) do

8 //even phase

9 par {

10 if i2.0 (l[0] > l[1]) then

11 begin b2.0

12 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 35,10\rangle};$

13 $\texttt{temp = l[0]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
36,12\rangle};$

14 $\texttt{l[0] = l[1]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
38,14\rangle};$

15 $\texttt{l[1] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
40,17\rangle};$

16 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 42,18\rangle}$

17 end

18
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 70,68,61,58,45,33,21,8\rangle}$

19 } {

20 if i3.0 (l[2] > l[3]) then

21 begin b3.0

22 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 37,11\rangle};$

23 $\texttt{temp = l[2]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
39,13\rangle};$

24 $\texttt{l[2] = l[3]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
41,15\rangle};$

25 $\texttt{l[3] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
43,16\rangle};$

26 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 44,19\rangle}$

27 end

28
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 71,69,60,59,46,34,20,9\rangle}$

29 };

30 //odd phase

31 par {

32 if i4.0 (l[1] > l[2]) then

33 begin b4.0

34 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 25\rangle};$

35 $\texttt{temp = l[1]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
26\rangle};$

36 $\texttt{l[1] = l[2]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
27\rangle};$

37 $\texttt{l[2] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
28\rangle};$

38 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 29\rangle}$

39 end

40
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 73,72,65,63,50,47,30,23\rangle}$

41 } {

42 if i5.0 (l[3] > l[4]) then

43 begin b5.0

44 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 49\rangle};$

45 $\texttt{temp = l[3]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
51\rangle};$

46 $\texttt{l[3] = l[4]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
52\rangle};$

47 $\texttt{l[4] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
53\rangle};$

48 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 54\rangle}$

49 end

50
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 75,74,64,62,55,48,24,22\rangle}$

51 ${\color[rgb]{150,0,150}\texttt{\\}}};$

52 $\texttt{count += 1}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
76,66,56,31\rangle}$

53
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 77,67,57,32,7\rangle};$

54

55 //array removal

56 ${\color[rgb]{150,0,150}\texttt{remove arr[5]}}\leavevmode\nobreak\
\texttt{l}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 78\rangle}$

57end

Figure 8: Executed annotated Odd-even Transposition Sort. Empty else branches and paths are omitted. temp | count | l | B | W
---|---|---|---|---
$\langle$54,7$\rangle$ $\langle$29,7$\rangle$ |  $\langle$6,0$\rangle$ |  $\langle$78,7$\rangle$ $\langle$52,7$\rangle$ $\langle$27,7$\rangle$ $\langle$4,0$\rangle$ |  $\langle$75,T$\rangle$ $\langle$61,F$\rangle$ $\langle$24,F$\rangle$ |  $\langle$77,T$\rangle$
$\langle$51,0$\rangle$ $\langle$26,0$\rangle$ |  |  $\langle$78,6$\rangle$ $\langle$43,4$\rangle$ $\langle$17,3$\rangle$ $\langle$3,0$\rangle$ |  $\langle$73,F$\rangle$ $\langle$55,T$\rangle$ $\langle$21,T$\rangle$ |  $\langle$67,T$\rangle$
$\langle$44,7$\rangle$ $\langle$19,4$\rangle$ |  |  $\langle$78,4$\rangle$ $\langle$41,7$\rangle$ $\langle$16,1$\rangle$ $\langle$2,0$\rangle$ |  $\langle$71,F$\rangle$ $\langle$50,F$\rangle$ $\langle$20,T$\rangle$ |  $\langle$57,T$\rangle$
$\langle$42,3$\rangle$ $\langle$18,7$\rangle$ |  |  $\langle$78,3$\rangle$ $\langle$40,1$\rangle$ $\langle$15,4$\rangle$ $\langle$1,0$\rangle$ |  $\langle$70,F$\rangle$ $\langle$46,T$\rangle$ $\langle$20,T$\rangle$ |  $\langle$32,T$\rangle$
$\langle$39,0$\rangle$ $\langle$13,0$\rangle$ |  |  $\langle$78,1$\rangle$ $\langle$38,3$\rangle$ $\langle$14,7$\rangle$ $\langle$1,0$\rangle$ |  $\langle$65,F$\rangle$ $\langle$45,T$\rangle$ $\langle$20,T$\rangle$ |  $\langle$7,F$\rangle$
$\langle$36,0$\rangle$ $\langle$12,0$\rangle$ |  |  $\langle$53,6$\rangle$ $\langle$28,1$\rangle$ $\langle$5,0$\rangle$ $\langle$1,0$\rangle$ |  $\langle$64,F$\rangle$ $\langle$30,T$\rangle$ $\langle$10,4$\rangle$ |
Figure 9: Populated auxiliary store after an execution of annotated Odd-Even
Transposition Sort. The order of stack elements is read from top to bottom,
beginning in the leftmost column. For example, $\langle$78,7$\rangle$ is the
head of the stack l, while $\langle$1,0$\rangle$ is the bottom element.

With the operational semantics of annotated programs introduced, we now
present an example of one step of annotated execution. Recall the sorting
program introduced in Section 3.3, and the executed annotated version of this
program in Figure 8. One important step of this execution is part of the array
declaration that initialises the second element of l to 3, namely l[1] = 3
$\langle 2\rangle$ as on line 3. Firstly, we consider the full program AP
where this statement is executed next, namely AP = begin b1 l[1] = 3
(pa,$\langle\leavevmode\nobreak\ \rangle$); AQ end, where AQ is the rest of
the program (lines 4–56) and pa is the statement path b1.0. The inference tree
of this step is given below.

$\prooftree\Hypo{\texttt{m}=\emph{next}(\emph{})}\Hypo{\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)}\Hypo{\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}\Infer
3[\text{[D2a]}]{(\texttt{l[1] = 3
(pa,$\langle\rangle$);}\mid\delta,\sigma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip
$\langle\texttt{m}\rangle$;}\mid\delta^{\prime},\sigma^{\prime},\square)}\Infer
1[\text{[S1a]}]{(\texttt{l[1] = 3 (pa,$\langle\rangle$);
AQ}\mid\delta,\sigma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{skip $\langle\texttt{m}\rangle$;
AQ}\mid\delta^{\prime},\sigma^{\prime},\square)}\Infer
1[\text{[B1a]}]{(\texttt{begin b1 l[1] = 3 (pa,$\langle\rangle$); AQ
end;}\mid\delta,\sigma,\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{begin b1 skip $\langle\texttt{m}\rangle$; AQ
end;}\mid\delta^{\prime},\sigma^{\prime},\square)}$

The program state produced after execution of this step is such that
$\sigma^{\prime}$ = $\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto\texttt{v}]$
and $\delta^{\prime}$ = $\delta[\texttt{(m,$\sigma$($\sigma$({l})+{n}))
$\rightharpoonup$ l)}]$. This shows that the old value of this memory location
(namely 0) is saved to $\delta$. This process can be repeated for all steps of
this execution.

######  Example 5.

Figure 8 shows an executed annotated version of the program discussed in
Section 3.3. This annotated version is produced via _ann_(P __), where P is
the program in Section 3.3. As can be seen, the main difference here is that
statements now contain identifier stacks. The interleaving order of this
program can be read from the identifier stacks within each statement. After
this execution, the array is sorted into ascending order, namely l =
[1,3,4,6,7].

As the program executes, the auxiliary store is populated as shown in Figure
9. For example, the pair $\langle 29,7\rangle$ on the stack temp indicates
that the statement using identifier 29 (line 38 in Figure 8) overwrites the
variable temp and the value 7, which be lost in traditional execution, is now
saved. Not all previous values of count are saved as most assignments to it
are constructive, with values re-calculated during reversal. The identifiers
76,66,56 and 31 are associated to count += 1 to capture interleaving order,
but do not appear in $\delta$. $\hfill\blacksquare$

###  4.6 Proving Correctness of Annotation

Our first result compares the execution of an original and the corresponding
annotated program. The only difference is that the annotated execution also
populates the auxiliary store. Theorem 1 states the annotation result.

######  Theorem 1.

(Annotation result) Let P be an original program and AP be the corresponding
annotated version $ann($P$)$. Further let $\square$ be the tuple
{$\sigma$,$\gamma$,$\mu$,$\beta$} of initial program state environments, and
$\delta$ be the initial auxiliary store.

If an execution $(\textup{{P} $\mid$ $\delta$,
$\square$})\hookrightarrow^{*}(\textup{{skip} $\mid$ $\delta$,
$\square^{\prime}$})$ exists, for some program state $\square^{\prime}$, then
there exists an annotated execution $(\textup{{AP} $\mid$ $\delta$,
$\square_{1}$})\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\textup{{skip
I} $\mid$ $\delta^{\prime}$, $\square_{1}^{\prime}$})$ for some I,
$\square_{1}$, $\square_{1}^{\prime}$ such that $\square_{1}\approx\square$
and $\square_{1}^{\prime}\approx\square^{\prime}$, and some auxiliary store
$\delta^{\prime}$.

###### Proof.

This is via induction on the length of the execution of an original program P,
namely
$(\texttt{P}\mid\delta,\square)\hookrightarrow^{*}(\texttt{skip}\mid\delta,\square^{\prime})$,
and the corresponding execution of the annotated version AP, namely
$(\texttt{AP}\mid\delta,\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip}\mid\delta^{\prime},\square^{\prime})$.
Each rule [R] within the traditional semantics has a corresponding rule [Ra]
within the forward semantics (Section 4.4). We first consider all base cases
(executions with transition length 1), namely original executions via the
rules [P3], [D1] and [W1]. Each of the corresponding annotated rules, namely
[P3a], [D1a] and [W1a], is shown to behave identically with respect to the
program state while modifying the auxiliary store. Therefore each base case
holds.

We briefly describe the induction step. We first assume that Theorem 1 holds
for all program executions of length $k$ such that $k\geq 1$, namely
$(\texttt{Q}\mid\delta_{1},\square_{1})\hookrightarrow^{*}(\texttt{skip}\mid\delta_{1},\square_{1}^{\prime})$.
Then we assume our original program has execution length $k$ \+ $1$, namely
$(\texttt{T}\mid\delta_{2},\square_{2})\hookrightarrow^{*}(\texttt{skip}\mid\delta_{2},\square_{2}^{\prime})$.
This assumed execution can then be rewritten to state the first step via some
transition rule [R] as
$(\texttt{T}\mid\delta_{2},\square_{2})\hookrightarrow(\texttt{T${}^{\prime}$}\mid\delta_{2},\square_{2}^{\prime\prime})\hookrightarrow^{*}(\texttt{skip}\mid\leavevmode\nobreak\
\delta_{2},\square_{2}^{\prime})$.

Considering each rule [R] from Section 4.4, we can then see that there exists
a corresponding transition rule of the annotated execution that behaves
identically w.r.t. the store. In some cases, for example [S1a], [P1a] and
[I2a], there is no difference other than the presence of the auxiliary store
(which is not used). All other rules, including [D1a], [I4a] and [H1a], behave
identically w.r.t the program state while differing on the use of the
auxiliary store (as required). Finally the induction hypothesis can be applied
to the remaining, shorter execution (namely
$(\texttt{T${}^{\prime}$}\mid\delta_{2},\square_{2}^{\prime\prime})\hookrightarrow^{*}(\texttt{skip}\mid\delta_{2},\square_{2}^{\prime})$).
Therefore Theorem 1 is valid. ∎

##  5 Inversion

The previous sections introduced, and proved correct, a modified forward
execution that saves information necessary for reversal. In this section, we
describe the process of using this information to reverse the execution.

Inversion produces our inverted version. This is of the same syntax as
annotated versions (Figure 4), but with IP and IS representing inverted
programs and statements respectively). The function _inv_ :
$\mathbb{AP}\rightarrow\mathbb{IP}$ is defined in Figure 10, takes an
annotated program and produces the corresponding inverted version. The
inversion of a destructive assignment produces the same statement. This may be
counter-intuitive, however the additional reversal information saved onto
$\delta$ allows the statement to be correctly reversed. We do not use RESTORE
statements similar to those used by RCC and discussed in Section 2.
Maintaining the original statement both helps our proof of correctness, and
the application of our approach to debugging [23], helping a debugger to
understand the current position within the reversal more easily. It is
important to note here that the inverted version is a forward-executing
program, simulating reversal by beginning in the final program state and
restoring to the initial state. To achieve this, an inverse execution must use
both the identifiers and lost information.

$\displaystyle inv(\texttt{$\varepsilon$})=\texttt{$\varepsilon$}$
$\displaystyle inv(\texttt{AS;AP})=inv(\texttt{AP});inv(\texttt{AS})$
$\displaystyle inv(\texttt{AP par AQ})=inv(\texttt{AP})\texttt{ par
}inv(\texttt{AQ})$ $\displaystyle inv(\texttt{skip I})=\texttt{skip I}$
$\displaystyle inv(\texttt{X = e (pa,A)})=\texttt{X = e (pa,A)}$
$\displaystyle inv(\texttt{X += e (pa,A)})=\texttt{X -= e (pa,A)}$
$\displaystyle inv(\texttt{X -= e (pa,A)})=\texttt{X += e (pa,A)}$
$\displaystyle inv(\texttt{if In b then AP else AQ end (pa,A)})=$ if In b then
$inv($AP$)$ else $inv($AQ$)$ end (pa,A) $\displaystyle inv(\texttt{while Wn b
do AP end (pa,A)})=\texttt{while Wn b do $inv($AP$)$ end (pa,A)}$
$\displaystyle inv(\texttt{begin Bn AP end})=\texttt{begin Bn $inv($AP$)$
end}$ $\displaystyle inv(\texttt{var X = e (pa,A)})=\texttt{remove X = e
(pa,A)}$ $\displaystyle inv(\texttt{arr[n] name (pa,A)})=\texttt{remove arr[n]
name (pa,A)}$ $\displaystyle inv(\texttt{proc Pn n is AP end
(pa,A)})=\texttt{remove Pn n is $inv($AP$)$ end (pa,A)}$ $\displaystyle
inv(\texttt{call Cn n (pa,A)})=\texttt{call Cn n (pa,A)}$ $\displaystyle
inv(\texttt{runc Cn AP end A})=\texttt{runc Cn $inv($AP$)$ A}$ $\displaystyle
inv(\texttt{remove Pn n is AP end (pa,A)})=\texttt{proc Pn n is $inv($AP$)$
end (pa,A)}$ $\displaystyle inv(\texttt{remove arr[n] name
(pa,A)})=\texttt{arr[n] name (pa,A)}$ $\displaystyle inv(\texttt{remove X = e
(pa,A)})=\texttt{var X = e (pa,A)}$ Figure 10: Partial definition of the
Inversion function $inv$, shown in full in Appendix A.2.

###  5.1 Using Captured Interleaving Order

All interleaving decisions when running an inverted program are made using the
identifiers assigned to statements during forward execution. Using the
execution sequence and beginning with the statement with the highest
previously used identifier (via _previous_(__)), the reverse execution is
determined by using identifiers in descending order.

######  Example 6.

Recall Example 4 of identifier use. The reverse execution begins with
_previous_(__) = 9 (the final identifier used during forward execution). The
first execution step is either opening the inverted while loop (identifier 8)
or the assignment Y = 12 (identifier 9). Identifiers used in descending order
determine which must happen, namely the assignment. This process repeats until
all statements (and identifiers) have been inverted. $\hfill\blacksquare$

Using identifiers in this way follows _backtracking order_ , where statements
are reversed in exactly the inverted order of the forward execution [3]. A
possible relaxation of backtracking reversibility is named _causal-consistent_
reversibility [9, 40], where a step of an execution can be reversed (out of
backtracking order) provided all of its consequences have previously been
undone. Currently we support a limited form of this relaxation. Skip steps,
which have no effect on the program state, do not require identifiers and can
be undone according to causal-consistent reversibility.

###  5.2 Restoring Unrecoverable Information

During an annotated execution we have saved unrecoverable information. Each
statement can now be reversed, many of which will make use of this additional
information. We note here that as reversal information is used, it is also
removed from $\delta$. An initially empty auxiliary store will be empty again
after complete inverse execution.

Assignments are reversed by restoring the variable or array element to the
previous value it held. Destructive assignments retrieve this from $\delta$,
while constructive assignments can easily be reversed (e.g. an increment
becomes a decrement). Control flow of conditionals and while loops are
determined by retrieving boolean values from $\delta$. Removal statements are
reversed by re-declaring the variable, array or procedure, using old values
saved onto $\delta$. More details of this are given below when presenting
operational semantics of inverted programs.

###  5.3 Operational Semantics of Inverted Programs

We now use SOS to define a transition system describing inverse execution,
correspondingly to in Section 4.4. Each _configuration_ is now composed of an
inverse program IP and program state $\square$, written as
$(\texttt{IP}\mid\square)$. Each transition between two configurations is part
of the transition relation $\stackrel{{\scriptstyle}}{{\rightsquigarrow}}$,
defined as the least relation generated by the following set of transition
rules. Let $\stackrel{{\scriptstyle}}{{\rightsquigarrow}}^{*}$ be the
reflexive and transitive closure of
$\stackrel{{\scriptstyle}}{{\rightsquigarrow}}$. We now give a syntax-
directed, small step semantics that defines inverse execution. We again use
$\hookrightarrow^{*}_{\texttt{a}}$ and $\hookrightarrow^{*}_{\texttt{b}}$ to
represent a step of arithmetic and boolean expression evaluation respectively.
As before _identifier steps_ are transitions using the arrow
$\stackrel{{\scriptstyle m}}{{\rightsquigarrow}}$, where m is an identifier,
while skip steps use the arrow
$\stackrel{{\scriptstyle}}{{\rightsquigarrow}}_{s}$. Transitions that may, or
may not, use an identifier are written using the arrow
$\stackrel{{\scriptstyle\circ}}{{\rightarrow}}$. As before, the components of
the following rules introduced for reversal are indicated using the colour
blue.

There is close correspondence between the rules here and in Section 4.4.
Matching pairs of rules are named accordingly, for example [D1a] and [D1r]
with [D1r] being the version of [D1a] adapted for reverse execution. The
semantics of both sequential and parallel composition and of block statements
are omitted. Taking the corresponding rules in Section 4.4, the annotated
versions are produced by changing all arrows to
$\stackrel{{\scriptstyle}}{{\rightsquigarrow}}$ and substituting IP and IS for
AP and AS respectively. We also note that evaluation is only performed during
reversal for constructive assignments. No boolean expressions or destructive
assignment expressions are evaluated. This potentially saves execution time
when compared to reversible languages [35], each of which evaluates post-
conditions.

Assignment Reversing a destructive assignment restores the variable ([D1r]) or
array element ([D2r]) to the old value saved on $\delta$ (e.g.
$\sigma[\texttt{l}\mapsto\texttt{v}]$). A constructive assignment is reversed
by evaluating the expression and incrementing ([C1r], [C4r]) or decrementing
([C2r], [C3r]) the variable or array element respectively.

$\displaystyle\text{[D1r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})\quad\texttt{$\delta($X$)$}=\texttt{(m,v):X${}^{\prime}$}}\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
= e (pa,A)}\mid\delta,\sigma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid{\color[rgb]{0,0,1}\delta[\texttt{X/X${}^{\prime}$}]},\sigma[\texttt{l}\mapsto\texttt{v}],\square)}$
$\displaystyle\text{[D2r]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad\texttt{$\delta($name$)$}=\texttt{(m,v):name${}^{\prime}$}\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto\texttt{v}]\quad{\color[rgb]{0,0,1}\delta^{\prime}=\delta[\texttt{name/name${}^{\prime}$)}]}\end{aligned}}{(\texttt{name[e]
= e${}^{\prime}$
(pa,A)}\mid\sigma,\gamma,\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\sigma^{\prime},\gamma,\delta^{\prime},\square)}$
$\displaystyle\text{[C1r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
+= e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\delta,\sigma[\texttt{l}\mapsto\sigma(\texttt{l})+\texttt{v}],\gamma,\square)}$
$\displaystyle\text{[C2r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\quad\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}{(\texttt{X
-= e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\delta,\sigma[\texttt{l}\mapsto\sigma(\texttt{l})-\texttt{v}],\gamma,\square)}$
$\displaystyle\text{[C3r]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad(\texttt{e${}^{\prime}$
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto(\sigma(\texttt{l})+\texttt{n})-\texttt{v}]\end{aligned}}{(\texttt{name[e]
-= e${}^{\prime}$
(pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\delta,\sigma^{\prime},\gamma,\square)}$
$\displaystyle\text{[C4r]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad(\texttt{e
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{n}\mid\sigma,\gamma,\square)\quad(\texttt{e${}^{\prime}$
pa}\mid\sigma,\gamma,\square)\hookrightarrow^{*}_{\texttt{a}}(\texttt{v}\mid\sigma,\gamma,\square)\\\\[-3.0pt]
&\texttt{$evalV($name,pa,$\gamma)$}=\texttt{l}\quad\sigma^{\prime}=\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto(\sigma(\texttt{l})+\texttt{n})+\texttt{v}]\end{aligned}}{(\texttt{name[e]
+= e${}^{\prime}$
(pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\delta,\sigma^{\prime},\gamma,\square)}$

Conditional Statement Opening a conditional does not evaluate the condition
and instead retrieves a true ([I1rT]) or false ([I1rF]) value from $\delta$
(e.g. $\delta($B$)$ = (m,T):B′). The true ([I2r]) or false ([I3r]) branch is
then executed, before the conditional closes ([I4r] or [I5r]) using an
identifier.

$\displaystyle\text{[I1rT]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})\quad\texttt{$\delta($B$)$}=\texttt{(m,T):B${}^{\prime}$}}}{(\texttt{if
In b then IP else IQ end (pa,A)}\mid\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{if In T then IP else IQ end
(pa,{\color[rgb]{0,0,1}A${}^{\prime}$})}\mid{\color[rgb]{0,0,1}\delta[\texttt{B/B${}^{\prime}$}]},\square)}$
$\displaystyle\text{[I1rF]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})\quad\texttt{$\delta($B$)$}=\texttt{(m,F):B${}^{\prime}$}}}{(\texttt{if
In b then IP else IQ end (pa,A)}\mid\delta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{if In F then IP else IQ end
(pa,{\color[rgb]{0,0,1}A${}^{\prime}$})}\mid{\color[rgb]{0,0,1}\delta[\texttt{B/B${}^{\prime}$}]},\square)}$
$\displaystyle\text{[I2r]}\quad\frac{(\texttt{IP}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{IP${}^{\prime}$}\mid\square^{\prime})}{(\texttt{if
In T then IP else IQ end
(pa,A)}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{if
In T then IP${}^{\prime}$ else IQ end (pa,A)}\mid\square^{\prime})}$
$\displaystyle\text{[I3r]}\quad\frac{(\texttt{IQ}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{IQ${}^{\prime}$}\mid\square^{\prime})}{(\texttt{if
In F then IP else IQ end
(pa,A)},\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{if
In F then IP else IQ${}^{\prime}$ end (pa,A)}\mid\square^{\prime})}$
$\displaystyle\text{[I4r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}}{(\texttt{if
In T then skip I else IQ end (pa,A)}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\square)}$
$\displaystyle\text{[I5r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}}{(\texttt{if
In F then AP else skip I end (pa,A)}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\square)}$

While Loop A while loop either has zero iterations ([W1r]), or begins with a
first iteration ([W3r]). This first iteration inserts a renamed copy (via
_IreL_(__)) of the loop body into $\beta$ ($\beta[\texttt{Wn $\Rightarrow$
IR}]$). The loop body is then executed step-by-step ([W5r]) until the loop
body reaches skip. At this point, the iteration is finished and the loop is
reset ([W6r]). All other iterations are performed ([W4r]) while T remains at
the head of the boolean sequence
($\texttt{$\delta($W$)$}=\texttt{(m,T):W${}^{\prime}$}$). When this sequence
contains an F, no more iterations are required and the loop closes ([W2r]).

$\displaystyle\text{[W1r]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{previous}(\emph{})\quad\texttt{A}=\texttt{m:A${}^{\prime}$}}\quad\texttt{$\beta($Wn$)$}=\emph{und}\quad{\color[rgb]{0,0,1}\texttt{$\delta($W$)$}=\texttt{(m,F):W${}^{\prime}$}}}{(\texttt{while
Wn b do IP end (pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid{\color[rgb]{0,0,1}\delta[\texttt{W/W${}^{\prime}$}]},\beta,\square)}$
$\displaystyle\text{[W2r]}\hskip
5.69046pt\frac{{\color[rgb]{0,0,1}\texttt{m}=\emph{previous}(\emph{})\quad\texttt{A}=\texttt{m:A${}^{\prime}$}}\quad\texttt{$\beta($Wn$)$}=\emph{def}\quad{\color[rgb]{0,0,1}\texttt{$\delta($W$)$}=\texttt{(m,F):W${}^{\prime}$}}}{(\texttt{while
Wn b do IP end (pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid{\color[rgb]{0,0,1}\delta[\texttt{W/W${}^{\prime}$}]},\beta[\texttt{Wn}],\square)}$
$\displaystyle\text{[W3r]}\hskip 5.69046pt\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{previous}(\emph{})\quad\texttt{A}=\texttt{m:A${}^{\prime}$}}\quad\texttt{$\beta($Wn$)$}=\emph{und}\quad{\color[rgb]{0,0,1}\texttt{$\delta($W$)$}=\texttt{(m,T):W${}^{\prime}$}\quad\texttt{$\delta($WI$)$}=\texttt{(m,C):WI${}^{\prime}$}}\\\\[-3.0pt]
&\texttt{IR}=\texttt{while Wn T do IP${}^{\prime}$ end
(pa,A${}^{\prime}$)}\quad{\color[rgb]{0,0,1}\delta^{\prime}=\delta[\texttt{W/W${}^{\prime}$},\texttt{WI/WI${}^{\prime}$}]}\quad\beta^{\prime}=\beta[\texttt{Wn
$\Rightarrow$ IR}]\end{aligned}}{(\texttt{while Wn b do IP end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{while Wn T do IP${}^{\prime}$ end
(pa,{\color[rgb]{0,0,1}A${}^{\prime}$})}\mid\delta^{\prime},\beta^{\prime},\square)}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where
}\texttt{IP${}^{\prime}$}=\emph{IreL}(\emph{setAI}(\texttt{IP},\texttt{C}\emph{})\emph{})$
$\displaystyle\text{[W4r]}\hskip 5.69046pt\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{m}=\emph{previous}(\emph{})\quad\texttt{A}=\texttt{m:A${}^{\prime}$}}\quad\texttt{$\beta($Wn$)$}=\emph{def}\quad{\color[rgb]{0,0,1}\texttt{$\delta($W$)$}=\texttt{(m,T):W${}^{\prime}$}\quad\texttt{$\delta($WI$)$}=\texttt{(m,C):WI${}^{\prime}$}}\\\\[-3.0pt]
&\texttt{IR}=\texttt{while Wn b do }\emph{IreL}(\texttt{IP}\emph{})\texttt{
end
(pa,A${}^{\prime}$)}\quad{\color[rgb]{0,0,1}\delta^{\prime}=\delta[\texttt{W/W${}^{\prime}$}]}\quad\beta^{\prime}=\beta[\texttt{Wn
$\Rightarrow$ IR}]\end{aligned}}{(\texttt{while Wn b do IP end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{while Wn T do
}\emph{IreL}(\texttt{IP}\emph{})\texttt{ end
(pa,{\color[rgb]{0,0,1}A${}^{\prime}$})}\mid\delta^{\prime},\beta^{\prime},\square)}$
$\displaystyle\text{[W5r]}\hskip
5.69046pt\frac{\texttt{$\beta($Wn$)$}=\emph{def}\quad(\texttt{IP}\mid\delta,\beta,\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{IP${}^{\prime}$}\mid\delta^{\prime},\beta^{\prime},\square^{\prime})}{(\texttt{while
Wn T do IP end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{while
Wn T do IP${}^{\prime}$ end
(pa,A)}\mid\delta^{\prime},\beta^{\prime\prime},\square^{\prime})}$
$\displaystyle\phantom{\text{[W3a]}\quad}\text{where
}\beta^{\prime\prime}=\beta^{\prime}[\emph{refW}(\texttt{Wn},\texttt{IP${}^{\prime}$}\emph{})]$
$\displaystyle\text{[W6r]}\hskip
5.69046pt\frac{\texttt{$\beta($Wn$)$}=\texttt{while Wn b do IP end
(pa,A)}}{(\texttt{while Wn T do skip I end
(pa,A)}\mid\delta,\beta,\square)\stackrel{{\scriptstyle}}{{\rightsquigarrow}}_{s}(\texttt{while
Wn b do IP end (pa,A)}\mid\delta,\beta,\square)}$

Variable, Procedure and Array Declaration A declaration reverses a removal
statement. Variable declaration ([L1r]) recreates the necessary mappings and
initialises this to the final value held on $\delta$
($\sigma[\texttt{l}\mapsto\texttt{v${}^{\prime}$}]$ and
$\gamma[(\texttt{X},\texttt{Bn})\Rightarrow\texttt{l}]$). Procedure
declaration ([L2r]) recreates the basis mapping from the inverted program
without using reversal information
($\mu[\texttt{Pn}\Rightarrow\texttt{(n,IP)}]$). Array declaration ([L3r])
recreates the array by initialising a block of consecutive memory locations
reserving a block of memory and initialising each element to their final
values on $\delta$
($\sigma[\texttt{l}\mapsto\texttt{l1},\\{\texttt{l1},\ldots,\texttt{l1}\texttt{+n}\\}\mapsto\delta(\texttt{name},\texttt{m})]$).

$\displaystyle\text{[L1r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})\quad\texttt{$\delta($X$)$}=\texttt{(m,v${}^{\prime}$):X${}^{\prime}$}}\quad\emph{nextLoc}(\sigma\emph{})=\texttt{l}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}}{(\texttt{var
X = e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid{\color[rgb]{0,0,1}\delta[\texttt{X/X${}^{\prime}$}]},\sigma[\texttt{l}\mapsto\texttt{v${}^{\prime}$}],\gamma[(\texttt{X},\texttt{Bn})\Rightarrow\texttt{l}],\square)}$
$\displaystyle\text{[L2r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}}{(\texttt{proc
Pn n is IP (pa,A)}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\mu[\texttt{Pn}\Rightarrow\texttt{(n,IP)}],\square)}$
$\displaystyle\text{[L3r]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\emph{nextLoc}(\sigma\emph{})=\texttt{l}\quad\emph{nextLocBlock}(\sigma,n\emph{})=\texttt{l1}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}\\\\[-3.0pt]
&\sigma^{\prime}=\sigma[\texttt{l}\mapsto\texttt{l1},\\{\texttt{l1},\ldots,\texttt{l1}\texttt{+n}\\}\mapsto\delta(\texttt{name},\texttt{m})]\quad\gamma^{\prime}=\gamma[(\texttt{name},\texttt{Bn})\Rightarrow\texttt{l}]\end{aligned}}{(\texttt{arr[n]
name (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\sigma^{\prime},\gamma^{\prime},\square)}$

Variable, Procedure and Array Removal Removal statements undo the effect of
declaration statements. Variable removal ([H1r]) removes the mappings for this
variable and restores the memory location to 0
($\sigma[\texttt{l}\mapsto\texttt{0}]$). Procedure removal ([H2r]) simply
removes the renamed copy of the body from $\mu$ ($\mu[\texttt{Pn}]$). Array
removal ([H3r]) removes the mapping for this array, restoring each memory
location it used to 0
($\sigma[\texttt{l}\mapsto\texttt{0},\\{\texttt{l1},\ldots,\texttt{l1}\texttt{+n}\\}\mapsto
0]$).

$\displaystyle\text{[H1r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\texttt{$\gamma($X,Bn$)$}=\texttt{l}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}}{(\texttt{remove
X = e (pa,A)}\mid\delta,\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\delta,\sigma[\texttt{l}\mapsto\texttt{0}],\gamma[(\texttt{X},\texttt{Bn})],\square)}$
$\displaystyle\text{[H2r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\texttt{$\mu$(Pn)}=\emph{def}}{(\texttt{remove
Pn n is IP (pa,A)}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\mu[\texttt{Pn}],\square)}$
$\displaystyle\text{[H3r]}\quad\frac{\begin{aligned}
&{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\texttt{pa}=\texttt{Bn:pa${}^{\prime}$}\quad\texttt{$\gamma($name,Bn$)$}=\texttt{l}\quad\texttt{l1}=\sigma(\texttt{l})\\\\[-3.0pt]
&\sigma^{\prime}=\sigma[\texttt{l}\mapsto\texttt{0},\\{\texttt{l1},\ldots,\texttt{l1}\texttt{+n}\\}\mapsto
0]\quad\gamma^{\prime}=\gamma[(\texttt{name},\texttt{Bn})]\end{aligned}}{(\texttt{remove
arr[n] name (pa,A)}\mid\sigma,\gamma,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid\sigma^{\prime},\gamma^{\prime},\square)}$

Procedure Call Opening an inverse procedure call ([G1r]) reverses the closure
by recreating the copy of the procedure body in $\mu$, using the inverse
renaming function _IreP_(__) to include the appropriate stack names (
$\mu[\texttt{Cn}\Rightarrow\texttt{(n,IP${}^{\prime}$)}]$). The body is then
executed ([G2r]), before the call is closed ([G3a]) by removing the copy from
$\mu$ ($\mu[\texttt{Cn}]$).

$\displaystyle\text{[G1r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\emph{evalP}(\texttt{n,pa}\emph{})=\texttt{Pn}\quad\mu(\texttt{Pn})=\texttt{(n,IP)}\quad{\color[rgb]{0,0,1}\texttt{$\delta($Pr$)$}=\texttt{(m,C):Pr${}^{\prime}$}}}{(\texttt{call
Cn n (pa,A)}\mid\delta,\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{runc Cn IP${}^{\prime}$ end
{\color[rgb]{0,0,1}A${}^{\prime}$}}\mid{\color[rgb]{0,0,1}\delta[\texttt{Pr/Pr${}^{\prime}$}]},\mu[\texttt{Cn}\Rightarrow\texttt{(n,IP${}^{\prime}$)}],\square)}$
$\displaystyle\phantom{[RG1]\quad}\text{where
}\texttt{IP${}^{\prime}$}=\emph{IreP}(\emph{setAI}(\texttt{IP},\texttt{C}\emph{}),\texttt{Cn}\emph{})$
$\displaystyle\text{[G2r]}\quad\frac{(\texttt{IP}\mid\mu,\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{IP${}^{\prime}$}\mid\mu^{\prime},\square^{\prime})}{(\texttt{runc
Cn IP end
A}\mid\mu,\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}(\texttt{runc
Cn IP${}^{\prime}$ end
A}\mid\mu^{\prime}[\emph{refC(}\texttt{Cn},\texttt{IP${}^{\prime}$}\emph{)}],\square^{\prime})}$
$\displaystyle\text{[G3r]}\quad\frac{{\color[rgb]{0,0,1}\texttt{A}=\texttt{m:A${}^{\prime}$}\quad\texttt{m}=\emph{previous}(\emph{})}\quad\texttt{$\mu$(Cn)}=\emph{def}}{(\texttt{runc
Cn skip I end A}\mid\mu,\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
{\color[rgb]{0,0,1}m:A}}\mid\mu[\texttt{Cn}],\square)}$

###  5.4 Inverted Odd-Even Transposition Sort

Before we discuss how inverted Odd-Even Transposition Sort works, we shall
show the reversal of a single step of execution of the annotated version that
we have presented in Section 4.5. Recall that this step is the first
assignment to the second array element, and the final program states
$\delta^{\prime}$, $\sigma^{\prime}$ and $\square$ are produced by the forward
execution of this statement. These are the starting states for the reversal of
this assignment. We consider the inverse program IP whose next statement to
execute (reverse) is this assignment, such that IP = begin b1 l[1] = 3
(pa,$\langle$2$\rangle$); IQ end. Note that IQ is the inverted version of the
statements still left to reverse, namely those on lines 55–56. The inference
tree is shown below.

$\prooftree\Hypo{\texttt{m}=\emph{previous}(\emph{})}\Hypo{\delta(\texttt{l})=\texttt{(m,v):X${}^{\prime}$}}\Hypo{\texttt{$evalV($X,pa,$\gamma)$}=\texttt{l}}\Infer
3[\text{[D2r]}]{(\texttt{l[1] = 3
(pa,$\langle$2$\rangle$);}\mid\delta^{\prime},\sigma^{\prime},\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip
$\langle\rangle$;}\mid\sigma^{\prime\prime},\delta^{\prime\prime},\square)}\Infer
1[\text{[S1a]}]{(\texttt{l[1] = 3 (pa,$\langle$2$\rangle$);
IQ}\mid\delta^{\prime},\sigma^{\prime},\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{skip $\langle\rangle$;
IQ}\mid\sigma^{\prime\prime},\delta^{\prime\prime},\square)}\Infer
1[\text{[B1a]}]{(\texttt{begin b1 l[1] = 3 (pa,$\langle$2$\rangle$); IQ
end}\mid\delta^{\prime},\sigma^{\prime},\square)\stackrel{{\scriptstyle
m}}{{\rightsquigarrow}}(\texttt{begin b1 skip $\langle\rangle$; IQ
end}\mid\sigma^{\prime\prime},\delta^{\prime\prime},\square)}$

This step produces the states $\sigma^{\prime\prime}$ =
$\sigma[(\sigma(\texttt{l})+\texttt{n})\mapsto\texttt{v}]$ and
$\delta^{\prime}$ = $\delta[\texttt{name/name${}^{\prime}$)}]$. Recalling that
v = 0, this means that $\sigma^{\prime\prime}$ and $\delta^{\prime\prime}$ are
equivalent to $\sigma$ and $\delta$ respectively, and therefore that the
reversal is correct.

⬇

1begin b1.0

2 ${\color[rgb]{150,0,150}\texttt{arr[5]}}\leavevmode\nobreak\
\texttt{l;}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 78\rangle};$

3 while w1.0 (count1 < 4) do

4 $\texttt{count -= 1}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
76,66,56,31\rangle};$

5 //odd phase

6 par {

7 if i4.0 (l[1] > l[2]) then

8 begin b4.0

9 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 29\rangle};$

10 $\texttt{l[2] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
28\rangle};$

11 $\texttt{l[1] = l[2]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
27\rangle};$

12 $\texttt{temp = l[1]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
26\rangle};$

13 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 25\rangle}$

14 end

15
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 73,72,65,63,50,47,30,23\rangle}$

16 } {

17 if i5.0 (l[3] > l[4]) then

18 begin b5.0

19 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 54\rangle};$

20 $\texttt{l[4] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
53\rangle};$

21 $\texttt{l[3] = l[4]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
52\rangle};$

22 $\texttt{temp = l[3]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
51\rangle};$

23 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 49\rangle}$

24 end

25
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 75,74,64,62,55,48,24,22\rangle}$

26 ${\color[rgb]{150,0,150}\texttt{\\}}};$

27 //even phase

28 par {

29 if i2.0 (l[0] > l[1]) then

30 begin b2.0

31 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 42,18\rangle};$

32 $\texttt{l[1] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
40,17\rangle};$

33 $\texttt{l[0] = l[1]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
38,14\rangle};$

34 $\texttt{temp = l[0]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
36,12\rangle};$

35 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 35,10\rangle}$

36 end

37
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 70,68,61,58,45,33,21,8\rangle}$

38 } {

39 if i3.0 (l[2] > l[3]) then

40 begin b3.0

41 ${\color[rgb]{150,0,150}\texttt{var}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 44,19\rangle};$

42 $\texttt{l[3] = temp}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
43,16\rangle};$

43 $\texttt{l[2] = l[3]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
41,19\rangle};$

44 $\texttt{temp = l[2]}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
39,13\rangle};$

45 ${\color[rgb]{150,0,150}\texttt{remove}}\leavevmode\nobreak\ \texttt{temp =
0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 37,118\rangle}$

46 end

47
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 71,69,60,59,46,34,20,9\rangle}$

48 }

49
${\color[rgb]{150,0,150}\texttt{end}}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 77,67,57,32\rangle};$

50

51 //inverting array declaration

52 $\texttt{count = 0}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
6\rangle};$

53 $\texttt{l[4] = 6}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
5\rangle};$ $\texttt{l[3] = 1}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 4\rangle};$

54 $\texttt{l[2] = 4}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
3\rangle};$ $\texttt{l[1] = 3}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\
\langle 2\rangle};$

55 $\texttt{l[0] = 7}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle
1\rangle};$

56 ${\color[rgb]{150,0,150}\texttt{remove[5]}}\leavevmode\nobreak\
\texttt{l}\quad{\color[rgb]{0,0,1}\leavevmode\nobreak\ \langle 0\rangle}$

57end

Figure 11: Inverted Odd-Even Transposition Sort. Empty else branches and paths
omitted.

######  Example 7.

Recall the executed annotated version of the sorting program in Example 5,
which we denote as AP. The inverted version of this program is produced via
_inv_(AP __) and is shown in Figure 11.

The overall statement order has been inverted, including within nested
constructs. For example, the block is the highest level construct, containing
local declarations (reversing forward removal statements), a block body and
local removals (reversing declaration statements). The block body still
consists of a loop which contains two sequentially composed parallel
statements, but with the ‘odd’ phase reversed first.

Complete execution of the program reverses the annotated execution. The number
of iterations of the loop, and the branches executed for all conditional
statements, are determined using boolean values (1 and 0 used for true and
false respectively) from the stacks W and B. Pairs stored on the stacks temp,
count and l are used to restore variables or array elements to their previous
values. For example, the pair (54,7) indicates the statement using identifier
54 overwrote the value 7 of the variable temp. So, the variable temp is
therefore restored to 7.

As reversal information is used, it is removed from $\delta$. Given that
$\delta$ was initially empty, after complete inverse execution $\delta$ is
again empty. This means our reversibility is garbage-free.
$\hfill\blacksquare$

###  5.5 Proving Correctness of Inversion

We now state our inversion result. Theorem 2 says that given the final state
produced by the matching annotated execution, the reverse execution restores
this to a state equivalent to that of before the forward execution.
Equivalence between program states, where one is used in a reverse execution,
is defined below (correspondingly to Definition 1). The inversion result also
restores the auxiliary store, showing our reversibility to be garbage-free.

######  Definition 2.

(Equivalent inverse states) Let $\square$ be the tuple of environments
{$\sigma$,$\gamma$,$\mu$,$\beta$,$\delta$} and $\square_{1}$ be the tuple of
annotated environments
{$\sigma_{1}$,$\gamma_{1}$,$\mu_{1}$,$\beta_{1}$,$\delta_{1}$}. $\square$ is
_equivalent_ to $\square_{1}$, written $\square\approx\square_{1}$, if and
only if:

  1. 1.

Same as part 1 in Definition 1.

  2. 2.

_d_($\beta$__) =_d_($\beta_{1}$__); $\beta(\textup{{Wn}})$ = AP,
$\beta_{1}(\textup{{Wn}})$ = IP, IP = $inv($AP$)$ for all Wn $\in$
_d_($\beta$__).

  3. 3.

_d_($\mu$__) =_d_($\mu_{1}$__); $\mu(\textup{{Pn}})$ = (n,AP),
$\mu_{1}(\textup{{Pn}})$ = (n,IP) and IP = $inv($AP$)$ for all Pn $\in$
_d_($\mu$__).

  4. 4.

$\delta$ = $\delta_{1}$

######  Theorem 2.

Let P be an original program, AP be the corresponding annotated version
$ann($P$)$, and AP′ be the executed version of AP. Further let $\square$ be
the tuple {$\sigma$,$\gamma$,$\mu$,$\beta$,$\delta$} of all initial state
environments.

If
$(\texttt{P}\mid\square)\hookrightarrow^{*}(\texttt{skip}\mid\square^{\prime})$
for some program state $\square^{\prime}$, and therefore by Theorem 1 the
annotated execution
$(\texttt{AP}\mid\square_{1})\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip
I}\mid\square_{1}^{\prime})$ exists for some I and program state
$\square_{1}^{\prime}$ such that
$\square_{1}^{\prime}\approx\square^{\prime}$, then there exists a
corresponding inverse execution
$(\emph{inv}(\texttt{AP${}^{\prime}$}\emph{})\mid\square_{2}^{\prime})\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}^{*}(\texttt{skip
I${}^{\prime}$}\mid\square_{2})$, for some program states
$\square_{2}^{\prime}$, $\square_{2}$, such that
$\square_{2}^{\prime}\approx\square_{1}^{\prime}$ and
$\square_{2}\approx\square_{1}$. Provided this holds, Definition 2 states that
$\delta_{2}$ = $\delta_{1}$, showing the reversal to be garbage-free.

Before proving this result, we consider the following challenges:

  1. 1.

Parallel composition allows different interleaving orders,

  2. 2.

Partially executed programs may not reach skip when inverted, or may not stop
at the corresponding position.

$\begin{array}[]{ccccc}(\texttt{P}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip
I}\mid\square^{\prime})&&${\Huge$\Rightarrow$}$1&&(\texttt{P}\mid\square)\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}}\leavevmode\nobreak\
(\texttt{skip I}\mid\square^{\prime})\\\ &&\\\ \text{?
}${\Huge$\downarrow$}$&&&&${\Huge$\Downarrow$}$2\\\ &&\\\
(\emph{inv${}^{+}$}(\texttt{P}\emph{})\mid\square_{1}^{\prime})\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}^{*}(\texttt{Q}\mid\square_{1})&&3${\Huge$\Leftarrow$}$&&(\emph{inv${}^{+}$}(\texttt{P}\emph{})\mid\square_{1}^{\prime})\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}^{*}}\leavevmode\nobreak\
(\texttt{Q}\mid\square_{1})\end{array}$

Figure 12: Diagram representation of proof outline

The first challenge considers different interleaving orders of the same
program introduced via our parallel operator. Statements of two programs in
parallel may interleave in different orders, producing different behaviours.
Some interleavings however may be “equivalent”, typically as a result of skip
steps performed in a different order. This can lead to a mismatch of skip
steps between a forward and reverse execution, impacting our proof of
correctness. In Section 5.5.1 we introduce the notion of _uniform execution_
to avoid this issue.

The second challenge concerns partially executed programs (defined later).
When reversing a complete program, we judge success as whether the inverted
version executes completely to skip. Imagine proving this via induction, where
after the first step of an execution we no longer have a complete execution.
The remaining execution will not reverse to skip, but to some intermediate
position, from which the first step can be reversed to reach skip. In Section
5.5.2 we overcome this by introducing _abort_ statements and _skip
equivalents_.

Given the two challenges, our method of proving the reversibility described
here to be correct is illustrated in Figure 12. We first convert an arbitrary
forward execution into an equivalent uniform execution ($\Rightarrow_{1}$),
then prove our property ($\Downarrow_{2}$) for uniform executions, before
converting back into a standard reverse execution. We now discuss this in more
detail.

####  5.5.1 Interleaving Parallel Composition

The semantics of parallel composition allows multiple different interleaving
orders of a given program. Different executions are equivalent when the order
of identifier steps is identical while the order of skip steps is different.
Since no skip steps alter the program state, each of these executions produces
the same final program state (hence executions are equivalent). Inverse skip
steps can also be applied in several different orders while preserving an
equivalent execution. This results in the potential for constructs to remain
“open” (so to speak) during an inverse execution for longer than during the
forward execution, adding difficultly to the task of matching rule uses
between a forward and reverse execution.

We avoid these difficulties by considering executions as a composition of
segments. Firstly let any arbitrary execution be named a _standard execution_.
We now introduce a _uniform execution_ , where each identifier step is
followed by all of the possible closing skip steps. A sequence starting with
an identifier step and followed by all its closing skip steps is called a
_segment_. All skip steps within a segment are said to have been ‘caused’ by
the preceding identifier step.

######  Definition 3.

(Uniform execution) A _uniform execution_ is a standard program execution
where all skip steps are performed as soon as they are available. A step of a
uniform execution is represented using$\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightarrow}}}\leavevmode\nobreak\
$and$\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}}\leavevmode\nobreak\
$for forward and reverse execution respectively.

We remark that skip steps within a uniform execution are not interleaved
across a parallel composition. This is due to identifier steps executed on one
side not being able to make skip steps available on the other. Therefore any
two equivalent standard executions (that is two transition sequences where the
order of identifier steps is identical, with skip steps potentially different)
will have the same uniform version. All skip steps from each sequence will be
performed as soon as they are available, which will be identical in both
cases. Consider Example 8 that shows a uniform version of a standard
execution.

######  Example 8.

Consider the concurrent program in Figure LABEL:sub@ex:standUni-program and
one possible standard execution captured with identifiers 0–2. Figure
LABEL:sub@ex:standUni-executions shows first the order of rule uses under this
standard execution (with the identifier it used or that caused it). [S2a] and
[B2a] are not executed as soon as available. The uniform execution contains
unchanged order of identifier steps (an equivalent execution), but with skip
steps performed as soon as possible. $\hfill\blacksquare$

⬇ 1par { 2 begin b1.0 3 $\texttt{X =
20}\quad{\color[rgb]{0,0,1}\langle\texttt{1}\rangle}$ 4 end 5} { 6 $\texttt{Y
= 2}\quad{\color[rgb]{0,0,1}\langle\texttt{0}\rangle}\texttt{;}$ 7 $\texttt{Z
= 4}\quad{\color[rgb]{0,0,1}\langle\texttt{2}\rangle}$ 8}

(a) Small program

Standard Execution [D1a] [D1a] [S2a] [D1a] [B1a] [P3a]
$\stackrel{{\scriptstyle 0}}{{\rightarrow}}$ $\stackrel{{\scriptstyle
1}}{{\rightarrow}}$ $\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$
$\stackrel{{\scriptstyle 2}}{{\rightarrow}}$
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$ Uniform Execution [D1a] [S2a]
[D1a] [B1a] [D1a] [P3a]
$\stackrel{{\scriptstyle 0}}{{\rightarrow}}$
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$ $\stackrel{{\scriptstyle
1}}{{\rightarrow}}$ $\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$
$\stackrel{{\scriptstyle 2}}{{\rightarrow}}$
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$

(b) Standard and uniform execution

Figure 13: The standard execution and a corresponding uniform execution of a
given program. Each execution is displayed as an ordered sequence of rule
labels, with the arrow from the corresponding transition shown below each. For
example, the rule [D1a] above the arrow $\stackrel{{\scriptstyle
1}}{{\rightarrow}}$ represents executing the statement X = 20, while the rule
[B1a] above the arrow $\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$
represents closing the block on line 4. Intermediate programs and states are
omitted.

One further consideration is of programs that begin with skip steps. This is a
special case of a uniform execution, where all skip steps performed at the
beginning have not been ‘caused’ by any identifier step. Such an execution
performs all initial skip steps in a fixed order, namely from the left side of
a parallel before those of the right, and in a depth first manner. This
ensures all equivalent executions have a single uniform version. Lemma 4
states that for any standard forward execution, there exists a uniform forward
execution that has the same behaviour (with respect to the program state). A
proof of this property uses Lemma 3 to show that statement reordering is
valid.

######  Lemma 3.

Given a sequence of two transitions where each is from the opposite side of a
parallel, these two transitions may be reordered in two specific circumstances
(depending on the type of each transition). Let P be an annotated program and
$\square$ be the tuple $\\{\gamma,\sigma,\mu,\beta,\delta\\}$ of initial
program state environments.

  1. 1.

If
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{1}}(\texttt{P${}^{\prime}$}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{2}}(\texttt{P${}^{\prime\prime\prime}$}\mid\square)$
exists, for some programs P′ and P′′′, such that the transition
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{1}}$ is from the opposite side
of a parallel composition to the transition
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{2}}$, then there exists the
reordered execution
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{2}}(\texttt{P${}^{\prime\prime}$}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{1}}(\texttt{P${}^{\prime\prime\prime}$}\mid\square)$
for some program P′′.

  2. 2.

If $(\texttt{P}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{P${}^{\prime}$}\mid\square^{\prime})\stackrel{{\scriptstyle}}{{\rightarrow}}_{S}(\texttt{P${}^{\prime\prime\prime}$}\mid\square^{\prime})$
exists, for some programs P′, P′′′ and program state $\square^{\prime}$, such
that the transition $\stackrel{{\scriptstyle m}}{{\rightarrow}}$ is from the
opposite side of a parallel composition to the transition
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{S}$, then there exists the
reordered execution
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{S}(\texttt{P${}^{\prime\prime}$}\mid\square)\stackrel{{\scriptstyle
m}}{{\rightarrow}}(\texttt{P${}^{\prime\prime\prime}$}\mid\square^{\prime})$
for some program P′′.

###### Proof.

Recall that skip steps do not change the program state in any way, and the
observation that any step from one side of a parallel composition cannot
‘cause’ skip steps on the other side of the same parallel.

Consider Part 1 of Lemma 3. The execution of two skip steps with one on each
side of a parallel means that neither skip step is the cause of the other.
With one of the steps requiring [P1a] and the other needing [P2a] to occur
within its inference tree, the definition of these rules shows the execution
of one cannot affect the execution of the other. This means the order of these
skip steps cannot change the final program state or structure, meaning the
reordering of these is permitted. The intermediate program P′′ is produced and
is as P′′′ but with the side of the parallel that contains
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{S_{1}}$ still in its initial form.

Consider Part 2 of Lemma 3. With each step being on opposite sides of a
parallel, the skip step $\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$ cannot
have been caused by the identifier step $\stackrel{{\scriptstyle
m}}{{\rightarrow}}$. This means that the skip step must have been caused by an
identifier step $\stackrel{{\scriptstyle k}}{{\rightarrow}}$ such that $k<m$.
As in Part 1, it is therefore guaranteed that both steps were available prior
to the execution of either. The rules [P1a] and [P2a] show that the program
structure of one side of a parallel cannot be changed via the other side. With
the skip step having no effect on the program state, the identifier step
$\stackrel{{\scriptstyle m}}{{\rightarrow}}$ and the skip step
$\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}$ can therefore be reordered. The
intermediate program P′′ is as P′′′ but with the side containing the
identifier step $\stackrel{{\scriptstyle m}}{{\rightarrow}}$ still in its
original form. Both parts are valid meaning Lemma 3 holds, as required. ∎

######  Lemma 4.

(Equivalent uniform execution) Given an arbitrary standard forward or reverse
program execution, there exists an equivalent uniform execution that modifies
the program state equivalently. Let P be an arbitrary program and $\square$ be
the tuple $\\{\gamma,\sigma,\mu,\beta,\delta\\}$ of initial program state
environments.

  1. 1.

If
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip
I}\mid\square^{\prime})$ for some I and final program state
$\square^{\prime}$, then there exists an equivalent uniform execution
$(\texttt{P}\mid\square)\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}}\leavevmode\nobreak\
(\texttt{skip I${}^{\prime}$}\mid\square^{\prime\prime})$ for I′ and program
state $\square^{\prime\prime}$ such that I′ = I and $\square^{\prime\prime}$ =
$\square^{\prime}$.

  2. 2.

If
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}^{*}(\texttt{skip
I}\mid\square^{\prime})$ for some I and final program state
$\square^{\prime}$, then there exists an equivalent uniform execution
$(\texttt{P}\mid\square)\leavevmode\nobreak\
\prescript{}{U}{\stackrel{{\scriptstyle\circ}}{{\rightsquigarrow}}^{*}}\leavevmode\nobreak\
(\texttt{skip I${}^{\prime}$}\mid\square^{\prime\prime})$ for I′ and program
state $\square^{\prime\prime}$ such that I′ = I and $\square^{\prime\prime}$ =
$\square^{\prime}$.

###### Proof.

A proof of Lemma 4 is by induction on the length of the execution using Lemma
3. All executions are assumed to be of complete programs. We consider each of
the two possible cases of execution, beginning with the special case of those
that start with any number of skip steps. Such a complete execution, written
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}^{*}(\texttt{P${}^{\prime}$}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip
I}\mid\square^{\prime})$, exists such that
$(\texttt{P}\mid\square)\stackrel{{\scriptstyle}}{{\rightarrow}}_{s}^{*}(\texttt{P${}^{\prime}$}\mid\square)$
contains all possible skip steps and that
$(\texttt{P${}^{\prime}$}\mid\square)\stackrel{{\scriptstyle\circ}}{{\rightarrow}}^{*}(\texttt{skip
I}\mid\square^{\prime})$ therefore begins with an identifier step. Since this