the first instruction is exactly the same dispatch call, i.e.
$\mathsf{st}^{\prime}=\mathsf{st}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$.
The configuration $(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}$
could either step by Disp or err if
$\operatorname{{\mathcal{D}}}(\mathsf{M}^{\prime},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$
is undefined. Let us inspect the possibility of the latter. By HM,
$\mathsf{M}^{\prime}$ optimizes $\mathsf{M}$, so $\mathsf{M}^{\prime}$
contains the same original method $\mathsf{m}!{\overline{\mathsf{ty}_{o}}}$.
Thus, dispatch cannot fail due to the lack of applicable methods. As
$\mathsf{M}^{\prime}$ is well-formed, we also know that if there is a
specialized method instance, it is for the best original method and ambiguity
is not possible. Thus,
$\operatorname{{\mathcal{D}}}(\mathsf{M}^{\prime},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$
succeeds, and $\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}$ steps by Disp:

$(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathcal{D}}}~{}(\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}.$

There are two possibilities for $\overline{\mathsf{st}^{\prime}_{b}}$. (a) If
$\mathsf{M}^{\prime}$ does not contain a specialization, then
$\overline{\mathsf{st}^{\prime}_{b}}=\overline{\mathsf{st}_{b}}$. By
reflexivity of the optimization relation, we then have:

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \overline{\mathsf{st}_{b}}\
\triangleright\ \overline{\mathsf{st}_{b}}.$

(b) If $\mathsf{M}^{\prime}$ contains a specialized method instance
$\langle\mathsf{m}!{\overline{\mathsf{T}}}\,\overline{\mathsf{st}^{\prime}_{b}},\
\overline{\mathsf{ty}_{o}}\rangle$, then
$\overline{\mathsf{st}^{\prime}_{b}}\neq\epsilon$ by the assumption on
$\mathsf{M}^{\prime}$, and thus the desired relation is guaranteed by HM:

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \overline{\mathsf{st}_{b}}\
\triangleright\ \overline{\mathsf{st}^{\prime}_{b}}.$

    2. (2)

If $\textsc{HOpt}_{0}$ is built with OI-Direct, then $\mathsf{st}^{\prime}$ is
a direct call, i.e.
$\mathsf{st}^{\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}!{\overline{\mathsf{T}^{\prime}}}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{k}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$
where
$\overline{\mathsf{T}^{\prime}}=\overline{\mathsf{ty}}^{\mathsf{E}}[{\mathsf{\overline{\mathsf{k}}}}]$,
and method instance $\mathsf{m}!{\overline{\mathsf{T}^{\prime}}}$ is in
$\mathsf{M}^{\prime}$. Note that by HI and the soundness of type inference, we
know that
$\operatorname{\mathit{typeof}}(\mathsf{E}[{\mathsf{\overline{\mathsf{k}}}}])<:\operatorname{\mathit{typeof}}(\overline{\mathsf{ty}}^{\mathsf{E}}[{\mathsf{\overline{\mathsf{k}}}}])$,
i.e. $\overline{\mathsf{T}}<:\overline{\mathsf{T}^{\prime}}$. Since both are
concrete types, and concrete types do not have subtypes other than themselves,
it has to be the case that
$\overline{\mathsf{T}^{\prime}}=\overline{\mathsf{T}}$ and
$\mathsf{m}!{\overline{\mathsf{T}}^{\prime}}=\mathsf{m}!{\overline{\mathsf{T}}}$.
Thus, $\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}$ calls
$\mathsf{m}!{\overline{\mathsf{T}}}$ and steps by Direct:

$(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathcal{D}}}~{}(\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}.$

By OI-Direct, $\mathsf{m}!{\overline{\mathsf{T}}}\,$
$\overline{\mathsf{st}^{\prime}_{b}}$ specializes
$\mathsf{m}!{\overline{\mathsf{ty}_{o}}}$. Since $\mathsf{M}^{\prime}$ does
not have stubs, we have by HM:

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \overline{\mathsf{st}_{b}}\
\triangleright\ \overline{\mathsf{st}^{\prime}_{b}}.$

Because the new top frames $\mathsf{E}^{\prime}\ \overline{\mathsf{st}_{b}}$
and $\mathsf{E}^{\prime}\ \overline{\mathsf{st}^{\prime}_{b}}$ are related in
both cases, and the rest of the stacks did not change, we get that the entire
stacks $\mathsf{F}_{2},\mathsf{F}^{\prime}_{2}$ are related:

$(\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}})\cdot(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ (\mathsf{E}^{\prime}\
\overline{\mathsf{st}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F}\ \triangleright\
(\mathsf{E}^{\prime}\ \overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime}.$

And thus we get the desired:

$\mathsf{F}_{2},\,\mathsf{M}\ \triangleright\
\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime}\ <:\ \Delta^{\prime}_{1}.$

  * •

Case Direct. This case is not possible because $\mathsf{F}$ is obtained by
running methods of $\mathsf{M}$, and $\mathsf{M}$ consists of only original
methods, which do not contain direct calls.

(2) Backward direction. This direction is similar to the forward direction.
Because the structure of $\mathsf{F}^{\prime}_{1}$ matches the structure of
$\mathsf{F}_{1}$, we can always find the corresponding step for
$\mathsf{F}_{1},\,\mathsf{M}$. The most interesting cases of

$\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathcal{D}}}~{}\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime}$

