1

# Correctness of Speculative Optimizations
with Dynamic Deoptimization

Olivier Flückiger  Northeastern UniversityUSA ,  Gabriel Scherer  Northeastern
UniversityUSA INRIAFrance ,  Ming-Ho Yee  ,  Aviral Goel  ,  Amal Ahmed
Northeastern UniversityUSA and  Jan Vitek  Northeastern UniversityUSA
CVUTCzech Republic

(2018)

###### Abstract.

High-performance dynamic language implementations make heavy use of
speculative optimizations to achieve speeds close to statically compiled
languages. These optimizations are typically performed by a just-in-time
compiler that generates code under a set of assumptions about the state of the
program and its environment. In certain cases, a program may execute code
compiled under assumptions that are no longer valid. The implementation must
then deoptimize the program on-the-fly; this entails finding semantically
equivalent code that does not rely on invalid assumptions, translating program
state to that expected by the target code, and transferring control. This
paper looks at the interaction between optimization and deoptimization, and
shows that reasoning about speculation is surprisingly easy when assumptions
are made explicit in the program representation. This insight is demonstrated
on a compiler intermediate representation, named sourir, modeled after the
high-level representation for a dynamic language. Traditional compiler
optimizations such as constant folding, unreachable code elimination, and
function inlining are shown to be correct in the presence of assumptions.
Furthermore, the paper establishes the correctness of compiler transformations
specific to deoptimization: namely unrestricted deoptimization, predicate
hoisting, and assume composition.

Speculative optimization, dynamic deoptimization, on-stack-replacement

††price: ††doi: 10.1145/3158137††journalyear: 2018††copyright:
rightsretained††journal: PACMPL††journalyear: 2018††journalvolume:
2††journalnumber: POPL††article: 49††publicationmonth: 1††doi:
10.1145/3158137††ccs: Software and its engineering Just-in-time compilers

##  1\. Introduction

Dynamic languages pose unique challenges to compiler writers. With features
such as dynamic binding, runtime code generation, and generalized reflection,
languages such as Java, C#, Python, JavaScript, R, or Lisp force implementers
to postpone code generation until the last possible instant. The intuition
being that just-in-time (JIT) compilation can leverage information about the
program state and its environment, _e.g._ , the value of program inputs or
which libraries were loaded, to generate efficient code and potentially update
code on-the-fly.

Many dynamic language compilers support some form of _speculative_
optimization to avoid generating code for unlikely control-flow paths. In a
dynamic language prevalent polymorphism causes even the simplest code to have
non-trivial control flow. Consider the JavaScript snippet in Figure 1 (example
from Bebenita et al. (2010)). Without optimization one iteration of the loop
executes 210 instructions; all arithmetic operations are dispatched and their
results boxed. If the compiler is allowed to make

for | (i=0; i ¡ a.length-1; i++) {
---|---
|  var t=a[i];
| a[i]=a[i+1];
| a[i+1]=t;
}
Figure 1. JavaScript rotate function.

the assumption it is operating on integers, the body of the loop shrinks down
to 13 instructions. As another example, most Java implementations assume that
non-final methods are not overridden. Speculating on this fact allows
compilers to avoid emitting dispatch code (Ishizaki et al., 2000). Newly
loaded classes are monitored, and any time a method is overridden, the virtual
machine invalidates code that contains devirtualized calls to that method. The
validity of speculations is expressed as a predicate on the program state. If
some program action, like loading a new class, falsifies that predicate, the
generated code must be discarded. To undo an assumption, an implementation
must ensure that functions compiled under that assumption are retired. This
entails replacing affected code with a version that does not depend on the
invalid predicate and, if a function currently being executed is found to
contain invalid code, that function needs to be replaced on-the-fly. In such a
case, it is necessary to transfer control to a different version of the
function, and in the process, it may be necessary to materialize portions of
the state that were optimized away and perform other recovery actions. In
particular, if the invalid function was inlined into another function, it is
necessary to synthesize a new stack frame for the caller. This is referred to
as _deoptimization_ , or _on-stack-replacement_ , and is found in most
industrial-strength compilers.

Speculative optimization gives rise to a large and multi-dimensional design
space that lies mostly unexplored. First, compiler writers must decide how to
obtain information about program state. This can be done ahead-of-time by
profiling, just-in-time by sampling or instrumenting code. Next, they must
select what facts to record. This can range from information about the
program, its class hierarchy, which packages were loaded, to information about
the value of a particular mutable location in the heap. Finally, they must
decide how to efficiently monitor the validity of speculations. While some
points in this space have been explored empirically, existing systems have
done it in an _ad hoc_ manner that is often both language- and implementation-
specific, and thus difficult to apply broadly.

This paper has a focused goal. We aim to demystify the interaction between
compiler transformations and deoptimization. When are two versions compiled
under different assumptions equivalent? How should traditional optimizations
be adapted when operating on code containing deoptimization points? In what
ways does deoptimization inhibit optimizations? In this work we give compiler
writers the formal tools they need to reason about speculative optimizations.
To do this in a way that is independent of the specific language being
targeted and of implementation details relative to a particular compiler
infrastructure, we have designed a high-level compiler intermediate
representation (IR), named sourir, that is adequate for many dynamic languages
without being tied to any one in particular.

Sourir is inspired by our work on RIR, an IR for the R language. A sourir
program is made up of functions, and each function can have multiple versions.
We equip the IR with a single instruction, named assume, specific to
speculative optimization. This instruction has the role of describing what
assumptions are being used to perform speculative optimization and what
information must be preserved for deoptimization. It tests if those
assumptions hold, and in case they do not, transfers control to another, less
optimized version of the code. Reifying assumptions in the IR makes the
interaction with compiler transformations explicit and simplifies reasoning.
The assume instruction is more than a branch: when deoptimizing it replaces
the current stack frame with a stack frame that has the variables and values
expected by the target version, and, in case the function was inlined, it
synthesizes missing stack frames. Furthermore, unlike a branch, its
deoptimization target is not followed by the compiler during analysis and
optimization. The code executed in case of deoptimization is invisible to the
optimizer. This simplifies optimizations and reduces compile time as

$\\\ {\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{rot}$}(\,\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{native}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{call}}~{}\mathsf{type}\nobreak=\nobreak\mathsf{typeof}(\mathsf{a})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{assume}}~{}\mathsf{type}=\mathsf{NumArray}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{rot}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{base}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{t}$}}~{}[{\,\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{assume}}~{}\mathsf{t}\neq\mathsf{HL}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{rot}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{base}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{s}$}}~{}[{\mathsf{i}=\mathsf{i},\mathsf{j}=\mathsf{i}+1\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.45003pt}]\nobreak\leftarrow\nobreak\mathsf{a}[{\mathsf{i}+1}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.45003pt}]\nobreak\leftarrow\nobreak\mathsf{t}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{t}$}}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{base}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}&\textsf{{call}}~{}\mathsf{j}\nobreak=\nobreak\mathsf{add}(\mathsf{i},1)\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{s}$}}&\textsf{{call}}~{}\mathsf{t1}\nobreak=\nobreak\mathsf{get}(\mathsf{a},\mathsf{i})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{call}}~{}\mathsf{t2}\nobreak=\nobreak\mathsf{get}(\mathsf{a},\mathsf{j})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{call}}~{}\mathsf{t3}\nobreak=\nobreak\mathsf{store}(\mathsf{a},\mathsf{i},\mathsf{t2})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{call}}~{}\mathsf{t4}\nobreak=\nobreak\mathsf{store}(\mathsf{a},\mathsf{j},\mathsf{t1})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{t}$}}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}\\\
}}}}}}}}}}}}}}}}}}}}}$

Figure 2. Compiled function from Figure 1.

analysis remains local to the version being optimized and the deoptimization
metadata is considered to be a stand-in for the target version.

As an example consider the function from Figure 1. A possible translation to
sourir is shown in Figure 2 (less relevant code elided).
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{base}$}}$ contains the original
version. Helper functions  $\mathsf{get}$ and  $\mathsf{store}$ implement
JavaScript (JS) array semantics, and the function  $\mathsf{add}$ implement JS
addition. Version $\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{native}$}}$
contains only primitive sourir instructions. This version is optimized under
the assumption that the variable $\mathsf{a}$ is an array of primitive
numbers, which is represented by the first assume instruction. Further, JS
arrays can be sparse and contain holes, in which case access might need to be
delegated to a getter function. For this example $\mathsf{HL}$ denotes such a
hole. The second assume instruction reifies the compiler’s speculation that
the array has no holes, by asserting the predicate
$\mathsf{t}\neq\mathsf{HL}$. It also contains the associated deoptimization
metadata. In case the predicate does not hold, we deoptimize to a related
position in the base version by recreating the variables in the target scope.
As can be seen in the second assume, local variables are mapped as
$[\mathsf{i}=\mathsf{i},\mathsf{j}=\mathsf{i}+1]$; the current value of
$\mathsf{i}$ is carried over into the target frame’s $\mathsf{i}$, whereas
variable $\mathsf{j}$ has to be recomputed.

We prove the correctness of a selection of traditional compiler optimizations
in the presence of speculation; these are constant propagation, unreachable
code elimination, and function inlining. The main challenge for correctness is
that the transformations operate on one version in isolation and therefore
only see a subset of all possible control flows. We show how to split the work
to prove correctness between the pass that establishes a version-to-version
correspondence and the actual optimizations. Furthermore, we introduce and
prove the correctness of three optimizations specific to speculation, namely
unrestricted deoptimization, predicate hoisting, and assume composition.

Our work makes several simplifying assumptions. We use the same IR for
optimized and unoptimized code. We ignore the issue of generation of versions:
we study optimizations operating on a program at a certain point in time, on a
set of versions created before that time. We do not model the low-level
details of code generation. Correctness of runtime code generation and code
modification within a JIT compiler has been addressed by Myreen (2010). Sourir
is not designed for implementation, but to give a reasoning model for existing
JIT implementations. We do not intend to implement a new JIT engine. Instead,
we evaluated our work by discussing it with JIT implementers; the V8 team
(Chromium, 2017) confirmed that intuitions and correctness arguments could be
ported from sourir to their setting.

##  2\. Related Work

The SELF virtual machine pioneered dynamic deoptimization (Hölzle et al.,
1992). The SELF compiler implemented many optimizations, one of which was
aggressive inlining, yet the language designers wanted to give end users the
illusion that they were debugging source code. They achieved this by replacing
optimized code and the corresponding stack frames with non-optimized code and
matching stack frames. When deoptimizing code that had been inlined, the SELF
compiler synthesized stack frames. The HotSpot compiler followed from the work
on SELF by introducing the idea of speculative optimizations (Paleczny et al.,
2001). HotSpot supported very specific assumptions related to the structure of
the class hierarchy and instrumented the class loader to trigger invalidation.
When an invalidation occurred affected functions were rolled forward to a safe
point and control was transferred from native code to the interpreter. The
Jikes RVM adopted these ideas to avoid compiling uncommon code paths (Fink and
Qian, 2003).

One drawback of the early work was that deoptimization points were barriers
around which optimizations were not allowed. Odaira and Hiraki (2005) were the
first to investigate exception reordering by hoisting guards. They remarked
that checking assumptions early might improve code. In Soman and Krintz (2006)
the optimizer is allowed to update the deoptimization metadata. In particular
they support eliding duplicate variables in the mapping and lazily
reconstructing values when transferring control. This unlocks further
optimizations, which were blocked in previous work. The paper also introduces
the idea of being able to transfer control at any point. We support both the
update of metadata and unconstrained deoptimization.

Modern virtual machines have all incorporated some degree of speculation and
support for deoptimization. These include implementations of Java (HotSpot,
Jikes RVM), JavaScript (WebKit Core, Chromium V8, Truffle/JS, Firefox), Ruby
(Truffle/Ruby), and R (FastR), among others. Anecdotal evidence suggests that
the representation adopted in this work is representative of the instructions
found in the IR of production VMs: the TurboFan IR from V8 (Chromium, 2017)
represents assume with three distinct nodes. First a _checkpoint_ , holding
the deoptimization target, marks a stable point, to where execution can be
rolled back. In sourir this corresponds to the original location of an assume.
A _framestate_ node records the layout of, and changes to, the local frame,
roughly the varmap in sourir. Assumption predicates are guarded by conditional
deoptimization nodes, such as _deoptimizeIf_. Graal (Duboscq et al., 2013)
also has an explicit representation for assumptions and associated metadata as
_guard_ and _framestate_ nodes in their high-level IR. In both cases guards
are associated with the closest dominating checkpoint.

Lowering deoptimization metadata is described in Schneider and Bolz (2012);
Duboscq et al. (2014). A detailed empirical evaluation of deoptimization
appears in Zheng et al. (2017). The implementation of control-flow transfer is
not modeled here as it is not relevant to our results. For one particular
implementation, we refer readers to D’Elia and Demetrescu (2016) which builds
on LLVM. Alternatively, Wang et al. (2015) propose an IR that supports
restricted primitives for hot-patching code in a JIT.

There is a rich literature on formalizing compiler optimizations. The CompCert
project (Leroy and Blazy, 2008) for example implements many optimizations, and
contains detailed proof arguments for a data-flow optimization used for
constant folding that is similar to ours. In fact, sourir is close to
CompCert’s RTL language without versions or assumptions. There are
formalizations for tracing compilers (Guo and Palsberg, 2011; Dissegna et al.,
2014), but we are unaware of any other formalization effort for speculative
optimizations in general. Béra et al. (2016) present a verifier for a
bytecode-to-bytecode optimizer. By symbolically executing optimized and
unoptimized code, they verify that the deoptimization metadata produced by
their optimizer correctly maps the symbolic values of the former to the latter
at all deoptimization points.

##  3\. Sourir: Speculative Compilation Under Assumptions

This section introduces our IR and its design principles. We first present the
structure of programs and the assume instruction. Then, Section 3.2 and
following explain how sourir maintains multiple equivalent versions of the
same function, each with a different set of assumptions. This enables the
speculative optimizations presented in Section 4. All concepts introduced in
this section are formalized in Section 5.

###  3.1. Sourir in a Nutshell

${\small\begin{array}[]{lll}&&\textsf{{var}}~{}\mathsf{n}\nobreak=\nobreak\textsf{{nil}}\\\
&&\textsf{{read}}\,\mathsf{n}\\\
&&\textsf{{array}}~{}\mathsf{t}[{\mathsf{n}\kern 0.53998pt}]\\\
&&\textsf{{var}}~{}\mathsf{k}\nobreak=\nobreak 0\\\
&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}&\textsf{{branch}}~{}\mathsf{k}<\mathsf{n}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{3}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\mathsf{t}[{\mathsf{k}\kern
0.45003pt}]\nobreak\leftarrow\nobreak\mathsf{k}\\\
&&\mathsf{k}\nobreak\leftarrow\nobreak\mathsf{k}+1\\\
&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{3}$}}&\textsf{{drop}}\,\mathsf{k}\\\
&&\textsf{{stop}}\\\ \end{array}}$

Figure 3. Example sourir code.

Sourir is an untyped language with lexically scoped mutable variables and
first-class functions. As an example the function in Figure 3 queries a number
$\mathsf{n}$ from the user and initializes an array with values from 0 to n-1.
By design, sourir is a cross between a compiler representation and a high-
level language. We have equipped it with sufficient expressive power so that
it is possible to write interesting programs in a style reminiscent of dynamic
languages.111An implementation of sourir and the optimizations presented here
is available at https://github.com/reactorlabs/sourir. The only features that
are critical to our result are _versions_ and _assumptions_. Versions are the
counterpart of dynamically generated code fragments. Assumptions, represented
by the assume instruction, support dynamic deoptimization of speculatively
compiled code. The syntax of sourir instructions is shown in Figure 4.

Sourir supports defining a local variable, removing a variable from scope,
variable assignment, creating arrays, array assignment, (unstructured) control
flow, input and output, function calls and returns, assumptions, and
terminating execution. Control-flow instructions take explicit labels, which
are compiler-generated symbols but we sometimes give them meaningful names for
clarity of exposition. Literals are integers, booleans, and nil. Together with
variables and function references, they form simple expressions. Finally, an
expression is either a simple expression or an operation: array access, array
length, or primitive operation (arithmetic, comparison, and logic operation).
Expressions are not nested—this is common in intermediate representations such
as A-normal form (Sabry and Felleisen, 1992). We do allow bounded nesting in
instructions for brevity.

$\displaystyle\begin{tabular}[]{@{}l@{}l@{\ \ }c@{\ \ }l@{}l@{}l@{\ \
}lll@{}}$\mathit{i}$&&$::=$&&&\lx@intercol\text{instructions}\hfil\lx@intercol\\\
&&$|$&$\textsf{{var}}~{}\mathit{x}\nobreak=\nobreak\mathit{e}$&$$&$$&$\text{variable
declaration}$\\\ &&$|$&$\textsf{{drop}}\,\mathit{x}$&$$&$$&$\text{drop a
variable from scope}$\\\
&&$|$&$\mathit{x}\nobreak\leftarrow\nobreak\mathit{e}$&$$&$$&$\text{assignment}$\\\
&&$|$&$\textsf{{array}}~{}\mathit{x}[{\mathit{e}\kern
0.53998pt}]$&$$&$$&$\text{array allocation}$\\\
&&$|$&$\textsf{{array}}~{}\mathit{x}\nobreak=\nobreak[{e^{*}\kern
0.72002pt}]$&$$&$$&$\text{array creation}$\\\
&&$|$&$\mathit{x}[{\mathit{e_{{\mathrm{1}}}}\kern
0.45003pt}]\nobreak\leftarrow\nobreak\mathit{e_{{\mathrm{2}}}}$&$$&$$&$\text{array
assignment}$\\\
&&$|$&$\textsf{{branch}}~{}\mathit{e}~{}L_{{\mathrm{1}}}~{}L_{{\mathrm{2}}}$&$$&$$&$\text{conditional
branch}$\\\ &&$|$&$\textsf{{goto}}\,L$&$$&$$&$\text{unconditional branch}$\\\
&&$|$&$\textsf{{print}}\,\mathit{e}$&$$&$$&$\text{print}$\\\
&&$|$&$\textsf{{read}}\,\mathit{x}$&$$&$$&$\text{read}$\\\
&&$|$&$\textsf{{call}}~{}\mathit{x}\nobreak=\nobreak\mathit{e}(e^{*})$&$$&$$&$\text{function
call}$\\\ &&$|$&$\textsf{{return}}\,\mathit{e}$&$$&$$&$\text{return}$\\\
&&$|$&$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$&$$&$$&$\text{assume
instruction}$\\\ &&$|$&$\textsf{{stop}}$&$$&$$&$\text{terminate
execution}${}\\\\[14.22636pt] \end{tabular}\begin{tabular}[]{@{}l@{}l@{\ \
}c@{\ \ }l@{}l@{}l@{\ \
}lll@{}}$\mathit{e}$&&$::=$&&&\lx@intercol\text{expression}\hfil\lx@intercol\\\
&&$|$&$\mathit{se}$&$$&$$&$\text{simple expression}$\\\
&&$|$&$\mathit{x}[\mathit{se}\kern 0.67497pt]$&$$&$$&$\text{array access}$\\\
&&$|$&$\textsf{length}(\mathit{se})$&$$&$$&$\text{array length}$\\\
&&$|$&$primop\,(se^{*})$&$$&$$&$\text{primitive operation}${}\\\\[14.22636pt]
$\mathit{se}$&&$::=$&&&\lx@intercol\text{simple
expressions}\hfil\lx@intercol\\\
&&$|$&$\mathit{lit}$&$$&$$&$\text{literals}$\\\
&&$|$&${F}$&$$&$$&$\text{function reference}$\\\
&&$|$&$\mathit{x}$&$$&$$&$\text{variables}${}\\\\[14.22636pt]
$\mathit{lit}$&&$::=$&&&\lx@intercol\text{literals}\hfil\lx@intercol\\\
&&$|$&$\dots,-1,0,1,\dots$&$$&$$&$\text{numbers}$\\\ &&$|$&$\textsf{{nil}
}~{}|~{}\textsf{{true} }~{}|~{}\textsf{{false}
}$&$$&$$&$\text{others}${}\\\\[14.22636pt] \end{tabular}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\begin{matrix}[l]\xi&::=&\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}~{}\mathit{VA}&\emph{target
and varmap}\\\
\tilde{\xi}&::=&\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}~{}\mathit{x}~{}\mathit{VA}&\emph{extra
continuation}\\\
\mathit{VA}&::=&[\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}]&\emph{varmap}\\\
\end{matrix}$

Figure 4. The syntax of sourir.

A program $\mathit{P}$ is a set of function declarations. The body of a
function is a list of versions indexed by a version label, where each version
is an instruction sequence. The first instruction sequence in the list (the
_active version_) is executed when the function is called. $\mathit{F}$ ranges
over function names, $\mathit{V}$ over version labels, and $\mathit{L}$ over
instruction labels. An absolute reference to an instruction is thus a triple
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$. Every instruction is
labeled, but for brevity we omit unused labels.

Versions model the speculative optimizations performed by the compiler. The
only instruction that explicitly references versions is assume. It has the
form $\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$ with
a list of predicates $(e^{*})$ and deoptimization metadata $\xi$ and
$\tilde{\xi}^{*}$. When executed, assume evaluates its predicates; if they
hold execution skips to the next instruction. Otherwise, deoptimization occurs
according to the metadata. The format of $\xi$ is
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}~{}[{\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}\kern
0.33005pt}]$, which contains a target
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$ and a varmap
$[\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}]$.
To deoptimize, a fresh environment for the target is created according to the
varmap. Each expression $e_{i}$ is evaluated in the old environment and bound
to $x_{i}$ in the new environment. The environment specified by $\xi$ replaces
the current one. Deoptimization might also need to create additional
continuations, if assume occurs in an inlined function. In this case multiple
$\tilde{\xi}$ of the form
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}~{}\mathit{x}~{}[{\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}\kern
0.33005pt}]$ can be appended. Each one synthesizes a continuation with an
environment constructed according to the varmap, a return target
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$, and the name
$\mathit{x}$ to hold the returned result—this situation and inlining are
discussed in Section 4.3. The purpose of deoptimization metadata is twofold.
First, it provides the necessary information for jumping to the target
version. Second, its presence in the instruction stream allows the optimizer
to keep the mapping between different versions up-to-date.

#### Example

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=32,\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,\mathsf{l}*32\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>32\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,\mathsf{l}*\mathsf{el}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}&\textsf{{return}}\,0\\\
\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}}}}}}}}$

Figure 5. Speculation on $\mathsf{x}$.

Consider the function  $\mathsf{size}$ in Figure 5 which computes the size of
a vector $\mathsf{x}$. In version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$, $\mathsf{x}$ is either
nil or an array with its length stored at index $0$. The optimized version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}$ expects that the input
is never nil. Classical compiler optimizations can leverage this fact:
unreachable code removal prunes the unused branch. Constant propagation
replaces the use of $\mathsf{el}$ with its value and updates the varmap so
that it restores the deleted variable upon deoptimization to the base version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$.

###  3.2. Deoptimization Invariants

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{show}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{print}}\,42\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{w}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{print}}\,\mathsf{x}\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}&\textsf{{print}}\,\mathsf{x}\\\
\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}}}}}$

Figure 6. The version $\mathsf{w}$ violates the deoptimization invariant.