are Disp and Direct, and some details on these are provided below.
In both cases, we have $\mathsf{F}_{1}=(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F}$,
$\mathsf{F}^{\prime}_{1}=(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime}$,
and
$\Delta_{1}=(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta$,
and we know that configurations step by making a function call. As a result,
we get:

$(\mathsf{E}^{\prime}\ \overline{\mathsf{st}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F},\,\mathsf{M}\
\triangleright\ (\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}\
<:\
(\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}})\cdot(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta,$

where
$\overline{\mathsf{ty}^{\prime}}=\operatorname{\mathcal{I}}(\mathsf{M},\overline{\mathsf{T}},\overline{\mathsf{st}_{b}})$
just like in the forward direction.

  * •

Case Disp. Here,
$\mathsf{st}^{\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$,
and the configuration steps as:

$(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathcal{D}}}~{}(\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime},$

where $\mathsf{E}^{\prime}=\mathsf{E}[{\mathsf{\overline{\mathsf{k}}}}]$,
$\overline{\mathsf{T}}=\operatorname{\mathit{typeof}}(\mathsf{E}^{\prime})$,
and
$\overline{\mathsf{st}^{\prime}_{b}}=\operatorname{\mathit{body}}(\operatorname{{\mathcal{D}}}(\mathsf{M}^{\prime},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))$.
There are two options for $\overline{\mathsf{st}^{\prime}_{b}}$: it is the
body of either the most applicable original method or its specialization in
$\mathsf{M}^{\prime}$. Note that $\textsc{HOpt}_{0}$ can be built only with
OI-Refl, so $\mathsf{st}=\mathsf{st}^{\prime}$. Because by HM,
$\mathsf{M}=\lfloor\mathsf{M}^{\prime}\rfloor$, $\mathsf{M}$ has the same most
applicable original method as $\mathsf{M}^{\prime}$, and thus
$\mathsf{F}_{1},\,\mathsf{M}$ steps by Disp. By reasoning similar to the
forward direction, we get that the new top frames (as well as entire
configurations) are related by the optimization relation.

  * •

Case Direct. Here,
$\mathsf{st}^{\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{k}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$,
and the argument about HI and the soundness of type inference applies
similarly to the case (2) of Disp of the forward direction. As
$\textsc{HOpt}_{0}$ can be built only by OI-Direct, we know
$\mathsf{st}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$.
Furthermore, dispatch is defined in $\mathsf{M}$ by OI-Direct, and thus
$\mathsf{F}_{1},\,\mathsf{M}$ steps by Disp. By reasoning similar to the
forward direction, by HM, we know that the instructions in the new top frames
are related, and thus the entire configurations are also related.

∎

###### Theorem 4.12 (Correctness of Optimized Method Table).

For any well-formed method tables $\mathsf{M}$ and $\mathsf{M}^{\prime}$ where
(1) $\mathsf{M}\triangleright\mathsf{M}^{\prime}$, (2) table
$\mathsf{M}^{\prime}$ does not have stubs, and (3)
$\langle\mathsf{main}!{\epsilon}\,{\overline{\mathsf{st}}},\epsilon\rangle\in\mathsf{M}$,

$\epsilon\
\overline{\mathsf{st}},\,\mathsf{M}~{}{\rightarrow^{*}_{\mathcal{D}}}~{}\mathsf{E}\
\epsilon,\,\mathsf{M}\ \ \iff\ \ \epsilon\
\overline{\mathsf{st}},\,\mathsf{M}^{\prime}~{}{\rightarrow^{*}_{\mathcal{D}}}~{}\mathsf{E}\
\epsilon,\,\mathsf{M}^{\prime},$

i.e. program $\overline{\mathsf{st}}$ runs to the same final value environment
in both tables.

###### Proof.

This is a corollary of Lem. 4.11. By reflexivity of the optimization relation
and well-formedness of $\mathsf{M}$, we know:

$\overline{\mathsf{st}},\,\mathsf{M}\ \triangleright\
\overline{\mathsf{st}},\,\mathsf{M}^{\prime}\ <:\ \overline{\mathsf{ty}},$

where
$\overline{\mathsf{ty}}=\operatorname{\mathcal{I}}(\mathsf{M},\epsilon,\overline{\mathsf{st}})$.
Thus, the bisimulation lemma is applicable: if one of the configurations can
make a step, so does the other, and the step leads to a pair of related
configurations. Since method tables did not change, the lemma can be applied
again to these configurations, and so on. If the program terminates and does
not err, both sides arrive to final configurations where environments are
guaranteed to coincide by O-Stack. ∎

Next, we show that compilation as defined in Fig. 9 produces optimized code in
an optimized method table according to Fig. 10.

###### Theorem 4.13 (Compilation Satisfies Optimization Relation).

For any well-formed method tables $\mathsf{M}$ and $\mathsf{M}^{\prime}$,
typing $\overline{\mathsf{ty}}$, and instruction $\mathsf{st}$, such that

$\mathsf{M}\triangleright\mathsf{M}^{\prime}\ \ \land\ \
\overline{\mathsf{ty}}\ \vdash\ \mathsf{st},\,\mathsf{M}^{\prime}\ \leadsto\
\mathsf{st}^{\prime\prime},\,\mathsf{M}^{\prime\prime},$

it holds that:

  1. (1)

$\overline{\mathsf{ty}}\ \vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\
\mathsf{st}\ \triangleright\ \mathsf{st}^{\prime\prime},$

  2. (2)

$\mathsf{M}\triangleright\mathsf{M}^{\prime\prime},$

  3. (3)

and the optimization relation on $\mathsf{M},\mathsf{M}^{\prime}$ is preserved
on $\mathsf{M},\mathsf{M}^{\prime\prime}$:
$\forall\overline{\mathsf{ty}^{x}},\mathsf{st}^{x},\mathsf{st}^{y}.\quad\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}\ \ \implies\ \ \overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ \mathsf{st}^{x}\
\triangleright\ \mathsf{st}^{y}$.

###### Proof.

By induction on the derivation of $\overline{\mathsf{ty}}\ \vdash\
\mathsf{st},\,\mathsf{M}^{\prime}\ \leadsto\
\mathsf{st}^{\prime\prime},\,\mathsf{M}^{\prime\prime}$. Similar to the proof
of Lem. 4.8 on maximal devirtualization, the most interesting case is
C-Instance where compilation of additional instances happens.

  * •

Cases C-NoDisp and C-Disp are straightforward: by reflexivity of the
optimization relation, we immediately get $\overline{\mathsf{ty}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ \mathsf{st}\ \triangleright\
\mathsf{st}$; by assumption $\mathsf{M}\triangleright\mathsf{M}^{\prime}$ and
$\mathsf{M}^{\prime\prime}=\mathsf{M}^{\prime}$, we also have
$\mathsf{M}\triangleright\mathsf{M}^{\prime\prime}$; property (3) also holds
trivially because of $\mathsf{M}^{\prime\prime}=\mathsf{M}^{\prime}$.

  * •

Case C-Direct. Here,
$\mathsf{st}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$
and
$\mathsf{st}^{\prime\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{k}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$.
Since $\mathsf{M}^{\prime\prime}=\mathsf{M}^{\prime}$, we have
$\mathsf{M}\triangleright\mathsf{M}^{\prime\prime}$ by assumption, and (3)
holds trivially.
If $\mathsf{m}!{\overline{\mathsf{T}}}$ is an original method, then by
$\lfloor\mathsf{M}^{\prime}\rfloor=\mathsf{M}$ (because of
$\mathsf{M}\triangleright\mathsf{M}^{\prime}$) and the properties of dispatch,
$\mathsf{m}!{\overline{\mathsf{T}}}$ has to be the method returned by
$\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$.
Therefore,
$\operatorname{\mathit{signtr}}(\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))=\overline{\mathsf{T}}=\operatorname{\mathit{signtr}}(\mathsf{M}^{\prime\prime}[{\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}}])=\operatorname{\mathit{o-signtr}}(\mathsf{M}^{\prime\prime}[{\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}}]).$
If $\mathsf{m}!{\overline{\mathsf{T}}}$ is a compiled instance in
$\mathsf{M}^{\prime}$, then by well-formedness of $\mathsf{M}^{\prime}$, we
know that its original method is the most applicable method in
$\lfloor\mathsf{M}^{\prime}\rfloor$. Since
$\lfloor\mathsf{M}^{\prime}\rfloor=\mathsf{M}$, we get
$\operatorname{\mathit{signtr}}(\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))=\operatorname{\mathit{o-signtr}}(\mathsf{M}^{\prime\prime}[{\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}}])$.
Thus, for both original and compiled $\mathsf{m}!{\overline{\mathsf{T}}}$, we
have $\overline{\mathsf{ty}}\ \vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\
\mathsf{st}\ \triangleright\ \mathsf{st}^{\prime\prime}$ by OI-Direct.

  * •

Case C-Instance. Here,
$\mathsf{st}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$
and
$\mathsf{st}^{\prime\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{k}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$
like in previous case, but $\mathsf{M}^{\prime\prime}$ is obtained by
compiling the body of method
$\mathsf{m}!{\overline{\mathsf{ty}^{\prime}}}\,$$\overline{\mathsf{st}}$ that
is a dispatch target of
$\operatorname{{\mathcal{D}}}(\mathsf{M}^{\prime},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$
where $\overline{\mathsf{ty}^{\prime}}\neq\overline{\mathsf{T}}$. Because of
the latter condition, we know that
$\mathsf{m}!{\overline{\mathsf{ty}^{\prime}}}$ has to be an original method in
$\mathsf{M}^{\prime}$. Since $\lfloor\mathsf{M}^{\prime}\rfloor=\mathsf{M}$,
$\mathsf{m}!{\overline{\mathsf{ty}^{\prime}}}$ is also the most applicable
method in $\mathsf{M}$, so it has to be returned by
$\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$.
Now, let us consider
$\mathsf{M}_{0}=\mathsf{M}^{\prime}+\langle\mathsf{m}!{\overline{\mathsf{T}}}\epsilon,\overline{\mathsf{ty}^{\prime}}\rangle$.
Since $\mathsf{m}!{\overline{\mathsf{T}}}\notin\mathsf{M}^{\prime}$ and
$\mathsf{M}_{0}$ only adds a new stub of a compiled instance to the well-
formed $\mathsf{M}^{\prime}$, we know $\mathit{WF}(\mathsf{M}_{0})$.
Furthermore, because $\mathsf{M}\triangleright\mathsf{M}^{\prime}$ and
$\mathsf{M}_{0}$ adds the stub without modifying anything else in
$\mathsf{M}^{\prime}$, it is easy to show that all instruction optimizations
$\overline{\mathsf{ty}^{x}}\ \vdash_{\mathsf{M},\mathsf{M}^{\prime}}\
\mathsf{st}^{x}\ \triangleright\ \mathsf{st}^{y}$ are preserved by
$\mathsf{M}_{0}$, that is $\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{0}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}$, and thus $\mathsf{M}\triangleright\mathsf{M}_{0}$. Using the
result of type inference on the original body in
$\lfloor\mathsf{M}^{\prime}\rfloor$, i.e.
$\overline{\mathsf{ty}^{\prime\prime}}=\operatorname{\mathcal{I}}(\mathsf{M},\overline{\mathsf{T}},\overline{\mathsf{st}})$,
we can apply the induction hypothesis to
$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\ \vdash\
\mathsf{st}_{0},\,\mathsf{M}_{0}\ \leadsto\
\mathsf{st}^{\prime}_{0},\,\mathsf{M}_{1}$, which gives us:

    * –

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}_{1}}\ \mathsf{st}_{0}\ \triangleright\
\mathsf{st}^{\prime}_{0},$

    * –

$\mathsf{M}\triangleright\mathsf{M}_{1},$

    * –

$\forall\overline{\mathsf{ty}^{x}},\mathsf{st}^{x},\mathsf{st}^{y}.\quad\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{0}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}\ \ \implies\ \ \overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{1}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}$.

The fact that $\mathsf{M}\triangleright\mathsf{M}_{1}$ and
$\mathit{WF}(\mathsf{M}_{1})$ by Lem. 4.7, lets us apply the induction
hypothesis to the next instruction $\mathsf{st}_{1}$ of the method body
$\overline{\mathsf{st}}$, which produces:

    * –

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}_{2}}\ \mathsf{st}_{1}\ \triangleright\
\mathsf{st}^{\prime}_{1},$

    * –

$\mathsf{M}\triangleright\mathsf{M}_{2},$

    * –

$\forall\overline{\mathsf{ty}^{x}},\mathsf{st}^{x},\mathsf{st}^{y}.\quad\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{1}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}\ \ \implies\ \ \overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{2}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}$.

Now we can apply the latter to
$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}_{1}}\ \mathsf{st}_{0}\ \triangleright\
\mathsf{st}^{\prime}_{0}$, which gives us
$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}_{2}}\ \mathsf{st}_{0}\ \triangleright\
\mathsf{st}^{\prime}_{0}$.
Proceeding in this manner, we get:

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}_{n+1}}\ \overline{\mathsf{st}}\ \triangleright\
\overline{\mathsf{st}^{\prime}}$

and

$\forall\overline{\mathsf{ty}^{x}},\mathsf{st}^{x},\mathsf{st}^{y}.\quad\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}\ \ \implies\ \ \overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{n+1}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}.$

Finally, let us look at $\mathsf{M}^{\prime\prime}$. Its only difference from
$\mathsf{M}_{n+1}$ is the non-stub body $\overline{\mathsf{st}^{\prime}}$ for
$\mathsf{m}!{\overline{\mathsf{T}}}$. Thus, all $\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}_{n+1}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}$ are trivially preserved by $\mathsf{M}^{\prime\prime}$, which
gives us

$\forall\overline{\mathsf{ty}^{x}},\mathsf{st}^{x},\mathsf{st}^{y}.\quad\overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime}}\ \mathsf{st}^{x}\ \triangleright\
\mathsf{st}^{y}\ \ \implies\ \ \overline{\mathsf{ty}^{x}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ \mathsf{st}^{x}\
\triangleright\ \mathsf{st}^{y}$

and

$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ \overline{\mathsf{st}}\
\triangleright\ \overline{\mathsf{st}^{\prime}}.$

The latter lets us conclude
$\mathsf{M}\triangleright\mathsf{M}^{\prime\prime}$.
Finally, because
$\operatorname{\mathit{signtr}}(\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))=\overline{\mathsf{ty}^{\prime}}$
and $\mathsf{m}!{\overline{\mathsf{T}}}$ optimizes
$\mathsf{m}!{\overline{\mathsf{ty}^{\prime}}}$ in $\mathsf{M}^{\prime\prime}$,
we get

$\operatorname{\mathit{signtr}}(\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))=\operatorname{\mathit{o-signtr}}(\mathsf{M}^{\prime\prime}[{\mathsf{\mathsf{m}!{\overline{\mathsf{T}}}}}])$

and conclude $\overline{\mathsf{ty}}\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ \mathsf{st}\ \triangleright\
\mathsf{st}^{\prime\prime}$ by OI-Direct.

∎

Finally, using an auxiliary lemma about preserving stub methods during
compilation, we can show that the JIT-compilation semantics is equivalent to
the dispatch semantics.

###### Lemma 4.14 (Preserving Stubs).

For any well-formed method tables $\mathsf{M}^{\prime}$ and
$\mathsf{M}^{\prime\prime}$, typing $\overline{\mathsf{ty}}$, and instruction
$\mathsf{st}$, such that

$\overline{\mathsf{ty}}\ \vdash\ \mathsf{st},\,\mathsf{M}^{\prime}\ \leadsto\
\mathsf{st}^{\prime\prime},\,\mathsf{M}^{\prime\prime},$

it holds that

$\\{\overline{\mathsf{T}}\ |\
\mathsf{m}!{\overline{\mathsf{T}}}\,{\epsilon}\in\mathsf{M}^{\prime}\\}=\\{\overline{\mathsf{T}}\
|\
\mathsf{m}!{\overline{\mathsf{T}}}\,{\epsilon}\in\mathsf{M}^{\prime\prime}\\},$

i.e. the set of stubbed method instances is preserved by a compilation step.

###### Proof.

By induction on the derivation of $\overline{\mathsf{ty}}\ \vdash\
\mathsf{st},\,\mathsf{M}^{\prime}\ \leadsto\
\mathsf{st}^{\prime\prime},\,\mathsf{M}^{\prime\prime}$, similar to the proof
of Lem. 4.7 on well formedness.

All cases except for C-Instance are trivial because the method table does not
change. For C-Instance, let’s denote the set of stubs in $\mathsf{M}^{\prime}$
by ${\sf{S}}^{\prime}$, that is:

${\sf{S}}^{\prime}=\\{\overline{\mathsf{T}}\ |\
\mathsf{m}!{\overline{\mathsf{T}}}\,{\epsilon}\in\mathsf{M}^{\prime}\\}.$

Since $\mathsf{m}!{\overline{\mathsf{T}}}\notin\mathsf{M}^{\prime}$ and
$\mathsf{M}_{0}=\mathsf{M}^{\prime}+\langle\mathsf{m}!{\overline{\mathsf{T}}}\epsilon,\overline{\mathsf{ty}^{\prime}}\rangle$,
we have ${\sf{S}}_{0}={\sf{S}}^{\prime}\cup\\{\overline{\mathsf{T}}\\}$. By
applying the induction hypothesis to
$\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime\prime}}\ \vdash\
\mathsf{st}_{0},\,\mathsf{M}_{0}\ \leadsto\
\mathsf{st}^{\prime}_{0},\,\mathsf{M}_{1}$, we know that the set
${\sf{S}}_{1}$ of stubs of $\mathsf{M}_{1}$ is the same as ${\sf{S}}_{0}$, and
$\mathsf{M}_{1}$ is well-formed by Lem. 4.7. Proceeding by applying the
induction hypothesis to compilation of all $\mathsf{st}_{i}$, we get that:

${\sf{S}}_{n+1}={\sf{S}}_{0}={\sf{S}}^{\prime}\cup\\{\overline{\mathsf{T}}\\}.$

Finally, the only difference between $\mathsf{M}^{\prime\prime}$ and
$\mathsf{M}_{n+1}$ is that the stub for $\mathsf{m}!{\overline{\mathsf{T}}}$
is replaced by an actual method body. Therefore, we get the desired property:

${\sf{S}}^{\prime\prime}={\sf{S}}_{n+1}\setminus\\{\overline{\mathsf{T}}\\}={\sf{S}}^{\prime}.$

∎

###### Lemma 4.15 (Bisimulation of Related Configurations with Dispatch and
JIT Semantics).

For any well-formed method tables $\mathsf{M}$ and $\mathsf{M}^{\prime}$ where
$\mathsf{M}^{\prime}$ does not have stubs, any frame stacks $\mathsf{F}_{1}$,
$\mathsf{F}^{\prime}_{1}$, and stack typing $\Delta_{1}$, such that
$\mathsf{F}_{1},\,\mathsf{M}\ \triangleright\
\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}\ <:\ \Delta_{1}$, the following
holds:

  1. (1)

Forward direction:

$\begin{array}[]{l}\mathsf{F}_{1},\,\mathsf{M}~{}{\rightarrow_{\mathcal{D}}}~{}\mathsf{F}_{2},\,\mathsf{M}\implies\exists\mathsf{F}^{\prime}_{2},\mathsf{M}^{\prime\prime},\Delta^{\prime}_{1}.\quad\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathsf{JIT}}}~{}\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime\prime}\
\ \land\ \ \mathsf{F}_{2},\,\mathsf{M}\ \triangleright\
\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime\prime}\ <:\
\Delta^{\prime}_{1}.\end{array}$

  2. (2)

Backward direction:

$\begin{array}[]{l}\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathsf{JIT}}}~{}\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime\prime}\implies\exists\mathsf{F}_{2},\Delta^{\prime}_{1}.\quad\mathsf{F}_{1},\,\mathsf{M}~{}{\rightarrow_{\mathcal{D}}}~{}\mathsf{F}_{2},\,\mathsf{M}\
\ \land\ \ \mathsf{F}_{2},\,\mathsf{M}\ \triangleright\
\mathsf{F}^{\prime}_{2},\,\mathsf{M}^{\prime\prime}\ <:\
\Delta^{\prime}_{1}.\end{array}$

Furthermore, $\mathsf{M}^{\prime\prime}$ is well-formed and does not have
stubs.

###### Proof.

By case analysis on the derivation of optimization
$\mathsf{F}_{1},\,\mathsf{M}\ \triangleright\
\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}\ <:\ \Delta_{1}$ and case
analysis on the step ($~{}{\rightarrow_{\mathcal{D}}}~{}$ for the forward and
$~{}{\rightarrow_{\mathsf{JIT}}}~{}$ for the backward direction), similarly to
the proof of bisimulation for the dispatch semantics (Lem. 4.11). The only
difference appears in cases where
$\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}$ steps by Disp: these are the
only places where JIT compilation fires and $\mathsf{M}^{\prime\prime}$ might
be different from $\mathsf{M}^{\prime}$. As an example, we consider only the
case of the forward direction where
$\mathsf{F}_{1},\,\mathsf{M}~{}{\rightarrow_{\mathcal{D}}}~{}\mathsf{F}_{2},\,\mathsf{M}$
steps by Disp, and $\textsc{HOpt}_{0}$ is built by OI-Refl, reusing all the
notation from Lem. 4.11. Thus, we have
$\mathsf{st}=\mathsf{st}^{\prime}={\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{i}}\leftarrow{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{j}}~{}?~{}\mathsf{\mathsf{m}}(\overline{{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{k}}}):{\scalebox{0.8}{{\normalsize\%}}}\mathsf{\mathsf{l}}$,
$\mathsf{F}_{1}=(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F}$,
$\mathsf{F}^{\prime}_{1}=(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime}$,
$\Delta_{1}=(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta$,
and $\mathsf{F}_{1},\,\mathsf{M}$ steps as:

$(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F},\,\mathsf{M}~{}{\rightarrow_{\mathcal{D}}}~{}(\mathsf{E}^{\prime}\
\overline{\mathsf{st}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F},\,\mathsf{M},$

where $\mathsf{E}^{\prime}=\mathsf{E}[{\mathsf{\overline{\mathsf{k}}}}]$,
$\overline{\mathsf{T}}=\operatorname{\mathit{typeof}}(\mathsf{E}^{\prime})$,
and
$\overline{\mathsf{st}_{b}}=\operatorname{\mathit{body}}(\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}}))$.
$\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}$ can step only by Disp, which
triggers JIT compilation. According to the definition of
$\operatorname{\mathit{jit}}$ from Fig. 7, there are two possibilities: either
$\mathsf{m}!{\overline{\mathsf{T}}}$ is already in $\mathsf{M}^{\prime}$, in
which case $\mathsf{M}^{\prime\prime}=\mathsf{M}^{\prime}$, or
$\mathsf{m}!{\overline{\mathsf{T}}}$ is not in $\mathsf{M}^{\prime}$, in which
case the new method instance gets compiled and added to
$\mathsf{M}^{\prime\prime}$.

  * •

In the former case, the proof proceeds exactly as in Lem. 4.11.

  * •

In the latter case, by Thm. 4.13, we know that
$\mathsf{M}\triangleright\mathsf{M}^{\prime\prime}$ and all instruction
optimizations on $\mathsf{M},\mathsf{M}^{\prime}$ are preserved for
$\mathsf{M},\mathsf{M}^{\prime\prime}$. Therefore, we know:

$(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta\
\vdash_{\mathsf{M},\mathsf{M}^{\prime\prime}}\ (\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F}\ \triangleright\
(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime}.$

Furthermore, as $\mathsf{M}^{\prime}$ is well-formed and does not have stubs
by assumption, $\mathsf{M}^{\prime\prime}$ is also well-formed by Lem. 4.7 and
does not have stubs by Lem. 4.14. Reasoning similarly to Lem. 4.11, we can see
that the body $\overline{\mathsf{st}_{b}}$ of the original method returned by
$\operatorname{{\mathcal{D}}}(\mathsf{M},\mathsf{\mathsf{m}},{\overline{\mathsf{T}}})$
optimizes to the body $\overline{\mathsf{st}^{\prime}_{b}}$ of the compiled
instance $\mathsf{m}!{\overline{\mathsf{T}}}$. Thus, we get that
$\mathsf{F}^{\prime}_{1},\,\mathsf{M}^{\prime}$ steps by Disp,

$(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime}~{}{\rightarrow_{\mathsf{JIT}}}~{}(\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime\prime},$

the resulting configurations are related,

$(\mathsf{E}^{\prime}\ \overline{\mathsf{st}_{b}})\cdot(\mathsf{E}\
\mathsf{st}\,\overline{\mathsf{st}})\cdot\mathsf{F},\,\mathsf{M}\
\triangleright\ (\mathsf{E}^{\prime}\
\overline{\mathsf{st}^{\prime}_{b}})\cdot(\mathsf{E}\
\mathsf{st}^{\prime}\,\overline{\mathsf{st}^{\prime}})\cdot\mathsf{F}^{\prime},\,\mathsf{M}^{\prime\prime}\
<:\
(\overline{\mathsf{T}}\,\overline{\mathsf{ty}^{\prime}})\cdot(\overline{\mathsf{ty}}^{\mathsf{E}}\mathsf{ty}\,\overline{\mathsf{ty}})\cdot\Delta,$

and $\mathsf{M}^{\prime\prime}$ has no stubs.

∎

###### Theorem 4.16 (Correctness ot JIT).

For any original well-formed method table $\mathsf{M}$ the following holds:

$\epsilon\
\overline{\mathsf{st}},\,\mathsf{M}~{}{\rightarrow^{*}_{\mathcal{D}}}~{}\mathsf{E}\
\epsilon,\,\mathsf{M}\ \ \iff\ \ \epsilon\
\overline{\mathsf{st}},\,\mathsf{M}~{}{\rightarrow^{*}_{\mathsf{JIT}}}~{}\mathsf{E}\
\epsilon,\,\mathsf{M}^{\prime},$

i.e. program $\overline{\mathsf{st}}$ runs to the final environment
$\mathsf{E}$ with the dispatch semantics $~{}{\rightarrow_{\mathcal{D}}}~{}$
if and only if it runs to the same environment with the JIT-compilation
semantics $~{}{\rightarrow_{\mathsf{JIT}}}~{}$.

###### Proof.

This is a corollary of Lem. 4.15. Be reflexivity of the optimization relation
and well-formedness of $\mathsf{M}$, we know:
$\overline{\mathsf{st}},\,\mathsf{M}\ \triangleright\
\overline{\mathsf{st}},\,\mathsf{M}\ <:\ \overline{\mathsf{ty}}$, where
$\overline{\mathsf{ty}}=\operatorname{\mathcal{I}}(\mathsf{M},\epsilon,\overline{\mathsf{st}})$.
Since $\mathsf{M}$ does not have stubs, the bisimulation lemma is applicable:
if one of the configurations can make a step, so does the other, and the step
leads to a pair of related configurations such that the lemma can be applied
again. If the program terminates and does not err, both sides arrive to final
configurations where environments are guaranteed to coincide by O-Stack. ∎

##  5\. Empirical Study

Anecdotal evidence suggests that type stability is discussed in the Julia
community, but does Julia code exhibit the properties of stability and
groundedness in practice? And if so, are there any indicators correlated with
instability and ungroundedness? To find out, we ran a dynamic analysis on a
corpus of Julia packages. All the packages come from the main language
registry and are readily available via Julia’s package manager; registered
packages have to pass basic sanity checks and usually have a test suite.

The main questions of this empirical study are:

  1. (1)

How uniformly are type stability and groundedness spread over Julia packages?
How much of a difference can users expect from different packages?

  2. (2)

Are package developers aware of type stability?

  3. (3)

Are there any predictors of stability and groundedness in the code and do they
influence how type-stable code looks?

###  5.1. Methodology

We take as our main corpus the 1000 most starred (using GitHub stars) packages
from the Julia package registry; as of the beginning of 2021, the registry
contained about 5.5K packages. The main corpus is used for an automated, high-
level, aggregate analysis. We also take the 10 most starred packages from the
corpus to perform finer-grained analysis and manual inspection. Out of the
1000 packages in the corpus, tests suits of only 760 succeeded on Julia 1.5.4,
so these 760 comprise our final corpus. The reasons of failures are diverse,
spanning from missing dependencies to the absence of tests, to timeout.

For every package of interest, the dynamic analysis runs the package test
suite, analyzes compiled method instances, and records information relevant to
type stability and groundedness. Namely, once a test suite runs to completion,
we query Julia’s virtual machine for the current set of available method
instances, which represent instances compiled during the tests’ execution. To
avoid bias towards the standard library, we remove instances of methods
defined in standard modules, such as Base, Core, etc., which typically leaves
us with several hundreds to several thousands of instances. For these
remaining instances, we analyze their type stability and groundedness. As type
information is not directly available for compiled, optimized code, we
retrieve the original method of an instance and run Julia’s type inferencer to
obtain each register’s type, similarly to the $\mathsf{Jules}$ model. In rare
cases, type inference may fail; on our corpus, this almost never happened,
with at most 5 failures per package. With the inference results at hand, we
check the concreteness of the register typing and record a yes/no answer for
both stability and groundedness. In addition to that, several metrics are
recorded for each method: method size, the number of gotos and returns in the
body, whether the method has varargs or @nospecialize
arguments666@nospecialize tells the compiler to _not_ specialize for that
argument and leave it abstract., and how polymorphic the method is, i.e. how
many instances were compiled for it. This information is then used to identify
possible correlations between the metrics and stability/groundedness.

To get a better understanding of type stability and performance, we employ
several additional tools to analyze the 10 packages. For example, we look at
their documentation, especially at the stated goals and domain of a package,
and check the Git history to see if and how type stability is mentioned in the
commits.

Table 1. Aggregate statistics for stability and groundedness | Stable | Grounded
---|---|---
Mean | 74% | 57%
Median | 80% | 57%
Std. Dev. | 22% | 24%

###  5.2. Package-Level Analysis

The aggregate results of the dynamic analysis for the 760 packages are shown
in Table 1: 74% of method instances in a package are stable and 57% grounded,
on average; median values are close to the means. The standard deviation is
noticeable, so even on small samples of packages, we expect to see packages
with large deflections from the means.

A more detailed analysis of the 10 most starred packages, in alphabetical
order, is shown in Table 2. A majority of these packages have stability
numbers very close to the averages shown above, with the exception of Knet,
which has only 16% of stable and 8% of grounded instances.

Table 2. Stability, groundedness, and polymorphism in 10 popular packages Package | Methods | Instances | Inst/Meth | Varargs | Stable | Grounded
---|---|---|---|---|---|---
DifferentialEquations | 1355 | 7381 | 5.4 | 3% | 70% | 44%
Flux | 381 | 4288 | 11.3 | 13% | 76% | 70%
Gadfly | 1100 | 4717 | 4.3 | 10% | 81% | 58%
Gen | 973 | 2605 | 2.7 | 2% | 64% | 43%
Genie | 532 | 1401 | 2.6 | 12% | 93% | 78%
IJulia | 39 | 136 | 3.5 | 8% | 84% | 60%
JuMP | 2377 | 36406 | 15.3 | 7% | 83% | 63%
Knet | 594 | 9013 | 15.2 | 7% | 16% | 8%
Plots | 1167 | 5377 | 4.6 | 8% | 74% | 58%
Pluto | 727 | 2337 | 3.2 | 4% | 80% | 66%

The Knet package is a type stability outlier. A quick search over project’s
documentation and history shows that the only kind of stability ever mentioned
is numerical stability; furthermore, the word ‘‘performance’’ is mostly used
to reference the performance of neural networks or CUDA-related utilities.
Indeed, the package primarily serves as a communication layer for a GPU; most
computations are done by calling the CUDA API for the purpose of building deep
neural networks. Thus, in this specific domain, type stability of Julia code
appears to be irrelevant.

On the other side of the stability spectrum is the 93% stable (78% grounded)
Genie package, which provides a web application framework. Inspecting the
package, we can confirm that its developers were aware of type stability and
intentional about performance. For example, Genie’s Git history contains
several commits mentioning (improved) ‘‘type stability.’’ The project README
file states that the authors build upon

> “Julia’s strengths (high-level, high-performance, dynamic, JIT compiled).”

Furthermore, the tutorial claims:

> “Genie’s goals: unparalleled developer productivity, excellent run-time
> performance.”

##### Type stability (non-)correlates

One parameter that we conjectured may correlate with stability is the average
number of method instances per method (Inst/Meth column of Table 2), as it
expresses the amount of polymorphism discovered in a package. Most of the
packages compile just 2--4 instances per method on average, but Flux, JuMP,
and Knet have this metric 5--6 times higher, with JuMP and Knet exploiting
polymorphism the most, at 15.3 and 15.2 instances per method, respectively.
The latter may be related to the very low type stability index of Knet.
However, the other two packages are more stable than the overall average.
Analyzing JuMP and Flux further, we order their methods by the number of
instances. In JuMP, the top 10% of most instantiated methods are 5% less
stable and grounded than the package average, whereas in Flux, the top 10%
have about the same stability characteristics as on average. Overall, we
cannot conclude that method polymorphism is related to type stability.

Another dimension of polymorphism is the variable number of arguments in a
method (Varargs column of Table 2). We looked into three packages with a
higher than average (9%) number of varargs methods in the 10 packages: Flux,
Gadfly and Genie. Relative to the total number of methods, Flux has the most
varargs methods---13%---and those methods are only 55% stable and 44%
grounded, which is a significant drop of 21% and 26% below this package’s
averages. However, the other two packages have higher-than-package-average
stability rates, 82% (Gadfly) and 99% (Genie), with groundedness being high in
Genie, 93%, and low in Gadfly, 38%. Again, no general conclusion about the
relationship between varargs methods and their stability can be made.

###  5.3. Method-Level Analysis

In this section, we inspect stability of individual methods in its possible
relationship with other code properties like size, control flow (number of
goto and return statements), and polymorphism (number of compiled instances
and varargs). Our analysis consists of two steps: first, we plot histograms
showing the number of methods with particular values of properties, and
second, we manually sample some of the methods with more extreme
characteristics.

####  5.3.1. Graphical Analysis

We use two-dimensional histograms like those presented in Fig. 11 to discover
possible relationships between stability of code and its other properties. The
vertical axis measures stability (on the left diagram) or groundedness (on the
right): $1$ means that all recorded instances of a method are stable/grounded,
and $0$ means that none of them are. The horizontal axis measures the property
of interest; in the case of Fig. 11, it is method size (actual numbers are not
important here: they are computed from Julia’s internal representation of
source code). The color of an area reflects how many methods have
characteristics corresponding to that area’s position on the diagram; e.g. in
Fig. 11, the lonely yellow areas indicate that there are about 500 (400) small
methods that are stable (grounded).

Figure 11. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX) in Pluto