A version is the unit of optimization and deoptimization. Thus we expect that
each function will have one original version and possibly many optimized
versions. Versions are constructed such that they preserve two crucial
invariants: (1) _version equivalence_ and (2) _assumption transparency_. By
the first invariant all versions of a function are observationally equivalent.
The second invariant ensures that even if the assumption predicates _do_ hold,
deoptimizing to the target should be correct. Thus one could execute an
optimized version and its base in lockstep; at every assume the varmap
provides a complete mapping from the new version to the base. This simulation
relation between versions is our correctness argument. The transparency
invariant allows us to add assumption predicates without fear of altering
program semantics. Consider a function  $\mathsf{show}$ in Figure 6 which
prints its argument $\mathsf{x}$. Version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}$ respects both
invariants: any value for $\mathsf{x}$ will result in the same behavior as the
base version and deoptimizing is always possible. On the other hand,
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{w}$}}$, which is equivalent
because it will never deoptimize, violates the second invariant: if it were to
deoptimize, the value of $\mathsf{x}$ would be set to $42$, which is almost
always incorrect. We present a formal treatment of the invariants and the
correctness proofs in Section 5.4 and following.

###  3.3. Creating Fresh Versions

We expect that versions are chained. A compiler will create a new version, say
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}$, from an existing version
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}$ by copying all
instructions from the original version and chaining their

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{fun}$}(\,\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{0}$}}&\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{fun}$}.\kern-0.5pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{0}$}}~{}[{\,\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>1\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{print}}\,\mathsf{x}+2\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>1\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{fun}$}.\kern-0.5pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{g}=\mathsf{x},\mathsf{h}=\mathsf{x}+1\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{print}}\,\mathsf{x}+2\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>1\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{print}}\,\mathsf{h}+1\\\
\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}}}}}}}}}}}$

Figure 7. Chained assume instructions: Version 1 was created from 0, then
optimized. Version 2 is a fresh copy of 1.

deoptimization targets. The latter is done by updating the target and varmap
of assume instructions such that all targets refer to
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}$ at the same label as the
current instruction. As the new version starts out as a copy, the varmap is
the identity function. For instance, if the target contains the variables
$\mathsf{x}$ and $\mathsf{y}$, then the varmap is
$[\mathsf{x}=\mathsf{x},\mathsf{z}=\mathsf{z}]$. Additional assume
instructions can be added; assume instructions that bear no predicates (_i.e._
, the predicate list is either empty or just tautologies) can be removed while
preserving equivalence. As an example in Figure 7, the new version
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}$ is a copy of
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}$; the instruction at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{0}$}}$ was added, the
instruction at $\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$ was
updated, and the one at $\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$
was removed.

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{dup}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>32\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=\mathsf{el},\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,\mathsf{l}*\mathsf{el}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}&\textsf{{return}}\,0\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}\dots{}\\\
\end{array}\\\ \end{array}}}}}}}}}$

Figure 8. A fresh copy of the base version of size.

Updating assume instructions is not required for correctness. But the idea
with a new version is that it captures a set of assumptions that can be undone
independently from the previously existing assumptions. Thus, we want to be
able to undo one version at a time. In an implementation, versions might, for
example, correspond to optimization tiers.222A common strategy for VMs is to
have different kind of optimizing compilers with different compilation speed
versus code quality trade-offs. The more a code fragment is executed, the more
powerful optimizations will be applied to it. This approach can lead to a
cascade of deoptimizations if an inherited assumption fails; we discuss this
in Section 4.6. In the following sections we use the base version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$ of Figure 5 as our
running example. As a first step, we generate the new version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{dup}$}}$ with two fresh assume
instructions shown in Figure 8. Initially the predicates are true and the
assume instructions never fire. Version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$ stays unchanged.

###  3.4. Injecting Assumptions

We advocate an approach where the compiler first injects assumption
predicates, and then uses them in optimizations. In contrast, earlier work
would apply an unsound optimization and then recover by adding a guard (see,
for example, Duboscq et al. (2013)). While the end result is the same, the
different perspective helps with reasoning about correctness. Assumptions are
boolean predicates, similar to user-provided assertions. For example, to
speculate on a branch target, the assumption is the branch condition or its
negation. It is therefore correct for the compiler to expect that the
predicate holds immediately following an assume. Injecting predicates is done
after establishing the correspondence between two versions with assume
instructions, as presented above. Inserting a fresh assume in a function is
difficult in general, as one must determine where to transfer control to or
how to reconstruct the target environment. On the other hand, it is always
correct to add a predicate to an existing assume. Thanks to the assumption
transparency invariant it is safe to deoptimize more often to the target. For
instance, in
$\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}},\mathsf{x}>10~{}\mathbf{else}~{}\dots$
the predicate $\mathsf{x}\neq\textsf{{nil}}$ was narrowed down to
$\mathsf{x}>10$.

##  4\. Optimization with Assumptions

In the previous section we introduced our approach for establishing a fresh
version of a function that lends itself to speculative optimizations. Next, we
introduce classical compiler optimizations that are exemplary of our approach.
Then we give additional transformations for the assume in Section 4.4 and
following, and conclude with a case study in Section 4.7. All transformations
introduced in this section are proved correct in Section 6.

###  4.1. Constant Propagation

Consider a simple constant propagation pass that finds constant variables and
then updates all uses. This pass maintains a map from variable names to
constant expressions or _unknown_. The map is computed for every position in
the instruction stream using a data-flow analysis. Following the approach by
Kildall (1973), the analysis has an update function to add and remove
constants to the map. For example analyzing
$\textsf{{var}}~{}\mathsf{x}\nobreak=\nobreak 2$, or
$\mathsf{x}\nobreak\leftarrow\nobreak 2$ adds the mapping
$\mathsf{x}\rightarrow 2$. The instruction
$\textsf{{var}}~{}\mathsf{y}\nobreak=\nobreak\mathsf{x}+1$ adds
$\mathsf{y}\rightarrow 3$ to the previous map. Finally,
$\textsf{{drop}}\,\mathsf{x}$ removes a mapping. Control-flow merges rely on a
join function for intersecting two maps; mappings which agree are preserved,
while others are set to _unknown_. In a second step, expressions that can be
evaluated to values are replaced and unused variables are removed. No
additional care needs to be taken to make this pass correct in the presence of
assumptions. This is because in sourir, the expressions needed to reconstruct
environments appear in the varmap of the assume and are thus visible to the
constant propagation pass. Additionally, the pass can update them, for
example, in
$\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\mathsf{F}.\kern-0.5pt\mathsf{V}.\kern-0.5pt\mathsf{L}~{}[{\mathsf{x}=\mathsf{y}+\mathsf{z}\kern
0.33005pt}]$, the variables $\mathsf{y}$ and $\mathsf{z}$ are treated the same
as in
$\textsf{{call}}~{}\mathsf{h}\nobreak=\nobreak{\scalebox{0.97}{$\mathsf{foo}$}}(\mathsf{y}+\mathsf{z})$.
They can be replaced and will not artificially keep constant variables alive.

Constant propagation can become speculative. After the instruction
$\textsf{{assume}}~{}\mathsf{x}=0~{}\mathbf{else}~{}\dots$, the variable
$\mathsf{x}$ is 0. Therefore, $\mathsf{x}\leftarrow 0$ is added to the state
map. This is the only extension required for speculative constant propagation.
As an example, in the case where we speculate on a nil check $\\\
{\small\begin{array}[]{lll}&&\dots\\\
&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=\mathsf{el},\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
&&\textsf{{branch}}~{}\mathsf{x}=\textsf{{nil}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{3}$}}\\\
&&\dots\\\ \end{array}}\\\ $ the map is
$\mathsf{x}\rightarrow\neg\textsf{{nil}}$ after
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$. Evaluating the branch
condition under this context yields $\neg\textsf{{nil}}==\textsf{{nil}}$, and
a further optimization opportunity presents itself.

###  4.2. Unreachable Code Elimination

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{pruned}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>32\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=\mathsf{el},\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,\mathsf{l}*\mathsf{el}\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}\dots{}\\\
\end{array}\\\ \end{array}}}}}}}$

Figure 9. A speculation that the argument is not nil eliminated one of the
former branches.

As shown above, an assumption coupled with constant folding leads to branches
becoming deterministic. Unreachable code elimination benefits from that. We
consider a two step algorithm: the first pass replaces
$\textsf{{branch}}~{}\mathit{e}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$
with $\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$ if
$e$ is a tautology and with
$\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$ if it
is a contradiction. The second pass removes unreachable instructions. In our
running example from Figure 8, we add the predicate
$\mathsf{x}\neq\textsf{{nil}}$ to the empty assume at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$. Constant propagation
shows that the branch always goes to
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{3}$}}$, and unreachable code
elimination removes the dead statement at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}$ and branch. This creates
the version shown in Figure 9. Additionally, constant propagation can replace
$\mathsf{el}$ by $32$. By also replacing its mention in the varmap of the
assume at $\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$, $\mathsf{el}$
becomes unused and can be removed from the optimized version. This yields
version $\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}$ in Figure 5 at
the top.

###  4.3. Function Inlining

Function inlining is our most involved optimization, since assume instructions
inherited from the inlinee need to remain correct. The inlining itself is
standard. Name mangling is used to separate the caller and callee
environments. As an example Figure 10 shows the inlining of  $\mathsf{size}$
into a function $\mathsf{main}$. Naïvely inlining without updating the
metadata of the assume at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$ will result in an
incorrect deoptimization, as execution would transfer to
$\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$
with no way to return to the $\mathsf{main}$ function. Also, $\mathsf{main}$’s
part of the environment is discarded in the transfer and permanently lost. The
solution is to synthesize a new stack frame. As shown in the figure, the
assume at in the optimized $\mathsf{main}$ is thus extended with
$\mathsf{main}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}~{}\mathsf{s}~{}[{\mathsf{pl}=\mathsf{pl},\mathsf{vec}=\mathsf{vec}\kern
0.33005pt}]$.

${\small\begin{array}[]{l}\mathsf{main}(\,\kern 0.35994pt)\\\
\begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{inl}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{array}}~{}\mathsf{pl}\nobreak=\nobreak[{1,2,3,4\kern
0.72002pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{array}}~{}\mathsf{vec}\nobreak=\nobreak[{\textsf{length}(\mathsf{pl}\kern
0.35994pt),\mathsf{pl}\kern 0.72002pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\begin{matrix}[l]\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}}~{}\mathbf{else}&\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=32,\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
&\mathsf{main}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}~{}\mathsf{s}~{}[{\mathsf{pl}=\mathsf{pl},\mathsf{vec}=\mathsf{vec}\kern
0.29704pt}]\end{matrix}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{drop}}\,\mathsf{l}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{drop}}\,\mathsf{x}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}&\textsf{{print}}\,\mathsf{s}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{array}}~{}\mathsf{pl}\nobreak=\nobreak[{1,2,3,4\kern
0.72002pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{array}}~{}\mathsf{vec}\nobreak=\nobreak[{\textsf{length}(\mathsf{pl}\kern
0.35994pt),\mathsf{pl}\kern 0.72002pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{call}}~{}\mathsf{s}\nobreak=\nobreak{\scalebox{0.97}{$\mathsf{size}$}}(\mathsf{vec})\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}&\textsf{{print}}\,\mathsf{s}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \end{array}\\\
\,\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern 0.35994pt)\\\
\begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}&\textsf{{assume}}~{}\mathsf{x}\neq\textsf{{nil}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=32,\mathsf{x}=\mathsf{x}\kern
0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\phantom{\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}}&\textsf{{return}}\,\mathsf{l}*32\\\
\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}\dots{}\\\
\end{array}\\\ \end{array}}}}}}}}}}}}}}}}}}}}}}$

Figure 10. An inlining of size into a main.

This creates an additional stack frame that returns to the base version of
$\mathsf{main}$, and stores the result in $\mathsf{s}$ with the entire caller
portion of the environment reconstructed. It is always possible to compute the
continuation, since the original call site must have a label and the scope at
this label is known. Overall, after deoptimization, it appears as if version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$ of $\mathsf{main}$ had
called version $\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$ of
$\mathsf{size}$ . Note, it would erroneous to create a continuation that
returns to the optimized version of the caller
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{inl}$}}$. If deoptimization
from the inlined code occurs, it is precisely because some of its assumptions
are invalid. Multiple continuations can be appended for further levels of
inlining. The inlining needs to be applied bottom up: for the next level of
inlining, _e.g._ , to inline
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{inl}$}}$ into an outer caller,
renamings must also be applied to the expressions in the extra continuations,
since they refer to local variables in
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{inl}$}}$.

###  4.4. Unrestricted Deoptimization

The assume instructions are expensive: they create dependencies on live
variables and are barriers for moving instructions. Hoisting a side-effecting
instruction over an assume is invalid, because if we deoptimize the effect
happens twice. Removing a local variable is also not possible if its value is
needed to reconstruct the target environment. Thus it makes sense to insert as
few assume instructions as possible. On the other hand it is desirable to be
able to “deoptimize everywhere”—checking assumptions in the basic block in
which they are used can avoid unnecessary deoptimization—so there is a tension
between speculation and optimization. Reaching an assume marks a stable state
in the execution of the program that we can fall back to, similar to a
transaction. Implementations, like (Duboscq et al., 2013), separate
deoptimization points and the associated guards into two separate
instructions, to be able to deoptimize more freely. As long as the effects of
instructions performed since the last deoptimization point are not observable,
it is valid to throw away intermediate results and resume control from there.
Effectively, in sourir this corresponds to moving an assume instruction
forward in the instruction stream, while keeping its deoptimization target
fixed.

An assume can be moved over another instruction if that instruction:

  1. (1)

has no side-effects and is not a call instruction,

  2. (2)

does not interfere with the varmap or predicates, and

  3. (3)

has the assume as its only predecessor instruction.

The first condition prevents side-effects from happening twice. The second
condition can be enabled by copying the affected variables at the original
assume instruction location (_i.e._ , taking a snapshot of the required part
of the environment).333In an SSA based IR this step is not necessary for SSA
variables, since the captured ones are guaranteed to stay unchanged. The last
condition prevents capturing traces incoming from other basic blocks where (1)
and (2) do not hold for all intermediate instructions since the original
location. This is not the weakest condition, but a reasonable, sufficient one.
Let us consider a modified version of our running example in Figure 11 on the
left. Again, we have an assume before the branch, but would like to place a
guard inside one of the branches.

$\begin{array}[]{ll}{\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{any}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>32\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,\mathsf{x}*\mathsf{el}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}\dots{}\\\
\end{array}\\\
\end{array}}&{\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{size}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{any}$}}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>32\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>0.29704pt}]\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&&\textsf{{return}}\,1*\mathsf{el}\\\
\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}\dots{}\\\
\end{array}\\\ \end{array}}\end{array}}}}}}}}}}}}}}$ Figure 11. Moving an
assume forward in the instruction stream.

There is an interfering instruction at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}$ that modifies
$\mathsf{x}$. By creating a temporary variable to hold the value of
$\mathsf{x}$ at the original assume location, it is possible to resolve the
interference. Now the assume can move inside the branch and a predicate can be
added on the updated $\mathsf{x}$ (see right side of the figure). Note that
the target is unchanged. This approach allows for the (logical) separation
between the deoptimization point and the position of assumption predicates. In
the transformed example a stable deoptimization point is established at the
beginning of the function by storing the value of $\mathsf{x}$, but then the
assumption is checked only in one branch. The intermediate states are
ephemeral and can be safely discarded when deoptimizing. For example the
variable $\mathsf{el}$ is not mentioned in the varmap here, it is not captured
by the assume. Instead it is recomputed by the original code at the
deoptimization target
$\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$.
To be able to deoptimize from any position it is sufficient to have an assume
after every side-effecting instruction, call, and control-flow merge.

###  4.5. Predicate Hoisting

Moving an assume backwards in the code would require replaying the moved-over
instructions in the case of deoptimization. Hoisting
$\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{size}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}~{}[{\mathsf{el}=\mathsf{el},\dots\kern
0.33005pt}]$ above $\textsf{{var}}~{}\mathsf{el}\nobreak=\nobreak 32$ is
allowed if the varmap is changed to $[\mathsf{el}=32,\dots]$ to compensate for
the lost definition. However this approach is tricky and does not work for
instructions with multiple predecessors as it could lead to conflicting
compensation code. But a simple alternative to hoisting assume is to hoist a
_predicate_ from one assume to a previous one. To understand why, let us
decompose the approach into two steps. Given an assume at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$ that dominates a second
one at $\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$, we copy a
predicate from the latter to the former. This is valid since the assumption
transparency invariant allows strengthening predicates. A data-flow analysis
can determine if the copied predicate from
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$ is available at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{2}$}}$, in which case it can be
removed from the original instruction. In our running example, version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{pruned}$}}$ in Figure 9 has two
assume instructions and one predicate. It is trivial to hoist
$\mathsf{x}\neq\textsf{{nil}}$, since there are no interfering instructions.
This allows us to remove the assume with the larger scope. More interestingly,
in the case of a loop-invariant assumption, predicates can be hoisted out of
the loop.

###  4.6. Assume Composition

As we have argued in Section 3.3, it is beneficial to undo as few assumptions
as possible. On the other hand, deoptimizing an assumption added in an early
version cascades through all the later versions. To be able to remove chained
assume instructions, we show that assumptions are _composable_. If an assume
in version $\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{3}$}}$ transfers
control to a target
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}.\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{a}$}}$,
that is itself an assumption with
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}.\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}$
as target, then we can combine the metadata to take both steps at once. By the
assumption transparency invariant, the pre- and post-deoptimization states are
equivalent: even if the assumptions are not the same, it is correct to
conservatively trigger the second deoptimization. For example, an instruction
$\textsf{{assume}}~{}\mathit{e}~{}\mathbf{else}~{}\mathsf{F}.\kern-0.5pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{a}$}}~{}[{\mathsf{x}=1\kern
0.33005pt}]$ that jumps to
$\textsf{{assume}}~{}\mathit{e^{\prime}}~{}\mathbf{else}~{}\mathsf{F}.\kern-0.5pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}[{\mathsf{y}=\mathsf{x}\kern
0.33005pt}]$ can be combined as
$\textsf{{assume}}~{}\mathit{e},\mathit{e^{\prime}}~{}\mathbf{else}~{}\mathsf{F}.\kern-0.5pt\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}~{}[{\mathsf{y}=1\kern
0.33005pt}]$. This new unified assume skips the intermediate version
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}$ and goes to
$\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{0}$}}$ directly. This could be
an interesting approach for multi-tier JITs: after the system stabilizes,
intermediate versions are rarely used and may be discarded.

###  4.7. Case Study

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{div}$}(\mathsf{tagx},\mathsf{x},\mathsf{tagy},\mathsf{y}\kern 0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip 7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{base}$}}\\\ \begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}&\textsf{{return}}\,\mathsf{y}/\mathsf{x}\\\ \hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}}}}}$ |  ${\small\begin{array}[]{lll}&&\textsf{{assume}}~{}\mathsf{tagx}=\mathsf{NUM},\mathsf{tagy}=\mathsf{NUM}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{div}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}~{}[{\dots\kern 0.29704pt}]\\\ &&\textsf{{branch}}~{}\mathsf{x}=0~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{error}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}\\\ &\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}&\textsf{{return}}\,\mathsf{y}/\mathsf{x}\\\ &&\dots\\\ \end{array}}$
---|---
(a) | (b)
${\small\begin{array}[]{lll}&&\textsf{{assume}}~{}\mathsf{tagx}=\mathsf{NUM},\mathsf{x}\neq 0~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{div}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}~{}[{\dots\kern 0.29704pt}]\\\ &&\textsf{{branch}}~{}\mathsf{tagy}\neq\mathsf{NUM}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{slow}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}\\\ &\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}&\textsf{{return}}\,\mathsf{y}/\mathsf{x}\\\ &&\dots\\\ \end{array}}$ |  ${\small\begin{array}[]{lll}&\phantom{\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{4}$}}}&\textsf{{assume}}~{}\mathsf{tagx}=\mathsf{NUM},\mathsf{tagy}=\mathsf{NUM},\mathsf{x}\neq 0~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{div}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{b}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}~{}[{\dots\kern 0.29704pt}]\\\ &&\textsf{{return}}\,\mathsf{y}/\mathsf{x}\\\ \end{array}}$
(c) | (d)

Figure 12. Case study.

We conclude with an example. In dynamic languages code is often dispatched on
runtime types. If types were known, code could be specialized, resulting in
faster code with fewer checks and branches. Consider Figure 12(a) which
implements a generic binary division function that expects two values and
their type tags. No static information is available; the arguments could be
any type. Therefore, multiple checks are needed before the division; for
example the slow branch will require even more checks on the exact value of
the type tag. Suppose there is profiling information that indicates numbers
can be expected. The function is specialized by speculatively pruning the
branches as shown in Figure 12(b). In certain cases, sourir’s transformations
can make it appear as though checks have been reordered. Consider a variation
of the previous example, that speculates on $\mathsf{x}$, but not $\mathsf{y}$
as shown in Figure 12(c). In this version, both checks on $\mathsf{x}$ are
performed first and then the ones on $\mathsf{y}$, whereas in the unoptimized
version they are interleaved. By ruling out an exception early, it is possible
to perform the checks in a more efficient order. The fully speculated on
version contains only the integer division and the required assumptions
(Figure 12(d)). This version has no more branches and is a candidate for
inlining.

##  5\. Speculative Compilation Formalized

A sourir program contains several functions, each of which can have multiple
versions. This high-level structure is described in Figure 13. The first
version is considered the currently active version and will be executed by a
call instruction. Each version consists of a stream of labeled instructions.
We use an indentation-based syntax that directly reflects this structure and
omit unreferenced instruction labels.

$\begin{array}[]{lrll}P&::=&\boxed{{\small\begin{array}[]{l}\mathit{F}(x^{*}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip 7.11317pt\mathit{V}\\\
\begin{array}[]{l!{\,\color{gray}\vrule}lll}\hfil\lx@intercol\,\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>\end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}&\text{indentation-
based syntax}\end{array}}$

$\begin{array}[]{lrll}\mathit{P}&::=&\mathit{F}(x^{*}):\mathit{D_{F}},...&\text{a
program is a list of named functions}\\\
\mathit{D_{F}}&::=&\mathit{V}:\mathit{I},...&\text{a function definition is a
list of versioned instruction streams}\\\
\mathit{I}&::=&\mathit{L}:\mathit{i},...&\text{an instruction stream with
labeled instructions}\\\ \end{array}$

Figure 13. Program syntax.

Besides grammatical and scoping validity, we impose the following well-
formedness requirements to ease analysis and reasoning. The last instruction
of each version of the $\mathsf{main}$ function is stop. Two variable
declarations for the same name cannot occur in the same instruction stream.
This simplifies reasoning by letting us use variable names to unambiguously
track information depending on the declaration site. Different versions have
separate scopes and can have names in common. If a function reference
${\mathit{F}}$ is used, that function $\mathit{F}$ must exist. Source and
target of control-flow transitions must have the same set of declared
variables. This eases determining the environment at any point. To jump to a
label $\mathit{L}$, all variables not in scope at $\mathit{L}$ must be dropped
($\textsf{{drop}}\,\mathsf{x}$).

###  5.1. Operational Semantics: Expressions

Figure 14 gives the semantics of expressions. Evaluation $\mathit{e}$ returns
a value $\mathit{v}$, which may be a literal $\mathit{lit}$, a function, or an
address $a$. Arrays are represented by addresses into heap $\mathit{M}$. The
heap is a map from addresses to blocks of values
$[\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{v_{\mathit{n}}}]$. An environment
$\mathit{E}$ is a mapping from variables to values. Evaluation is defined by a
relation $\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}$: under
$\mathit{M}$ and environment $\mathit{E}$, $\mathit{e}$ evaluates to
$\mathit{v}$. This definition in turn relies on a relation
$\mathit{E}~{}\mathit{se}\rightharpoonup\mathit{v}$ defining evaluation of
simple expressions $\mathit{se}$, which does not access arrays. The notation
$[\\![primop]\\!]$ to denote, for each primitive operation $primop$, a partial
function on values. Arithmetic operators and arithmetic comparison operators
are only defined when their arguments are numbers. Equality and inequality are
defined for all values. The relation
$\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}$, when seen as a
function from $\mathit{M}$, $\mathit{E}$, $\mathit{e}$ to $\mathit{v}$, is
partial: it is not defined on all inputs. For example, there is no
$\mathit{v}$ such that the relation
$\mathit{M}~{}\mathit{E}~{}\mathsf{x}[{\mathit{se}}]\rightarrow\mathit{v}$
holds if $\mathit{E}(\mathsf{x})$ is not an address $a$, if $a$ is not bound
in $\mathit{M}$, if $\mathit{se}$ does not reduce to a number $n$, or if $n$
is out of bounds.