Stability and groundedness by method size in Pluto

We generate graphs for all of the 10 packages listed in Table 2, for all
combinations of the properties of interest; the graphs are provided in
Appendix A . Most of the graphs look very similar to the ones from Fig. 11,
which depicts Pluto---a package for creating Jupyter-like notebooks in Julia.
In the following paragraphs, we discuss features of these graphs and highlight
the discrepancies.

The first distinctive feature of the graphs is the hot area in the top-left
corner: most of the 10 packages employ many small, stable/grounded methods;
the bottom-left corner is usually the second-most hot, so a significant number
of small methods are unstable/ungrounded. For the Knet package, these two
corners are reversed; for DifferentialEquations, they are reversed only on the
groundedness plot. Both of these facts are not surprising after seeing Table
2, but having a visual tool to discover such facts may be useful for package
developers.

The second distinctive feature of these graphs is the behavior of large,
ungrounded methods (bottom-right part of the right-hand-side graph). The
‘‘tail’’ of large methods on the groundedness graphs almost always lies below
the $1$-level; furthermore, larger methods tend to be less grounded. However,
if we switch from groundedness to stability plots, a large portion of the tail
jumps to the $1$-level. This means larger methods are unlikely to be grounded
(as expected, because of the growing number of registers), but they still can
be stable and thus efficiently used by other methods. Pluto provides a good
example of such a method: its explore! method of size 13003 (right-most
rectangle on Fig. 11, 330 lines in the source code) analyzes Julia syntax
trees for scope information with a massive if/else if/.. statement. This
method has a very low chance of being grounded, and it was not grounded on the
runs we analyzed. However, the method has a concrete return type annotation,
so Julia (and the programmer) can easily see that it is stable.

In the case of the number of gotos and returns, the plots are largely similar
to the ones for method size, but they highlight one more package with low
groundedness. Namely, the Gen package (aimed at probabilistic inference
(Cusumano-Towner et al., 2019)) has the hottest area in the bottom-left
corner, contrary to the first general property we identified for the size-
based plots. Recall (Tables 1 and 2) that Gen’s groundedness is 14% less than
the average on the whole corpus of 760 packages.

####  5.3.2. Manual Inspection

To better understand the space of stable methods, we performed a qualitative
analysis of a sample of stable methods that have either large sizes or many
instances.

Many large methods have one common feature: they often have a return type
ascription on the method header of the form:

⬇

function f(...) :: Int

...

end

These ascriptions are a relatively new tool in Julia, and they are used only
occasionally, in our experience. An ascription makes the Julia compiler insert
implicit conversions on all return paths of the method. Conversions are user
extendable: if the user defines type A, they can also add methods of a special
function convert for conversion to A. This function will be called when the
compiler expects A but infers a different type, for example, if the method
returns B. If the method returns A, however, then convert is a no-op.

Type ascriptions may be added simply as documentation, but they can also be
used to turn type instability into a run-time error: if the ascribed type is
concrete and a necessary conversion is not available, the method will fail.
This provides a useful, if unexpected, way to assure that a large method never
becomes unstable.

While about 85% of type-stable methods in the top 10 packages are
uninteresting in that they always return the same type, sampling the rest
illuminates a clear pattern: the methods resemble what we are used to see in
statically typed languages with parametric polymorphism. Below is a list of
categories that we identify in this family.

  * •

Various forms of the identity function---a surprisingly popular function that
packages keep reinventing. In an impure language, such as Julia, an identity
function can produce various side effects. For example, the Genie package adds
a caching effect to its variant of the identity function:

⬇

# Define the secret token used in the app for encryption and salting.

function secret_token!(value::AbstractString=Generator.secret_token())

SECRET_TOKEN[] = value

return value

end

  * •

Container manipulations for various kinds of containers, such as arrays,
trees, or tuples. For instance, the latter is exemplified by the following
function from Flux, which maps a tuple of functions by applying them to the
given argument:

⬇

function extraChain(fs::Tuple, x)

res = first(fs)(x)

return (res, extraChain(Base.tail(fs), res)...)

end

extraChain(::Tuple{}, x) = ()

  * •

Smart constructors for user-defined polymorphic structures. For example, the
following convenience function from JuMP creates an instance of the
VectorConstraint structure with three fields, each of which is polymorphic:

⬇

function build_constraint(_error::Function, Q::Symmetric{V,M}, ::PSDCone)

where {V<:AbstractJuMPScalar,M<:AbstractMatrix{V}}

n = LinearAlgebra.checksquare(Q)

shape = SymmetricMatrixShape(n)

return VectorConstraint(

vectorize(Q, shape),

MOI.PositiveSemidefiniteConeTriangle(n),

shape)

end

  * •

Type computations---an unusually wide category for a dynamically typed
language. Thus, for instance, the Gen package defines a type that represents
generative functions in probabilistic programming, and a function that
extracts the return and argument types:

⬇

# Abstract type for a generative function with return value type T and trace
type U.

abstract type GenerativeFunction{T,U <: Trace} end

get_return_type(::GenerativeFunction{T,U}) where {T,U} = T

get_trace_type(::GenerativeFunction{T,U}) where {T,U} = U

###  5.4. Takeaways

Our analysis shows that a Julia user can expect mostly stable (74%) and
somewhat grounded (57%) code in widely used Julia packages. If the authors are
intentional about performance and stability, as demonstrated by the Genie
package, those numbers can be much higher. Although our sample of packages is
too small to draw strong conclusions, we suggest that several factors can be
used by a Julia programmer to pinpoint potential sources of instability in
their package. For example, in some cases, varargs methods might indicate
instability. Large methods, especially ones with heavy control flow, tend to
not be type grounded but often are stable; in particular, if they always
return the same concrete type. Finally, although highly polymorphic methods
are neither stable nor unstable in general, code written in the style of
parametric polymorphism often suggests type stability.

Our dynamic analysis and visualization code is written in Julia (and some bash
code), and relies on the vanilla Julia implementation. Thus, it can be
employed by package developers to study type instability in their code, as
well as check for regressions.

##  6\. Related Work

Type stability and groundedness are the consequences of Julia’s compilation
strategy put into practice. The approach Julia takes is new and simpler than
other approaches to efficient compilation of dynamic code.

Attempts to efficiently compile dynamically dispatched languages go back
nearly as far as dynamically dispatched languages themselves. Atkinson (1986)
used a combination of run-time-checked user-provided types and a simple type
inference algorithm to inline methods. Chambers and Ungar (1989) pioneered the
just-in-time model of compilation in which methods are specialized based on
run-time information. Hölzle and Ungar (1994) followed up with method inlining
optimization based on recently observed types at the call site. Rigo (2004)
specialized methods on invocation based on their arguments, but this was
limited to integers. Similarly, Cannon (2005) developed a type-inferring just-
in-time compiler for Python, but it was limited by the precision of type
inference. Logozzo and Venter (2010) extended this approach with a more
sophisticated abstract interpretation-based inference system for JavaScript.

At the same time, trace-based compilers approached the problem from another
angle (Chang et al., 2007). Instead of inferring from method calls, these
compilers had exact type information for variables in straight-line fragments
of the program called traces. Gal et al. (2009) describes a trace-based
compiler for JavaScript that avoids some pitfalls of type stability, as traces
can cross method boundaries. However, it is more difficult to fix a program
when tracing does not work well, for the boundaries of traces are not apparent
to the programmer.

Few of these approaches to compilation have been formalized. Guo and Palsberg
(2011) described the core of a trace-based compiler with two optimizations,
variable folding and dead branch/store elimination. Myreen (2010) formalized
self-modifying code for x86. Finally, Flückiger et al. (2018) formally
described speculation and deoptimization and proved correctness of some
optimizations; Barriere et al. (2021) extended and mechanized these results.

The Julia compiler uses standard techniques, but differs considerably in how
it applies them. Many production just-in-time compilers rely on static type
information when it is available, as well as a combination of profiling and
speculation (Duboscq et al., 2013; Würthinger et al., 2012). Speculation
allows these compilers to perform virtual dispatch more efficiently (Flückiger
et al., 2020). Profiling allows for tuning optimizations to a specific
workload (Xu et al., 2009; Ottoni, 2018), eliminating overheads not required
for cases observed during execution. Julia, on the other hand, performs
optimization only once per method instance. This presents both advantages and
issues. For one, Julia’s performance is more predictable than that of other
compilers, as the warmup is simple (Barrett et al., 2017). Overall, Julia is
able to achieve high performance with a simple compiler.

##  7\. Conclusion

Julia’s performance is impressive, as it improves on that of a statically
typed language such as Java, whose compiler has been developed for two decades
by an army of engineers. This is achieved by a combination of careful language
design, simple but powerful compiler optimizations, and disciplined use of
abstractions by programmers.

In this paper, we formally define the notions of type stability and
groundedness, which guide programmers towards code idioms the compiler can
optimize. To this end, we model Julia’s intermediate representation with an
abstract machine called $\mathsf{Jules}$, prove the correctness of its JIT
compiler, and show that type groundedness is the property that enables the
compiler to devirtualize method calls. The weaker notion of type stability is
still useful as it allows callers of a function to be grounded. This
relationship between groundedness and stability explains the discrepancy
between the definition of stability and what programmers do in practice,
namely, inspecting the compiler’s output to look for variables that have
abstract types. Our corpus analysis of Julia packages shows that more than
half of compiled methods are grounded, and over two-thirds are stable. This
suggests that developers follow type-related performance guidelines.

Although our analysis suggests high presence of type-stable code, some Julia
packages, even among more popular ones, have significant unstable portions.
This may indicate an oversight from the package authors, albeit an
understandable one: the tools for detecting unstable code are
limited.777Besides manually calling @code_warntype, one can use JET.jl
package in “performance linting” mode. JET relies on Julia’s type inference;
its primary goal is to report likely dynamic-dispatch errors, and it does not
provide sound analysis. There is a future work opportunity in developing a
user-facing static type system that would soundly determine whether a method
is type stable or not. This could provide the benefits of a traditional
(gradual) type system, and additionally, allow programmers to ensure type
stability. A less demanding approach to facilitating stability would be to add
primitives for reifying the programmer’s intent. For example, the user could
write assert(is_type_stable()) to indicate that the method does not tolerate
inefficient compilation.

Although the specific optimizations enabled by grounded code may not be as
important for other languages, they can benefit from the lessons learned from
Julia’s performance model: namely, that the interface exposed by a compiler
can be just as important as the cleverness of the compiler itself. Performance
is not an isolated property: it is the result of a dialogue between the
compiler and the programmers that use it.

## Data Availability Statement

The paper is accompanied by the artifact (Pelenitsyn et al., 2021b)
reproducing the results of Sec. 5. In particular, the artifact contains the
list of 1000 Julia packages analyzed (with the exact package versions), as
well as Bash and Julia scripts performing stability analysis and generating
Tables 1 and 2, and Fig. 11.

## Acknowledgments

We thank Ming-Ho Yee and the anonymous reviewers for their insightful comments
and suggestions to improve this paper.

This work was supported by Office of Naval Research (ONR) award 503353, the
National Science Foundation awards 1759736, 1925644, 1618732, CCF-1909143 and
CCF-1908389 the Czech Ministry of Education from the Czech Operational
Programme Research, Development, and Education, under grant agreement No.
CZ.02.1.01/0.0/0.0/15_003/0000421, and the European Research Council under the
European Union’s Horizon 2020 research and innovation programme, under grant
agreement No. 695412.