$\displaystyle\begin{tabular}[]{@{}l@{}l@{\ \ }c@{\ \ }l@{}l@{}l@{\ \
}lll@{}}$\mathit{v}$&&$::=$&&&\lx@intercol\text{values}\hfil\lx@intercol\\\
&&$|$&$\mathit{lit}$&$$&$$&$$\\\ &&$|$&$F$&$$&$$&$$\\\
&&$|$&$\mathit{a}$&$$&$$&$${}\\\\[14.22636pt] \end{tabular}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt\begin{array}[]{ll}addr::=a&\text{addresses}\\\
\mathit{M}::=(\mathit{a}\,\rightarrow[\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{v_{\mathit{n}}}])^{*}&\text{heap}\\\
\mathit{E}::=(\mathsf{x}\rightarrow\mathit{v})^{*}&\text{environment}\\\
\end{array}$

$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{35.12196pt}[]{l}\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{E}~{}\mathit{lit}\rightharpoonup\mathit{lit}$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{34.69698pt}[]{l}\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{E}~{}{F}\rightharpoonup
F$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{40.74701pt}[]{l}\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{E}~{}\mathit{x}\rightharpoonup\mathit{E}(\mathit{x})$}}\end{array}$

$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{37.16893pt}[]{l}$\mathit{E}~{}\mathit{se}\rightharpoonup\mathit{v}~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{M}~{}\mathit{E}~{}\mathit{se}\rightarrow\mathit{v}$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{178.57277pt}[]{l}$\mathit{E}~{}\mathit{se_{{\mathrm{1}}}}\rightharpoonup\mathit{v_{{\mathrm{1}}}}\quad..\quad\mathit{E}~{}\mathit{se_{\mathit{n}}}\rightharpoonup\mathit{v_{\mathit{n}}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{M}~{}\mathit{E}~{}primop(\mathit{se_{{\mathrm{1}}}},\,..\,,\mathit{se_{\mathit{n}}})\rightarrow[\\![primop]\\!](\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{v_{\mathit{n}}})$}}\end{array}$

$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{114.23595pt}[]{l}$\mathit{E}~{}\mathit{se}\rightharpoonup\mathit{a}\quad\mathit{M}(\mathit{a})=[\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{v_{\mathit{n}}}]~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{M}~{}\mathit{E}~{}\textsf{length}(\mathit{se}\kern
0.25195pt)\rightarrow\mathit{n}$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{123.06404pt}[]{l}$\mathit{a}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{E}(\mathit{x})\quad\mathit{M}(\mathit{a})=[\mathit{v_{{\mathrm{0}}}},\,..\,,\mathit{v_{\mathit{m}}}]~{}~{}$\\\
$\mathit{E}~{}\mathit{se}\rightharpoonup\mathit{n}\quad
0\leq\mathit{n}\leq\mathit{m}~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{M}~{}\mathit{E}~{}\mathit{x}[{\mathit{se}}]\rightarrow\mathit{v_{\mathit{n}}}$}}\end{array}$

Figure 14. Evaluation
$\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}$ of expressions and
$\mathit{E}~{}\mathit{se}\rightharpoonup\mathit{v}$ of simple expressions.

###  5.2. Operational Semantics: Instructions and Programs

We define a small-step, labeled operational semantics with a notion of machine
state, or configuration, that represents the dynamic state of a program being
executed, and a transition relation between configurations. A configuration is
a six-component tuple
$\langle\mathit{P}\,\mathit{I}\,\mathit{L}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$
described in Figure 15. Continuations $\mathit{K}$ are tuples of the form
$\langle\mathit{I}~{}\mathit{L}~{}\mathit{x}~{}\mathit{E}\rangle$, storing the
information needed to correctly return to a caller function. On a call
$\textsf{{call}}~{}\mathsf{x}\nobreak=\nobreak\mathit{e}(\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{e_{\mathit{n}}})$,
the continuation pushed on the stack contains the current instruction stream
$\mathit{I}$ (to be restored on return), the label $\mathit{L}$ of the next
instruction after the call (the return label), the variable $\mathit{x}$ to
name the returned result, and environment $\mathit{E}$. For the details, see
the reduction rules for call and return in Figure 17.

$\displaystyle\begin{array}[]{ll}\begin{array}[]{c}\mathit{C}::=\langle\mathit{P}\,\mathit{I}\,\mathit{L}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\\\
\text{configuration}\end{array}&\left(\begin{array}[]{lrll}\mathit{P}&&&\text{program}\\\
\mathit{I}&&&\text{instructions}\\\ \mathit{L}&&&\text{next label}\\\
K^{*}&::=&(\mathit{K_{{\mathrm{1}}}},\,..\,,\mathit{K_{\mathit{n}}})&\text{call
stack}\\\ \mathit{M}&&&\text{heap}\\\ \mathit{E}&&&\text{environment}\\\
\end{array}\right.\\\ &\\\
\begin{array}[]{c}\mathit{K}::=\langle\mathit{I}~{}\mathit{L}~{}\mathit{x}~{}\mathit{E}\rangle\\\
\text{continuation}\end{array}&\left(\begin{array}[]{lrll}\mathit{I}&&&\text{code
of calling function}\\\ \mathit{L}&&&\text{return label}\\\
\mathit{x}&&&\text{return variable}\\\ \mathit{E}&&&\text{environment at call
site}\\\ \end{array}\right.\end{array}$ Figure 15. Abstract machine state.

$\mathit{A}$ $::=$ I/O action $|$ $\textsf{print}~{}\mathit{lit}$ $|$
$\textsf{read}~{}\mathit{lit}$ $|$ stop $\mathit{A}_{\tau}$ $::=$ $|$
$\mathit{A}$ $|$ $\tau$ silent label $\mathit{T}$ $::=$ action trace $|$
(empty trace) $|$ $\mathit{A}$ $|$ $\mathit{A}_{\tau}$ $|$
$\mathit{T}~{}\mathit{A}$ $|$ $\mathit{T}~{}\mathit{A}_{\tau}$

$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{25.97005pt}[]{l}\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{C}\overset{\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C}$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{79.1923pt}[]{l}$\mathit{C}\overset{\mathit{T}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime}}\quad\mathit{C^{\prime}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{C}\overset{\mathit{T}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime\prime}}$}}\end{array}$
$\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{79.50793pt}[]{l}$\mathit{C}\overset{\mathit{T}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime}}\quad\mathit{C^{\prime}}\overset{\mathit{A}}{\longrightarrow}\mathit{C^{\prime\prime}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.17pt}{$\mathit{C}\overset{\mathit{T}~{}\mathit{A}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime\prime}}$}}\end{array}$

Figure 16. Actions and traces.

The relation
$\mathit{C}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}}$
specifies that executing the next instruction may result in the configuration
$\mathit{C^{\prime}}$. The action $\mathit{A}_{\tau}$ indicates whether this
reduction is observable: it is either the silent action, written $\tau$, an
I/O action $\textsf{read}~{}\mathit{lit}$ or $\textsf{print}~{}\mathit{lit}$,
or stop. We write
$\mathit{C}\overset{\mathit{T}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime}}$
when there are zero or more steps from $\mathit{C}$ to $\mathit{C^{\prime}}$.
The trace $\mathit{T}$ is a list of non-silent actions in the order in which
they appeared. Actions are defined in Figure 16, and the full reduction
relation is given in Figure 17.

$\displaystyle{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{152.04411pt}[]{l}$\mathit{I}(L)=~{}\textsf{{var}}~{}\mathit{x}\nobreak=\nobreak\mathit{e}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}[\mathit{x}\leftarrow\mathit{v}]\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{151.59967pt}[]{l}$\mathit{I}(L)=~{}\textsf{{drop}}\,\mathit{x}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}\mathord{\setminus}\\{\mathit{x}\\}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{198.98743pt}[]{l}$\mathit{I}(L)=~{}\textsf{{array}}~{}\mathit{x}\nobreak=\nobreak[{\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{e_{\mathit{n}}}\kern
0.448pt}]\quad\mathit{M}~{}\mathit{E}~{}\mathit{e_{{\mathrm{1}}}}\rightarrow\mathit{v_{{\mathrm{1}}}}\quad..\quad\mathit{M}~{}\mathit{E}~{}\mathit{e_{\mathit{n}}}\rightarrow\mathit{v_{\mathit{n}}}~{}~{}$\\\
$\mathit{a}~{}\text{fresh}\quad\mathit{M^{\prime}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{M}[\mathit{a}\leftarrow[\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{v_{\mathit{n}}}]]~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M^{\prime}}\,\mathit{E}[\mathit{x}\leftarrow\scalebox{0.97}{$\mathsf{a}$}]\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{152.93387pt}[]{l}$\mathit{I}(L)=~{}\textsf{{array}}~{}\mathit{x}[{\mathit{e}\kern
0.33598pt}]\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow n~{}~{}$\\\
$\mathit{a}~{}\text{fresh}\quad\mathit{M^{\prime}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{M}[\mathit{a}\leftarrow[\textsf{{nil}}_{1},..,\textsf{{nil}}_{n}]]~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M^{\prime}}\,\mathit{E}[\mathit{x}\leftarrow\scalebox{0.97}{$\mathsf{a}$}]\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{152.04411pt}[]{l}$\mathit{I}(L)=~{}\mathit{x}\nobreak\leftarrow\nobreak\mathit{e}\quad\mathsf{x}\in
dom(\mathit{E})\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}[\mathit{x}\leftarrow\mathit{v}]\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{178.96967pt}[]{l}$\mathit{I}(L)=~{}\mathit{x}[{\mathit{e^{\prime}}\kern
0.28001pt}]\nobreak\leftarrow\nobreak\mathit{e}\quad\scalebox{0.97}{$\mathsf{a}$}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{E}(\mathit{x})\quad\mathit{M}~{}\mathit{E}~{}\mathit{e^{\prime}}\rightarrow\mathit{n}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}~{}~{}$\\\
$\mathit{M}(\mathit{a})=[\mathit{v_{{\mathrm{0}}}},\,..\,,\mathit{v_{\mathit{m}}}]\quad
0\leq\mathit{n}\leq\mathit{m}~{}~{}$\\\
$\mathit{M^{\prime}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{M}[\mathit{a}\leftarrow[\mathit{v_{{\mathrm{0}}}},\,..\,,\mathit{v_{\mathit{m}}}]\\{\mathit{v_{\mathit{n}}}/\mathit{v}\\}]~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M^{\prime}}\,\mathit{E}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{175.01088pt}[]{l}$\mathit{I}(L)=~{}\textsf{{read}}\,\mathit{x}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\textsf{read}~{}\mathit{lit}}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}[\mathit{x}\leftarrow\mathit{lit}]\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{152.78859pt}[]{l}$\mathit{I}(L)=~{}\textsf{{print}}\,\mathit{e}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{lit}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\textsf{print}~{}\mathit{lit}}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{131.83618pt}[]{l}$\mathit{I}(L)=~{}\textsf{{branch}}~{}\mathit{e}~{}L_{{\mathrm{1}}}~{}L_{{\mathrm{2}}}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\textsf{{true}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,L_{{\mathrm{1}}}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{132.96953pt}[]{l}$\mathit{I}(L)=~{}\textsf{{branch}}~{}\mathit{e}~{}L_{{\mathrm{1}}}~{}L_{{\mathrm{2}}}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\textsf{{false}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,L_{{\mathrm{2}}}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{115.94266pt}[]{l}$\mathit{I}(L)=~{}\textsf{{goto}}\,L^{\prime}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,L^{\prime}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{124.81349pt}[]{l}$\mathit{I}(L)=~{}\textsf{{stop}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\textsf{stop}}{\longrightarrow}\langle\mathit{P}\,\emptyset\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{177.06526pt}[]{l}$\mathit{I}(L)=~{}\textsf{{call}}~{}\mathit{x}\nobreak=\nobreak\mathit{e}(\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{e_{\mathit{n}}})~{}~{}$\\\
$\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow F~{}~{}$\\\
$\mathit{P}(F)=F(\mathit{x}_{{\mathrm{1}}},\,..\,,\mathit{x}_{\mathit{n}}):\mathit{D_{F}}\quad\mathit{I^{\prime}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(F,\mathsf{active})~{}~{}$\\\
$L^{\prime}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathsf{start}(\mathit{I^{\prime}})\quad\mathit{M}\,\mathit{E}\,[{\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}\kern
0.18481pt}]\rightsquigarrow\mathit{E^{\prime}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I^{\prime}}\,L^{\prime}\,(K^{*},\langle\mathit{I}~{}(L\kern-1.0pt+\kern-2.0pt1)~{}\mathit{x}~{}\mathit{E}\rangle)\;\mathit{M}\,\mathit{E^{\prime}}\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{185.20572pt}[]{l}$\mathit{I}(L)=~{}\textsf{{return}}\,\mathit{e}\quad\mathit{M}~{}\mathit{E}~{}\mathit{e}\rightarrow\mathit{v}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,(K^{*},\langle\mathit{I^{\prime}}~{}L^{\prime}~{}\mathit{x}~{}\mathit{E^{\prime}}\rangle)\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I^{\prime}}\,L^{\prime}\,K^{*}\;\mathit{M}\,\mathit{E^{\prime}}[\mathit{x}\leftarrow\mathit{v}]\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{164.90297pt}[]{l}$\mathit{I}(L)=~{}\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}\quad\forall\mathit{m},\mathit{M}~{}\mathit{E}~{}\mathit{e_{\mathit{m}}}\rightarrow\textsf{{true}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P}\,\mathit{I}\,(L\kern-1.0pt+\kern-2.0pt1)\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$}}\end{array}}\quad\quad{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{176.45854pt}[]{l}$\mathit{I}(L)=~{}\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}\quad\neg(\forall\mathit{m},\mathit{M}~{}\mathit{E}~{}\mathit{e_{\mathit{m}}}\rightarrow\textsf{{true}})~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\mathsf{deoptimize}(\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle,\xi,\tilde{\xi}^{*})$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{271.82571pt}[]{l}$\mathit{M}\,\mathit{E}\,\mathit{VA}\rightsquigarrow\mathit{E^{\prime}}\quad\mathit{I^{\prime}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(F^{\prime},V^{\prime})~{}~{}$\\\
$\begin{matrix}[l]\forall\mathit{q}&\in 1,..,\mathit{r},\\\
&\tilde{\xi}_{\mathit{q}}=F_{\mathit{q}}.\kern-0.5ptV_{\mathit{q}}.\kern-0.5ptL_{\mathit{q}}~{}\mathit{x}_{\mathit{q}}~{}\mathit{VA}_{\mathit{q}}\\\
&\mathit{M}\,\mathit{E}\,\mathit{VA}_{\mathit{q}}\rightsquigarrow\mathit{E_{\mathit{q}}}\quad\mathit{I_{\mathit{q}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(F_{\mathit{q}},V_{\mathit{q}})\quad\mathit{K_{\mathit{q}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\langle\mathit{I_{\mathit{q}}}~{}L_{\mathit{q}}~{}\mathit{x}_{\mathit{q}}~{}\mathit{E_{\mathit{q}}}\rangle\end{matrix}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\mathsf{deoptimize}(\langle\mathit{P}\,\mathit{I}\,L\,K^{*}\;\mathit{M}\,\mathit{E}\rangle,F^{\prime}.\kern-0.5ptV^{\prime}.\kern-0.5ptL^{\prime}~{}\mathit{VA},\tilde{\xi}_{{\mathrm{1}}},\,..\,,\tilde{\xi}_{\mathit{r}})\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\langle\mathit{P}\,\mathit{I^{\prime}}\,L^{\prime}\,(K^{*},\mathit{K_{{\mathrm{1}}}},\,..\,,\mathit{K_{\mathit{r}}})\;\mathit{M}\,\mathit{E^{\prime}}\rangle$}}\end{array}}\quad\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{127.24922pt}[]{l}$\mathit{M}~{}\mathit{E}~{}\mathit{e_{{\mathrm{1}}}}\rightarrow\mathit{v_{{\mathrm{1}}}}\quad..\quad\mathit{M}~{}\mathit{E}~{}\mathit{e_{\mathit{n}}}\rightarrow\mathit{v_{\mathit{n}}}~{}~{}$\\\
\end{tabular*}}{\raisebox{-1.92888pt}{$\mathit{M}\,\mathit{E}\,[{\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}\kern
0.18481pt}]\rightsquigarrow[\mathit{x}_{{\mathrm{1}}}\rightarrow\mathit{v_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}\rightarrow\mathit{v_{\mathit{n}}}]$}}\end{array}}\quad$
Figure 17. Reduction relation
$\mathit{C}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}}$ for sourir IR.

Most rules get the current instruction, $\mathit{I}(\mathit{L})$, perform an
operation, and advance to the next label, referred to by the shorthand
$(\mathit{L}\kern-1.0pt+\kern-2.0pt1)$. The $\textsf{read}~{}\mathit{lit}$ and
$\textsf{print}~{}\mathit{lit}$ actions represent observable I/O operations.
They are emitted by Read and Print in Figure 17. The action
$\textsf{read}~{}\mathit{lit}$ on the $\textsf{{read}}\,\mathit{x}$ transition
may be any literal value. This is the only reduction rule that is non-
deterministic. Note that the relation
$\mathit{C}\overset{\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime}}$,
containing only sequences of silent reductions, is deterministic. The stop
reduction emits the stop transition, and also produces a configuration with no
instructions, $\emptyset$. This is a technical device to ensure that the
resulting configuration is stuck. A program with a silent loop has a different
trace from a program that halts. Given a program $\mathit{P}$, let
$\mathsf{start}(\mathit{P})$ be its starting configuration, and
$\mathsf{reachable}(\mathit{P})$ be the set of configurations reachable from
it; they are all the states that may be encountered during a valid run of
$\mathit{P}$.

$\displaystyle{\begin{array}[b]{<EMAIL_ADDRESS>\frac{\begin{tabular*}{157.52133pt}[]{l}$\mathit{I}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(\mathsf{main},\mathsf{active})\quad
L\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathsf{start}(\mathit{I})~{}~{}$\\\
\end{tabular*}}{\raisebox{-2.41112pt}{$\mathsf{start}(\mathit{P})\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\langle\mathit{P}\,\mathit{I}\,L\,\emptyset\;\emptyset\,\emptyset\rangle$}}\end{array}}\quad\quad\mathsf{reachable}(\mathit{P})\
\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\
\\{\mathit{C}\mid\exists\mathit{T},\
\mathsf{start}(\mathit{P})\overset{\mathit{T}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C}\\}$

###  5.3. Equivalence of Configurations: Bisimulation

We use weak bisimulation to prove equivalence between configurations. The idea
is to define, for each program transformation, a correspondence relation $R$
between configurations over the source and transformed programs. We show that
related configurations have the same observable behavior, and reducing them
results in configurations that are themselves related. Two programs are
equivalent if their starting configurations are related.

###### Definition 5.1 (Weak Bisimulation).

Given programs $\mathit{P_{{\mathrm{1}}}}$ and $\mathit{P_{{\mathrm{2}}}}$ and
relation $R$ between the configurations of $\mathit{P_{{\mathrm{1}}}}$ and
$\mathit{P_{{\mathrm{2}}}}$, $R$ is a _weak simulation_ if for any related
states $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ and any
reduction
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
over $\mathit{P_{{\mathrm{1}}}}$, there exists a reduction
$\mathit{C_{{\mathrm{2}}}}\overset{~{}\mathit{A}_{\tau}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime}_{{\mathrm{2}}}}$
over $\mathit{P_{{\mathrm{2}}}}$ such that
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})$ are
themselves related by $R$. Reduction over $\mathit{P_{{\mathrm{2}}}}$ is
allowed to take zero or more steps, but not to change the trace. In other
words, the diagram on the left below can always be completed into the diagram
on the right.

${\mathit{C_{{\mathrm{1}}}}}$${\mathit{C^{\prime}_{{\mathrm{1}}}}}$${\mathit{C_{{\mathrm{2}}}}}$$\scriptstyle{R}$$\scriptstyle{A_{\tau}}$
${\mathit{C_{{\mathrm{1}}}}}$${\mathit{C^{\prime}_{{\mathrm{1}}}}}$${\mathit{C_{{\mathrm{2}}}}}$${\mathit{C^{\prime}_{{\mathrm{2}}}}}$$\scriptstyle{R}$$\scriptstyle{A_{\tau}}$$\scriptstyle{R}$∗$\scriptstyle{A_{\tau}}$

$R$ is a weak bisimulation if it is a weak simulation and the symmetric
relation $R^{-1}$ also is—a reduction from $\mathit{C_{{\mathrm{2}}}}$ can be
matched by $\mathit{C_{{\mathrm{1}}}}$. Finally, two configurations are
_weakly bisimilar_ if there exists a weak bisimulation $R$ that relates them.

In the remainder, the adjective weak is always implied. The following result
is standard, and essential to compose the correctness proof of subsequent
transformation passes.

###### Lemma 5.2 (Transitivity).

If $R_{12}$ is a weak bisimulation between $\mathit{P_{{\mathrm{1}}}}$ and
$\mathit{P_{{\mathrm{2}}}}$, and $R_{23}$ is a weak bisimulation between
$\mathit{P_{{\mathrm{2}}}}$ and $\mathit{P_{{\mathrm{3}}}}$, then the composed
relation
$R_{13}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}(R_{12};R_{23})$ is
a weak bisimulation between $\mathit{P_{{\mathrm{1}}}}$ and
$\mathit{P_{{\mathrm{3}}}}$.

###### Definition 5.3 (Version bisimilarity).