## References

  * (1)
  * Aigner and Hölzle (1996) Gerald Aigner and Urs Hölzle. 1996.  Eliminating Virtual Function Calls in C++ Programs. In _European Conference on Object-Oriented Programming (ECOOP)_.  https://doi.org/10.1.1.7.7766
  * Atkinson (1986) Robert G. Atkinson. 1986\.  Hurricane: An Optimizing Compiler for Smalltalk. In _Object-Oriented Programming Systems, Languages and Applications (OOPSLA)_.  https://doi.org/10.1145/960112.28712
  * Barrett et al. (2017) Edd Barrett, Carl Friedrich Bolz-Tereick, Rebecca Killick, Sarah Mount, and Laurence Tratt. 2017.  Virtual Machine Warmup Blows Hot and Cold.  _Proc. ACM Program. Lang._ 1, OOPSLA (2017).  https://doi.org/10.1145/3133876
  * Barriere et al. (2021) Aurele Barriere, Olivier Flückiger, Sandrine Blazy, David Pichardie, and Jan Vitek. 2021\.  Formally Verified Speculation and Deoptimization in a JIT Compiler.  _Proc. ACM Program. Lang._ 5, POPL (2021).  https://doi.org/10.1145/3434327
  * Belyakova et al. (2020) Julia Belyakova, Benjamin Chung, Jack Gelinas, Jameson Nash, Ross Tate, and Jan Vitek. 2020\.  World Age in Julia: Optimizing Method Dispatch in the Presence of Eval.  _Proc. ACM Program. Lang._ 4, OOPSLA (2020).  https://doi.org/10.1145/3428275
  * Bezanson et al. (2018) Jeff Bezanson, Jiahao Chen, Ben Chung, Stefan Karpinski, Viral B. Shah, Jan Vitek, and Lionel Zoubritzky. 2018.  Julia: Dynamism and Performance Reconciled by Design.  _Proc. ACM Program. Lang._ 2, OOPSLA (2018).  https://doi.org/10.1145/3276490
  * Bezanson et al. (2017) Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B. Shah. 2017.  Julia: A Fresh Approach to Numerical Computing.  _SIAM Rev._ 59, 1 (2017).  https://doi.org/10.1137/141000671
  * Cannon (2005) Brett Cannon. 2005\.  _Localized Type Inference of Atomic Types in Python_.  Master’s thesis. California Polytechnic State University.
  * Chambers and Ungar (1989) Craig Chambers and David Ungar. 1989.  Customization: Optimizing Compiler Technology for SELF, a Dynamically-Typed Object-Oriented Programming Language. In _Proceedings of the ACM Programming Language Design and Implementation Conference (PLDI)_. 146--160.  https://doi.org/10.1145/73141.74831
  * Chang et al. (2007) Mason Chang, Michael Bebenita, Alexander Yermolovich, Andreas Gal, and Michael Franz. 2007\.  _Efficient just-in-time execution of dynamically typed languages via code specialization using precise runtime type inference_.  Technical Report. Donald Bren School of Information and Computer Science, University of California, Irvine, 2007.
  * Cusumano-Towner et al. (2019) Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka. 2019.  Gen: A General-purpose Probabilistic Programming System with Programmable Inference. In _Proceedings of the ACM Programming Language Design and Implementation Conference (PLDI)_.  https://doi.org/10.1145/3314221.3314642
  * Deutsch and Schiffman (1984) L. Peter Deutsch and Allan M. Schiffman. 1984.  Efficient Implementation of the Smalltalk-80 System. In _ACM Symposium on Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/800017.800542
  * Duboscq et al. (2013) Gilles Duboscq, Thomas Würthinger, Lukas Stadler, Christian Wimmer, Doug Simon, and Hanspeter Mössenböck. 2013.  An Intermediate Representation for Speculative Optimizations in a Dynamic Compiler. In _Workshop on Virtual Machines and Language Implementations (VMIL)_.  https://doi.org/10.1145/2542142.2542143
  * Flückiger et al. (2020) Olivier Flückiger, Guido Chair, Ming-Ho Yee, Jan Jecmen, Jakob Hain, and Jan Vitek. 2020.  Contextual Dispatch for Function Specialization.  _Proc. ACM Program. Lang._ 4, OOPSLA (2020).  https://doi.org/10.1145/3428288
  * Flückiger et al. (2018) Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, and Jan Vitek. 2018.  Correctness of speculative optimizations with dynamic deoptimization.  _Proc. ACM Program. Lang._ 2, POPL (2018).  https://doi.org/10.1145/3158137
  * Gal et al. (2009) Andreas Gal, Brendan Eich, Mike Shaver, David Anderson, David Mandelin, Mohammad R. Haghighat, Blake Kaplan, Graydon Hoare, Boris Zbarsky, Jason Orendorff, Jesse Ruderman, Edwin W. Smith, Rick Reitmaier, Michael Bebenita, Mason Chang, and Michael Franz. 2009\.  Trace-based just-in-time type specialization for dynamic languages. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/1543135.1542528
  * Guo and Palsberg (2011) Shu-yu Guo and Jens Palsberg. 2011.  The Essence of Compiling with Traces. In _Symposium on Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/1926385.1926450
  * Hölzle and Ungar (1994) U. Hölzle and D. Ungar. 1994.  Optimizing dynamically-dispatched calls with run-time type feedback. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/178243.178478
  * Logozzo and Venter (2010) Francesco Logozzo and Herman Venter. 2010.  RATA: Rapid Atomic Type Analysis by Abstract Interpretation -- Application to JavaScript Optimization. In _Compiler Construction (CC)_.  https://doi.org/10.1007/978-3-642-11970-5_5
  * Myreen (2010) Magnus O. Myreen. 2010\.  Verified Just-in-Time Compiler on X86. In _Symposium on Principles of Programming Languages (POPL)_.  https://doi.org/10.1145/1706299.1706313
  * Ottoni (2018) Guilherme Ottoni. 2018\.  HHVM JIT: A Profile-Guided, Region-Based Compiler for PHP and Hack. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/3192366.3192374
  * Pelenitsyn et al. (2021a) Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, and Jan Vitek. 2021a.  Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation.  _Proc. ACM Program. Lang._ 5, OOPSLA, Article 150 (2021), 26 pages.  https://doi.org/10.1145/3485527
  * Pelenitsyn et al. (2021b) Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, and Jan Vitek. 2021b.  Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation (Artifact).  https://doi.org/10.5281/zenodo.5500548
  * Rigo (2004) Armin Rigo. 2004\.  Representation-Based Just-in-Time Specialization and the Psyco Prototype for Python. In _Partial Evaluation and Program Manipulation (PEPM)_.  https://doi.org/10.1145/1014007.1014010
  * Würthinger et al. (2012) Thomas Würthinger, Andreas Wöß, Lukas Stadler, Gilles Duboscq, Doug Simon, and Christian Wimmer. 2012.  Self-Optimizing AST Interpreters. In _Dynamic Language Symposium (DLS)_.  https://doi.org/10.1145/2384577.2384587
  * Xu et al. (2009) Guoqing Xu, Matthew Arnold, Nick Mitchell, Atanas Rountev, and Gary Sevitsky. 2009.  Go with the Flow: Profiling Copies to Find Runtime Bloat. In _Programming Language Design and Implementation (PLDI)_.  https://doi.org/10.1145/1542476.1542523
  * Zappa Nardelli et al. (2018) Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, and Jan Vitek. 2018.  Julia Subtyping: A Rational Reconstruction.  _Proc. ACM Program. Lang._ 2, OOPSLA (2018).  https://doi.org/10.1145/3276483

##  Appendix A Graphs for Sec. 5

This appendix contains graphs similar to the ones described in Sec. 5.3.1 for
all 10 packages discussed in Sec. 5. There are 6 graphs per package: the top
two show the relationship between the method size and stability (left) or
groundedness (right); the other four graphs connect the two type-related
properties with control-flow features: the number of gotos and the number of
returns in a method instance.

Note that the bottom four graphs for every package are different from the top
two in that they group method instances, not methods. Therefore, the bottom
four graphs have all data bins either at level $OY=0$ or $1$, because we
always know whether a method instance is stable (grounded) or not. The change
comes from the fact that the control-flow features in question depend on
compiled code and the way it was optimized: e. g., an if true in a method can
be optimized away during compilation.

###  A.1. Package: DifferentialEquations

Figure 12. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in DifferentialEquations

Figure 13. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in
DifferentialEquations

Figure 14. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in
DifferentialEquations

###  A.2. Package: Flux

Figure 15. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Flux

Figure 16. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Flux

Figure 17. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Flux

###  A.3. Package: Gadfly

Figure 18. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Gadfly

Figure 19. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Gadfly

Figure 20. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Gadfly

###  A.4. Package: Gen

Figure 21. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Gen

Figure 22. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Gen

Figure 23. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Gen

###  A.5. Package: Genie

Figure 24. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Genie

Figure 25. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Genie

Figure 26. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Genie

###  A.6. Package: IJulia

Figure 27. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in IJulia

Figure 28. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in IJulia

Figure 29. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in IJulia

###  A.7. Package: JuMP

Figure 30. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in JuMP

Figure 31. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in JuMP

Figure 32. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in JuMP

###  A.8. Package: Knet

Figure 33. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Knet

Figure 34. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Knet

Figure 35. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Knet

###  A.9. Package: Plots

Figure 36. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Plots

Figure 37. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Plots

Figure 38. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Plots

###  A.10. Package: Pluto

Figure 39. Stability (left, OY axis) and groundedness (right, OY) by method
size (OX)

Stability and groundedness by method size in Pluto

Figure 40. Stability (left, OY axis) and groundedness (right, OY) by number of
gotos in method instances (OX)

Stability and groundedness by number of goto’s in method instances in Pluto

Figure 41. Stability (left, OY axis) and groundedness (right, OY) by number of
returns in method instances (OX)

Stability and groundedness by number of returns in method instances in Pluto