Let $\mathit{V_{{\mathrm{1}}}}$, $\mathit{V_{{\mathrm{2}}}}$ be two versions
of a function $\mathit{F}$ in $\mathit{P}$, and let
$\mathit{I_{{\mathrm{1}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(\mathit{F},\mathit{V_{{\mathrm{1}}}})$
and
$\mathit{I_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{P}(\mathit{F},\mathit{V_{{\mathrm{2}}}})$.
$\mathit{V_{{\mathrm{1}}}}$ and $\mathit{V_{{\mathrm{2}}}}$ are _(weakly)
bisimilar_ if
$\langle\mathit{P}\,\mathit{I_{{\mathrm{1}}}}\,\mathsf{start}(\mathit{I_{{\mathrm{1}}}})\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$
and
$\langle\mathit{P}\,\mathit{I_{{\mathrm{2}}}}\,\mathsf{start}(\mathit{I_{{\mathrm{2}}}})\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$
are weakly bisimilar for all $K^{*}$, $\mathit{M}$, $\mathit{E}$.

###### Definition 5.4 (Equivalence).

$\mathit{P_{{\mathrm{1}}}}$, $\mathit{P_{{\mathrm{2}}}}$ are _equivalent_ if
$\mathsf{start}(\mathit{P_{{\mathrm{1}}}})$,
$\mathsf{start}(\mathit{P_{{\mathrm{2}}}})$ are weakly bisimilar.

###  5.4. Deoptimization Invariants

We can now give a formal definition of the invariants from Section 3.2:
Version Equivalence holds if any pair of versions
$(\mathit{V_{{\mathrm{1}}}},\mathit{V_{{\mathrm{2}}}})$ of a function
$\mathit{F}$ are bisimilar; Assumption Transparency holds if for any
configuration $\mathit{C}$, at an
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$,
$\mathit{C}$, is bisimilar to
$\mathsf{deoptimize}(\mathit{C},\xi,\tilde{\xi}^{*})$, as defined in Figure
17, DeoptimizeConf.

###  5.5. Creating Fresh Versions and Injecting Assumptions

Configuration $\mathit{C}$ is _over_ location
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$ if it is
$\langle\mathit{P}\,\mathit{P}(\mathit{F},\mathit{V})\,\mathit{L}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$,
where $\mathit{P}(\mathit{F},\mathit{V})$ denotes the instructions at version
$\mathit{V}$ of $\mathit{F}$ in $\mathit{P}$. Let
$\mathit{C}[\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}\nobreak\leftarrow\nobreak\mathit{F^{\prime}}.\kern-0.5pt\mathit{V^{\prime}}.\kern-0.5pt\mathit{L^{\prime}}]$
be the configuration
$\langle\mathit{P}\,\mathit{P}(\mathit{F^{\prime}},\mathit{V^{\prime}})\,\mathit{L^{\prime}}\,K^{*}\;\mathit{M}\,\mathit{E}\rangle$.
More generally, $\mathit{C}[X\nobreak\leftarrow\nobreak Y]$ replaces various
components of $\mathit{C}$. For example,
$\mathit{C}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$
updates the program in $\mathit{C}$; if only the versions change between two
locations $\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$ and
$\mathit{F}.\kern-0.5pt\mathit{V^{\prime}}.\kern-0.5pt\mathit{L}$, write
$\mathit{C}[\mathit{V}\nobreak\leftarrow\nobreak\mathit{V^{\prime}}]$ instead
of repeating the locations, etc.

###### Theorem 5.5.

Creating a new copy of the currently active version of a function, possibly
adding new assume instructions, returns an equivalent program.

###### Proof.

Consider $\mathit{P_{{\mathrm{1}}}}$ with a function $\mathit{F}$ with active
version $\mathit{V_{{\mathrm{1}}}}$. Adding a version yields
$\mathit{P_{{\mathrm{2}}}}$ with new active version
$\mathit{V_{{\mathrm{2}}}}$ of $\mathit{F}$ such that

  * •

any label $\mathit{L}$ of $\mathit{V_{{\mathrm{1}}}}$ exists in
$\mathit{V_{{\mathrm{2}}}}$L: the instruction at $\mathit{L}$ in
$\mathit{V_{{\mathrm{1}}}}$ and $\mathit{V_{{\mathrm{2}}}}$ are identical
except for assume instructions updated so that
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$ in
$\mathit{V_{{\mathrm{1}}}}$ has a corresponding
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}~{}\mathsf{Id}$
in $\mathit{V_{{\mathrm{2}}}}$ where $\mathsf{Id}$ is the identity over the
environment at $\mathit{L}$.

  * •

$\mathit{V_{{\mathrm{2}}}}$ may contain extra empty assume instructions: for
any instruction $\mathit{i}$ at $\mathit{L}$ in $\mathit{V_{{\mathrm{1}}}}$,
$\mathit{V_{{\mathrm{2}}}}$ may contain an assume of the form
$\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}~{}\mathsf{Id}$,
where $\mathsf{Id}$ is the identity mapping over the environment at
$\mathit{L}$, followed by $\mathit{i}$ at a fresh label $\mathit{L^{\prime}}$.

Let us write $\mathit{I_{{\mathrm{1}}}}$ and $\mathit{I_{{\mathrm{2}}}}$ for
the instructions of $\mathit{V_{{\mathrm{1}}}}$ and
$\mathit{V_{{\mathrm{2}}}}$ respectively. Stack $K^{*}_{{\mathrm{2}}}$ is a
_replacement_ of $K^{*}_{{\mathrm{1}}}$ if it is obtained from
$K^{*}_{{\mathrm{1}}}$ by replacing continuations of the form
$\langle\mathit{I_{{\mathrm{1}}}}~{}\mathit{L}~{}\mathit{x}~{}\mathit{E}\rangle$
by
$\langle\mathit{I_{{\mathrm{2}}}}~{}\mathit{L}~{}\mathit{x}~{}\mathit{E}\rangle$.
Replacement is a device used in the proof and does not correspond to any of
the reduction rules. We define a relation $R$ as the smallest relation such
that :

  1. (1)

For any configuration $\mathit{C_{{\mathrm{1}}}}$ over
$\mathit{P_{{\mathrm{1}}}}$, $R$ relates $\mathit{C_{{\mathrm{1}}}}$ to
$\mathit{C_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$.

  2. (2)

For any configuration $\mathit{C_{{\mathrm{1}}}}$ over a
$\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}$ such
that $\mathit{L}$ in $\mathit{V_{{\mathrm{2}}}}$ is not an added assume, $R$
relates $\mathit{C_{{\mathrm{1}}}}$ to
$\mathit{C_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}][\mathit{V_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{2}}}}]$.

  3. (3)

For any configuration $\mathit{C_{{\mathrm{1}}}}$ over a
$\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}$ such
that at $\mathit{L}$ in $\mathit{V_{{\mathrm{2}}}}$ is a newly added assume
followed by label $\mathit{L^{\prime}}$, $R$ relates
$\mathit{C_{{\mathrm{1}}}}$ to both (a)
$\mathit{C_{{\mathrm{1}}}}[\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}\nobreak\leftarrow\nobreak\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{2}}}}.\kern-0.5pt\mathit{L}]$
and (b)
$\mathit{C_{{\mathrm{1}}}}[\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}\nobreak\leftarrow\nobreak\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{2}}}}.\kern-0.5pt\mathit{L^{\prime}}]$.

  4. (4)

For any related pair $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in
R$, where $K^{*}_{{\mathrm{1}}}$ is the call stack of
$\mathit{C_{{\mathrm{2}}}}$, for any replacement $K^{*}_{{\mathrm{2}}}$, the
pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}}[K^{*}_{{\mathrm{1}}}\nobreak\leftarrow\nobreak
K^{*}_{{\mathrm{2}}}])$ is in $R$.

The proof proceeds by showing that $R$ is a bisimulation. If a related pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ comes from the
cases (1), (2) or (3) of the definition of $R$, we say that it is a _base
pair_. A pair $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$ in case
(4) is defined from another pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$, such
that the call stack of $\mathit{C_{{\mathrm{2}}}}$ is a replacement of the
stack of $\mathit{C^{\prime}_{{\mathrm{2}}}}$. If
$(\mathit{C_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$ is a
base pair, we say that it is the base pair of
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$. Otherwise, we say
that the base pair of $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$
is the base pair of
$(\mathit{C_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})$.

#### Bisimulation proof: generalities

To prove that $R$ is a bisimulation, consider all related pairs
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ and show that a
reduction from $\mathit{C_{{\mathrm{1}}}}$ can be matched by
$\mathit{C_{{\mathrm{2}}}}$ and conversely. Without loss of generality, assume
that $\mathit{C_{{\mathrm{2}}}}$ is not a newly added assume instruction –
that the base pair of $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$
is not in the case (3,b) of the definition of $R$. Indeed, the proof of the
case (3,b) follows from proof of the case (3,a). In the case (3,b),
$\mathit{C_{{\mathrm{2}}}}$ is a newly added assume instruction
$\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\dots$ at $\mathit{L}$
followed by $\mathit{L^{\prime}}$. $\mathit{C_{{\mathrm{2}}}}$ can only reduce
silently into
$\mathit{C^{\prime}_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{C_{{\mathrm{2}}}}[\mathit{L}\nobreak\leftarrow\nobreak\mathit{L^{\prime}}]$,
which is related to $\mathit{C_{{\mathrm{1}}}}$ by the case (3,a). The empty
reduction sequence from $\mathit{C_{{\mathrm{1}}}}$ matches this reduction
from $\mathit{C_{{\mathrm{2}}}}$. Conversely, assume the result in the case
(3,a), then any reduction of $\mathit{C_{{\mathrm{1}}}}$ can be matched from
$\mathit{C^{\prime}_{{\mathrm{2}}}}$, and thus matched from
$\mathit{C_{{\mathrm{2}}}}$ by prepending the silent reduction
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
to the matching reduction sequence. Finally, if
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$ comes from case (4)
and has a base pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})$ from (3,b),
and $\mathit{C_{{\mathrm{2}}}}$ has label $\mathit{L}$ followed by
$\mathit{L^{\prime}}$, then the bisimulation property for
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ comes from the
one of
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}}[\mathit{L}\nobreak\leftarrow\nobreak\mathit{L^{\prime}}])\in
R$ by the same reasoning.

#### Bisimulation proof: easy cases

The easy cases of the proof are the reductions
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
where neither $\mathit{C_{{\mathrm{1}}}}$ nor
$\mathit{C^{\prime}_{{\mathrm{1}}}}$ are over $\mathit{V_{{\mathrm{1}}}}$, and
the reductions
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
where neither $\mathit{C_{{\mathrm{2}}}}$ nor
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ are over $\mathit{V_{{\mathrm{2}}}}$. For
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$,
define $\mathit{C^{\prime}_{{\mathrm{2}}}}$ as
$\mathit{C^{\prime}_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$,
and both
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
and
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$
hold. The
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
case is symmetric, defining $\mathit{C^{\prime}_{{\mathrm{1}}}}$ as
$\mathit{C^{\prime}_{{\mathrm{2}}}}[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]$.

#### Bisimulation proof: harder cases

The harder cases are split in two categories: version-change reductions
(deoptimizations, functions call and returns), and same-version reductions
within $\mathit{V_{{\mathrm{1}}}}$ in $\mathit{P_{{\mathrm{1}}}}$ or
$\mathit{V_{{\mathrm{2}}}}$ in $\mathit{P_{{\mathrm{2}}}}$. We consider same-
version reductions first. Without loss of generality, assume that the pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ is a base pair,
that is a pair related by the cases (2) or (3) of the definition of $R$, but
not (4) – the case that changes the call stack of the configuration. Indeed,
if pair $(\mathit{C_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$
comes from (4), the only difference between this pair and its base pair
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ is in the call
stack of $\mathit{C_{{\mathrm{2}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$.
This means that $\mathit{C_{{\mathrm{2}}}}$ and
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ have the exact same reduction behavior
for non-version-change reductions. As long as the proof that the related
configurations $\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$
match each other does not use version-change reductions (a property that holds
for the proofs of the non-version-change cases below), it also applies to
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$. For a
reduction
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
that is not a version-change reduction (deoptimization, call or return), prove
that it can be matched from $\mathit{C_{{\mathrm{1}}}}$ by reasoning on
whether $\mathit{C_{{\mathrm{2}}}}$ or $\mathit{C^{\prime}_{{\mathrm{2}}}}$
are assume instructions, coming from $\mathit{V_{{\mathrm{1}}}}$ or newly
added.

  * •

If none of them are assume instructions, then they are both in the case (2) of
the definition of $R$, they are equal to
$\mathit{C_{{\mathrm{1}}}}[\mathit{V_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{2}}}}]$
and
$\mathit{C^{\prime}_{{\mathrm{1}}}}[\mathit{V_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{2}}}}]$
respectively, so
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
and
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$
hold.

  * •

If $\mathit{C_{{\mathrm{2}}}}$ or $\mathit{C^{\prime}_{{\mathrm{2}}}}$ are
assume instructions coming from $\mathit{V_{{\mathrm{1}}}}$, the same
reasoning holds – the problematic case where the assume is
$\mathit{C_{{\mathrm{2}}}}$ and the guards do not pass is not considered here
as the reduction is not a deoptimization.

  * •

If $\mathit{C^{\prime}_{{\mathrm{2}}}}$ is a newly added assume in
$\mathit{V_{{\mathrm{2}}}}$ at $\mathit{L}$ followed by $\mathit{L^{\prime}}$,
$\mathit{C_{{\mathrm{2}}}}$ is an instruction of $\mathit{V_{{\mathrm{2}}}}$
copied from $\mathit{V_{{\mathrm{1}}}}$, so
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$ are in the case (2) of
the definition of $R$ and $\mathit{C_{{\mathrm{1}}}}$ is
$\mathit{C_{{\mathrm{1}}}}[\mathit{V_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{1}}}}]$.
The reduction from $\mathit{C_{{\mathrm{2}}}}$ corresponds to a reduction
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
in $\mathit{P_{{\mathrm{1}}}}$ with
$\mathit{C^{\prime}_{{\mathrm{1}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{C^{\prime}_{{\mathrm{2}}}}[\mathit{V_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{1}}}}]$,
and
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$
by the case (3,a) of the definition of $R$.

The reasoning for transitions
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
that have to be matched from $\mathit{C_{{\mathrm{2}}}}$ and are not version-
change transitions (deoptimization, function calls or return) is similar.
$\mathit{C_{{\mathrm{2}}}}$ cannot be a new assume, so we have
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$,
and either $\mathit{C^{\prime}_{{\mathrm{2}}}}$ is not a new assume and
matches $\mathit{C_{{\mathrm{1}}}}$ by case (2) of the definition of R, or it
is a new assume and it matches it by the case (3,a).

#### Bisimulation proof: final cases

The cases that remain are the hard cases of version-change reductions:
function call, return and deoptimization. If
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
is a deoptimization reduction, then $\mathit{C_{{\mathrm{1}}}}$ is over a
location
$\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}$ in
$\mathit{P_{{\mathrm{1}}}}$, and its instruction is
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$, and
$\mathit{C^{\prime}_{{\mathrm{1}}}}$ is
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{1}}}},\xi,\tilde{\xi}^{*})$.
$\mathit{C_{{\mathrm{2}}}}$ is over the copied instruction
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}~{}\mathsf{Id}$
and $\mathsf{Id}$ is the identity. $\mathit{C_{{\mathrm{2}}}}$ also
deoptimizes, given that the tests give the same results in the same
environment, so we have
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
for
$\mathit{C^{\prime}_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L_{{\mathrm{1}}}}~{}\mathsf{Id},\emptyset)$.
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ is over
$\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}$, that
is the same assume instruction as $\mathit{C_{{\mathrm{1}}}}$, so it also
deoptimizes, to
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathsf{deoptimize}(\mathit{C^{\prime}_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})$.
We show that $\mathit{C^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$ are related by $R$:

  * •

If $(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$ is a base
pair, then $\mathit{C_{{\mathrm{1}}}}$ is
$\mathit{C_{{\mathrm{2}}}}[\mathit{V_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{1}}}}]$.
In particular, the two configurations have the same environment, and
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ is identical to
$\mathit{C_{{\mathrm{2}}}}$ except it is over
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L_{{\mathrm{1}}}}$. It is
thus equal to $\mathit{C_{{\mathrm{1}}}}$. As a consequence,
$\mathit{C^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$, which are obtained from
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$ by the
same deoptimization reduction, are the same configurations, and related in
$R$.

  * •

If $\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$ are related by
the case (4) of the definition of $R$, the stack of
$\mathit{C_{{\mathrm{2}}}}$ is a replacement of the stack of
$\mathit{C_{{\mathrm{1}}}}$. The same reasoning as in the previous case shows
that configurations $\mathit{C^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$ are identical, except that the
stack of $\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$ is a replacement of the
stack of $\mathit{C^{\prime}_{{\mathrm{1}}}}$: they are related by the case
(4) of the definition of $R$.

Conversely, if
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
is a deoptimization instruction then, by the same reasoning as in the proof of
matching a deoptimization of $\mathit{C_{{\mathrm{1}}}}$,
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ is identical to
$\mathit{C_{{\mathrm{1}}}}$ (modulo replaced stacks). This means that the
empty reduction sequence from $\mathit{C_{{\mathrm{1}}}}$ matches the
reduction of $\mathit{C_{{\mathrm{2}}}}$.

If
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
is a function call transition,

$\langle\mathit{P_{{\mathrm{1}}}}\,\mathit{I_{{\mathrm{1}}}}\,\mathit{L}\,K^{*}_{{\mathrm{1}}}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P_{{\mathrm{1}}}}\,\mathit{I^{\prime}_{{\mathrm{1}}}}\,\mathit{L^{\prime}}\,(K^{*},\langle\mathit{I_{{\mathrm{1}}}}~{}(\mathit{L}\kern-1.0pt+\kern-2.0pt1)~{}\mathsf{x}~{}\mathit{E}\rangle)\;\mathit{M}\,\mathit{E^{\prime}}\rangle$

$\mathit{C_{{\mathrm{2}}}}$ is on the same call with the same arguments, so it
takes a transition
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
of the form

$\langle\mathit{P_{{\mathrm{2}}}}\,\mathit{I_{{\mathrm{2}}}}\,\mathit{L}\,K^{*}_{{\mathrm{2}}}\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P_{{\mathrm{2}}}}\,\mathit{I^{\prime}_{{\mathrm{2}}}}\,\mathit{L^{\prime}}\,(K^{*},\langle\mathit{I_{{\mathrm{2}}}}~{}(\mathit{L}\kern-1.0pt+\kern-2.0pt1)~{}\mathsf{x}~{}\mathit{E}\rangle)\;\mathit{M}\,\mathit{E^{\prime}}\rangle$

The stack of $\mathit{C^{\prime}_{{\mathrm{2}}}}$ is a replacement of the
stack of $\mathit{C^{\prime}_{{\mathrm{1}}}}$: assuming that
$K^{*}_{{\mathrm{2}}}$ is a replacement of $K^{*}_{{\mathrm{1}}}$, the
difference in the new continuation is precisely the definition of stack
replacement – note that it is precisely this reasoning step that required the
addition of case (4) in the definition of $R$. Also, the new instruction
streams $\mathit{I^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{I^{\prime}_{{\mathrm{2}}}}$ are either identical (if the function is
not $\mathit{F}$ itself) or equal to $\mathit{I_{{\mathrm{1}}}}$ and
$\mathit{I_{{\mathrm{2}}}}$ respectively, so we do have
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime}_{{\mathrm{2}}}})\in R$
as expected. The proof of the symmetric case, matching a function call from
$\mathit{C_{{\mathrm{2}}}}$, is identical.

If
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
is a function return transition

$\langle\mathit{P_{{\mathrm{1}}}}\,\mathit{I_{{\mathrm{1}}}}\,L\,(K^{*},\langle\mathit{I^{\prime}_{{\mathrm{1}}}}~{}L^{\prime}~{}\mathit{x}~{}\mathit{E^{\prime}}\rangle)\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P_{{\mathrm{1}}}}\,\mathit{I^{\prime}_{{\mathrm{1}}}}\,L^{\prime}\,K^{*}_{{\mathrm{1}}}\;\mathit{M}\,\mathit{E^{\prime}}[\mathit{x}\leftarrow\mathit{v}]\rangle$

then
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
is also a function return transition

$\langle\mathit{P_{{\mathrm{2}}}}\,\mathit{I_{{\mathrm{2}}}}\,L\,(K^{*},\langle\mathit{I^{\prime}_{{\mathrm{2}}}}~{}L^{\prime}~{}\mathit{x}~{}\mathit{E^{\prime}}\rangle)\;\mathit{M}\,\mathit{E}\rangle\overset{\tau}{\longrightarrow}\langle\mathit{P_{{\mathrm{2}}}}\,\mathit{I^{\prime}_{{\mathrm{2}}}}\,L^{\prime}\,K^{*}_{{\mathrm{2}}}\;\mathit{M}\,\mathit{E^{\prime}}[\mathit{x}\leftarrow\mathit{v}]\rangle$

We have to show that $\mathit{C^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ are related by $R$. The environments and
heaps of the two configurations are identical. We know that the stack of
$\mathit{C_{{\mathrm{2}}}}$ is a replacement of the stack of
$\mathit{C_{{\mathrm{1}}}}$, which means that $K^{*}_{{\mathrm{2}}}$ a
replacement of $K^{*}_{{\mathrm{1}}}$, and that either
$\mathit{I^{\prime}_{{\mathrm{1}}}}$ and $\mathit{I^{\prime}_{{\mathrm{2}}}}$
are identical or they are respectively equal to $\mathit{I_{{\mathrm{1}}}}$
and $\mathit{I_{{\mathrm{2}}}}$. In either case,
$\mathit{C^{\prime}_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$
are related by $R$. The proof of the symmetric case, matching a function
return from $\mathit{C_{{\mathrm{2}}}}$, is identical. We have established
that $R$ is a bisimulation.

Finally, remark that our choice of $R$ also proves that the new version
respects the assumption transparency invariant. A new assume at $\mathit{L}$
in $\mathit{V_{{\mathrm{2}}}}$ is of the form
$\textsf{{assume}}~{}\textsf{{true}}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}~{}\mathsf{Id}$,
with $\mathsf{Id}$ the identity environment. Any configuration $\mathit{C}$
over $\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{2}}}}.\kern-0.5pt\mathit{L}$
is related by $R^{-1}$ to
$\mathit{C}[\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{2}}}}.\kern-0.5pt\mathit{L}\nobreak\leftarrow\nobreak\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}]$,
which is equal to
$\mathsf{deoptimize}(\mathit{C},\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{1}}}}.\kern-0.5pt\mathit{L}~{}\mathsf{Id},\emptyset)$.
These two configurations are related by the bisimulation $R^{-1}$, so they are
bisimilar. ∎

###### Lemma 5.6.

Adding a new predicate $\mathit{e^{\prime}}$ to an existing assume instruction
$\textsf{{assume}}~{}e^{*}~{}\mathbf{else}~{}\xi~{}\tilde{\xi}^{*}$ of
$\mathit{P_{{\mathrm{1}}}}$ returns an equivalent program
$\mathit{P_{{\mathrm{2}}}}$.

###### Proof.

This is a consequence of the invariant of assumption transparency. Let
$R_{\mathit{P_{{\mathrm{1}}}}}$ be the bisimilarity relation for
configurations over $\mathit{P_{{\mathrm{1}}}}$, and
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$ be the location of
the modified assume. Let us define the relation $R$ between
$\mathit{P_{{\mathrm{1}}}}$ and $\mathit{P_{{\mathrm{2}}}}$ by

$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in
R\quad\iff\quad(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}}[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}])\in
R_{\mathit{P_{{\mathrm{1}}}}}$

We show that $R$ is a bisimulation. Consider
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})\in R$. If
$\mathit{C_{{\mathrm{2}}}}$ is not over
$\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$, the reductions of
$\mathit{C_{{\mathrm{2}}}}$ (in $\mathit{P_{{\mathrm{2}}}}$) and
$\mathit{C_{{\mathrm{2}}}}[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]$
(in $\mathit{P_{{\mathrm{1}}}}$) are identical, and the latter configuration
is, by assumption, bisimilar to $\mathit{C_{{\mathrm{1}}}}$, so it is
immediate that any reduction from $\mathit{C_{{\mathrm{1}}}}$ can be matched
by $\mathit{C_{{\mathrm{2}}}}$ and conversely. If $\mathit{C_{{\mathrm{2}}}}$
is over $\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}$, we can
compare its reduction behavior (in $\mathit{P_{{\mathrm{2}}}}$) with the one
of
$\mathit{C_{{\mathrm{2}}}}[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]$
(in $\mathit{P_{{\mathrm{1}}}}$). The first configuration deoptimizes when one
of the $e^{*},\mathit{e^{\prime}}$ is not true in the environment of
$\mathit{C_{{\mathrm{2}}}}$, while the second deoptimizes when one of the
$e^{*}$ is not true – in the same environment. If $\mathit{C_{{\mathrm{2}}}}$
gives the same boolean value to both series of test, then the two
configurations have the same reduction behavior, and
$(\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}})$ match each other by
the same reasoning as in the previous paragraph. The only interesting case is
the configurations $\mathit{C_{{\mathrm{2}}}}$ that pass all the tests in
$e^{*}$, but fail $\mathit{e^{\prime}}$. Let us show that, even in that case,
the reductions of $\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$
match each other. The following diagram will be useful to follow the proof
below: