# Triple hourglass Weyl phonons

Guang Liu  Department of Physics, Southern University of Science and
Technology, Shenzhen 518055, People’s Republic of China  Zhongjia Chen
Department of Physics, Southern University of Science and Technology, Shenzhen
518055, People’s Republic of China  Songshan Lake Materials Laboratory,
Dongguan, Guangdong 523808, People’s Republic of China  Peng Wu  Department of
Physics, Southern University of Science and Technology, Shenzhen 518055,
People’s Republic of China  Hu Xu<EMAIL_ADDRESS>Department of Physics,
Southern University of Science and Technology, Shenzhen 518055, People’s
Republic of China

###### Abstract

Unconventional Weyl phonons with higher topological charges in crystalline
solids have attracted increasing attention. By symmetry analysis and low-
energy $\emph{{k}}\cdot\emph{{p}}$ effective Hamiltonian, we propose the
symmetry enforced triple hourglass Weyl phonons (THWPs) with Chern number
$\mathcal{C}$ = $\pm$ 3 protected by $6_{3}$ screw rotation symmetry in chiral
space groups 173 ($P6_{3}$) and 182 ($P6_{3}22$). We take LiIO3 with space
group 173 as a candidate and confirm that it possesses THWP with linear and
quadratic dispersions along the $k_{z}$ direction and in the $k_{x}$-$k_{y}$
plane, respectively. Due to the constraints of crystal symmetry and
topological charge conservation, six equivalent single Weyl phonons (SWPs)
emerge and lie in the $k_{z}$ = 0 plane. Therefore, the unique phonon surface
arcs connect the projections of two THWPs and six SWPs, leading to nontrivial
sextuple-helicoid surface arcs on the (001) surface Brillouin zone. Our work
proposes a class of topological phonons and realizes it in realistic
materials, providing a perfect platform for experimental observation of THWPs.
We expect our work to provide a new idea for detection of unconventional
quasiparticles.

###### pacs:

73.20.At, 71.55.Ak, 74.43.-f

In recent years, various topological quasiparticles in three-dimensional (3D)
crystalline solids, such as Weyl pointsBurkov and Balents (2011); Fang et al.
(2012); Yuan et al. (2018), triple pointsPark et al. (2021); Zhang et al.
(2018); Miao et al. (2018), Dirac pointsYoung et al. (2012); Liu et al.
(2014); Armitage et al. (2018); Cai et al. (2020); Chen et al. (2021), nodal
linesKim et al. (2015); Yu et al. (2015); Jin et al. (2018); Liu et al.
(2021a), and nodal surfacesLiang et al. (2016); Wu et al. (2018); Wang et al.
(2021), etc., have attracted widespread attention because of their unique
physical properties and potential applications. Among them, Weyl-type
excitations are of particular importance, which are peculiar quasiparticle
excitations featuring nontrivial isolated point touching of two band branches.
Weyl fermions were first predicted theoretically in the magnetic pyrochlore
iridatesWan et al. (2011). However, due to the limitation of magnetic domains
of these magnetic materials, some typical physical properties of Weyl points
are difficult to be observed experimentallyZyuzin and Burkov (2012); Son and
Spivak (2013); Huang et al. (2015). Fortunately, non-magnetic materials with
well-defined surface states and Fermi arcs are later proposed and observed
experimentallyWeng et al. (2015); Lv et al. (2015a); Lu et al. (2015); Xu et
al. (2015); Lv et al. (2015b).

Fig. 1: (a) The schematics of a triple Weyl point with triple-helicoid surface
arcs. (b) The schematic of a pair of triple Weyl points connected by time-
reversal symmetry with sextuple-helicoid surface arcs. (c) The schematic of
the hourglass band dispersion on a $6_{3}$ invariant screw axis.

Motivated by these works, more works on Weyl-type excitations have been
reported. According to the band dispersion around crossing points which can
lead to exotic topological properties, the Weyl-type points exhibit a variety
of classification. For example, according to degree of the tilt of the local
dispersion around the crossing, Weyl points are divided into type-IYuan et al.
(2018); Wan et al. (2011); Weng et al. (2015); Lv et al. (2015a); Lu et al.
(2015); Xu et al. (2015); Lv et al. (2015b); Xia et al. (2019a), type-
IISoluyanov et al. (2015); Deng et al. (2016); Tamai et al. (2016); Yu et al.
(2016); Xia et al. (2019b); Jin et al. (2022), and type-III Weyl pointsZheng
et al. (2020); Li et al. (2021a); Ding et al. (2022). The latter two break the
Lorentz symmetry, resulting in unique transport properties different from
type-I Weyl points with normal point-like Fermi surfacesSoluyanov et al.
(2015); Deng et al. (2016); Tamai et al. (2016); Yu et al. (2016); Xia et al.
(2019b); Jin et al. (2022). In addition, the Weyl points, which act as
“source” or “sink” of Berry curvatureFang et al. (2003), are topologically
protected by the discrete translational symmetry of the lattice and no further
symmetries are needed for their existence. Therefore, the topology of Weyl
point can be defined by a quantized topological charge (i.e., the Chern number
$\mathcal{C}$ = $\pm$1), which is the flux of the Berry curvature passing
through a closed surface in momentum space. However, considering an additional
symmetry, there will exist some Weyl points with higher Chern number
$\mathcal{C}$Tsirkin et al. (2017); Chang et al. (2017); Wang et al. (2020);
Huang et al. (2020); Yu et al. (2022); Jin et al. (2021); Zhang et al. (2020);
Li et al. (2021b); Cui et al. (2021); Liu et al. (2021b). For example, a
fourfold or sixfold rotation symmetry can protects Weyl points with
$\mathcal{C}$=$\pm 2$Zhang et al. (2018); Tsirkin et al. (2017); Chang et al.
(2017); Wang et al. (2020); Huang et al. (2020), a sixfold rotation symmetry
can protects Weyl points with $\mathcal{C}$=$\pm 3$Fang et al. (2012); Yu et
al. (2022), and Weyl points with $\mathcal{C}$=$\pm 4$Zhang et al. (2020); Li
et al. (2021b); Cui et al. (2021); Liu et al. (2021b) can be realized when the
cubic symmetry is included in the presence of threefold screw rotational
symmetry. Under this convention, Weyl points are divided into single Weyl,
quadratic Weyl, triple Weyl, and charge-four Weyl points with
$\mathcal{C}$=$\pm 1$, $\pm 2$, $\pm 3$, and $\pm 4$, respectively.

Phonons can be a perfect platform for realization of these unconventional Weyl
points due to their particular device applications and the unique advantages
of whole frequency range observation. For example, quadratic Weyl phonons
(QWPs) can exist with other two equal single Weyl phonons (SWPs) in
$\alpha$-SiO2Wang et al. (2020). Unlike paired SWPs with opposite chiral
charges, the projection of QWP connects two SWPs by two surface arcs. More
importantly, such a combination does not violate the no-go theoremNielsen and
Ninomiya (1981a, b) and satisfies topological charge conservation. The charge-
four Weyl (CFW) point was proposed only in the spinless systemZhang et al.
(2020); Cui et al. (2021); Liu et al. (2021b), and the quadruple-helicoid
surface states are available. However, the studies focusing on topological
nontrivial triple Weyl phonons (TWPs) are still in its infancy, and the TWPs
with clearly visible surface states have so far not been realized in realistic
materials. As shown in Fig. 1(a), we propose the existence of the TWP with
exotic triple-helicoid surface states, which connect the projections of the
TWP and three SWPs. Interestingly, sextuple-helicoid surface states in Fig.
1(b) can be expected when two TWPs are connected by time-reversal symmetry
$\mathcal{T}$. However, the TWPs originate from the accidental degeneracies on
a C6 invariant line, and therefore we can not explicitly distinguish it from
SWPs and QWPs on the same path. Then a questions arises: _Is there some kind
of constraint that guarantees the existence of TWPs on high-symmetry lines
(HSLs)?_ The hourglass-shaped band structures, which may result in symmetry
enforced intersection, such as hourglass nodal points and nodal linesWang et
al. (2017a); Furusaki (2017); Wang et al. (2017b); Zheng et al. (2021); Chen
et al. (2022), would be a good choice to realize the TWPs. Therefore, a class
of exotic topological phase, i.e., the triple hourglass Weyl phonons (TWHPs),
can be expected.

Through $\emph{{k}}\cdot\emph{{p}}$ effective model analysis, we identified
all candidate space groups (SGs) capable of possessing TWPs, which are listed
in Table. S1 of the supplementary material (SM)See Supplemental Material for
the computational method and effective model analysis . On this basis, by
analyzing the evolution of the irreducible representations (IRs) on C6
invariant HSLs, we find that SGs 173 and 182 can host the THWPs with
$\mathcal{C}$ = $\pm$3 in our candidate SGs, which originates from the
different screw rotation degrees of the C6. Therefore, we divide the triple
Weyl phonons into general TWPs and THWPs. Taking LiIO3 as an example, we
confirm the nontrivial topological properties of THWPs and find it possesses
an unique sextuple-helicoid surface arcs on the (001) surface, which is
consistent with our prediction. It should be stressed that THWP are enforced
to appear by symmetry, and its hourglass band characteristics makes it easier
to be observed and detected.

To understand the properties of TWPs, the crossings of two phonon branches can
be described by a two-band $\emph{{k}}\cdot\emph{{p}}$ effective Hamiltonian,
namely

$\mathcal{H}(\emph{{k}})=d(\emph{{k}})\sigma_{+}+d^{*}(\emph{{k}})\sigma_{-}+f(\emph{{k}})\sigma_{z}$
(1)

where $\sigma_{x,y,z}$ are Pauli matrix, $\sigma_{\pm}=(\sigma_{x}\pm
i\sigma_{y})/2$, $d(\emph{{k}})$ represents a complex function, and
$f(\emph{{k}})$ represents a real function. As an illustration, we consider a
generic point $k$ on the $C_{6}$ invariant axis [$\Gamma$-Z $(0,0,w)$] of
hexagonal crystal system. Since [$C_{6z}$, $\mathcal{H}(\emph{{k}})$] = 0, the
band eigenstates at k can be simultaneously chosen as $C_{6z}$ eigenstates.
The little group can be generated by the screw rotation symmetry
$\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{u}{6}\\}$, changing the coordinates
of the lattice as

$\displaystyle\widetilde{C}_{6z}:(x,y,z)\rightarrow(\frac{1}{2}x-\frac{\sqrt{3}}{2}y,\frac{\sqrt{3}}{2}x+\frac{1}{2}y,z+\frac{u}{6}),$
(2)

where $u$ = 0, 1, 2, 3, 4, 5. Considering a general point located at the
$k_{z}$ axis (0,0,$w$). Then we can get the relation

$\widetilde{C}_{6z}^{6}=T_{00u}=e^{i2u\pi w}.$ (3)

Hence, the eigenvalues of $\widetilde{C}_{6z}$ can be expressed as

$E_{n}=\\{e^{in\pi/6}e^{i\pi uw/3},n=0,2,4,6,8,10\\},$ (4)

where $E_{n}$ can be used to indicate each phonon branch. When two phonon
branches with different eigenvalues cross on this $\widetilde{C}_{6z}$
invariant path, the matrix representation of $\widetilde{C}_{6z}$ can be
written as

$D(\widetilde{C}_{6z})=\left(\begin{array}[]{cc}E_{n_{1}}&\\\ &E_{n_{2}}\\\
\end{array}\right),$ (5)

where $n_{1}$/$n_{2}$ represents different $n$ in Eq. (4). According to the
invariant theory, the Hamiltonian of this crossing point can be expressed
under the constraint of $\widetilde{C}_{6z}$ invariant symmetry as

$D(\widetilde{C}_{6z})\mathcal{H}_{eff}(\emph{{k}})D^{-1}(\widetilde{C}_{6z})=\mathcal{H}_{eff}(R_{6z}\emph{{k}}),$
(6)

where $R_{6z}$ is a 3$\times$3 rotation matrix of $\widetilde{C}_{6z}$. There
exist three possibilities, leading to three types of Weyl point:

$E_{n_{1}}/E_{n_{2}}=e^{\pm i\pi/3},\mathcal{C}=\pm 1,$ (7)
$E_{n_{1}}/E_{n_{2}}=e^{\pm 2i\pi/3},\mathcal{C}=\pm 2,$ (8)
$E_{n_{1}}/E_{n_{2}}=-1,\mathcal{C}=\pm 3.$ (9)

Under the constraint of Eqs. (6) and (9), the crossing point would be a triple
Weyl point, and the corresponding Hamiltonian can be expressed as

$\mathcal{H}_{eff}(\emph{{k}})=\left(\begin{array}[]{cc}f(\emph{{k}})&d(\emph{{k}})\\\
d^{*}(\emph{{k}})&-f(\emph{{k}})\\\ \end{array}\right),$ (10)

where $f(\emph{{k}})$ = $a_{1}(k_{x}^{2}+k_{y}^{2})+a_{2}k_{z}$,
$d(\emph{{k}})$ = $\alpha_{1}k_{+}^{3}+\alpha_{2}k_{-}^{3}$, $a_{1,2}$ are
real parameters, $\alpha_{1,2}$ are complex parameters, and $k_{\pm}=k_{x}\pm
ik_{y}$. In this low-energy effective Hamiltonian, the topological charge of
the crossing point is characterized by the leading order of the chiral term
[i.e., the antidiagonal term]. Besides, the in-plane cubic dispersion
originating from the the chiral term is suppressed by the in-plane quadratic
dispersion of the nonchiral term [i.e., diagonal term], so the triple Weyl
point possesses the in-plane [$k_{x}$-$k_{y}$] quadratic dispersion in a
spinless system.

Table 1: IRs of $C_{6}$ with different screw rotation degrees at high symmetry points (HSPs) $\Gamma$ and A, where $u$ represents screw rotation degree. $R_{1}$, $R_{2}$, $R_{3}$, $R_{4}$, $R_{5}$, and $R_{6}$ represent different IRs corresponding to $n$ = 0, 2, 4, 6, 8, and 10 in Eq. (4), respectively.  Degree | HSP | $R_{1}$ | $R_{2}$ | $R_{3}$ | $R_{4}$ | $R_{5}$ | $R_{6}$ | 2D IRs | Triple Weyl on $\Gamma$-A
---|---|---|---|---|---|---|---|---|---
$u$=0 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$
$u$=1 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | $e^{i\pi/6}$ | i | $e^{5i\pi/6}$ | $e^{-5i\pi/6}$ | -i | $e^{-i\pi/6}$ |  $R_{1,6}$,$R_{2,5}$ ,$R_{3,4}$
$u$=2 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ | 1 |  $R_{1,5}$,$R_{2,4}$
$u$=3 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | i | $e^{5i\pi/6}$ | $e^{-5i\pi/6}$ | -i | $e^{-i\pi/6}$ | $e^{i\pi/6}$ |  $R_{1,4}$,$R_{2,3}$,$R_{5,6}$
$u$=4 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ | 1 | $e^{i\pi/3}$ |  $R_{1,3}$,$R_{4,6}$
$u$=5 | $\Gamma$ | 1 | $e^{i\pi/3}$ | $e^{2i\pi/3}$ | -1 | $e^{-2i\pi/3}$ | $e^{-i\pi/3}$ |  $R_{2,6}$,$R_{3,5}$ | $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$
A | $e^{5i\pi/6}$ | $e^{-5i\pi/6}$ | -i | $e^{-i\pi/6}$ | $e^{i\pi/6}$ | i |  $R_{1,2}$,$R_{3,6}$,$R_{4,5}$

Based on the symmetry analysis above, we list the operation eigenvalues of the
C6 screw rotation operation at high symmetry points (HSPs) $\Gamma$ and A in
Table I. Under the action of time-reversal symmetry, two one-dimensional (1D)
IRs can form a two-dimensional (2D) IR. For example, when $u$ = 0 at $\Gamma$,
$R_{2,6}=R_{2}\oplus R_{6}$. In Table I, we list all 2D IRs at high symmetry
$\Gamma$ and A points, respectively. Then we consider the evolution of two
sets of 2D IRs along the HSL $\Gamma$-A. The two sets of 2D IRs will split
into four 1D IRs along $\Gamma$-A. When the screw rotation $6_{3}$ [i.e.,
$\widetilde{C}_{6z}$ with $u$ = 3] is presented, interesting things happen. As
shown in Fig. 1(c), two sets of 2D IRs $R_{2,6}$ and $R_{3,5}$ at $\Gamma$
split into four 1D IRs $R_{2}$, $R_{6}$, $R_{3}$, and $R_{5}$ along
$\Gamma$-A, then form two 2D IRs $R_{2,3}$ and $R_{5,6}$ at A. According to
the compatibility relations, there must a crossing with $\mathcal{C}$ = $\pm
3$ between $R_{3}$ and $R_{6}$. In contrast to the general triple Weyl phonon,
this crossing is enforced by $6_{3}$ screw rotation symmetry and has a
hourglass type band dispersion structure, which is the THWP. Interestingly,
the topological charge of the THWP can be obtained explicitly from the band
dispersion without further calculations. In addition, we find that only SGs
173 and 182 satisfy such a symmetry requirement.

Fig. 2: The crystal structure and phonon band of LiIO3.(a) The primitive cell.
(b) The bulk BZ and the corresponding (001) surface BZ. (c) Phonon spectrum.
(d) Phonon dispersions along $\Gamma$-A contributed from phonon branches 25 to
28, which corresponding to the red box in (c). (e) Three-dimensional
representation of the phonon dispersion on the $k_{x}$-$k_{y}$ plane of the
crossing point in (d).

Lithium carbonate ($\alpha$-LiIO3) is an ideal candidate to realize the
symmetry enforced THWPs, which is synthesized by reagent grade iodic acid and
lithium carbonate dissolved in waterRosenzweig and Morosin (1966). As shown in
Fig. 2(a), the SG of $\alpha$-LiIO3 is 173 ($P6_{3}$), in which a primitive
cell contains two Li, two I, and six O atoms. The bulk Brillouin zone (BZ),
the projected (001) surface BZ of $\alpha$-LiIO3 and the corresponding HSPs
are shown in Fig. 2(b). As shown in Fig. 2(c), we plot the phonon band
structure with non-analytic term correction for $\alpha$-LiIO3. We focus on
the non-trivial hourglass crossing on the C6 invariant axis, which corresponds
to the THWP. We find that the hourglass crossing contributed from the phonon
branches 25 to 28 is an ideal selection. As shown in Fig. 2(d), the THWP has a
typical linear dispersion characteristic along the $k_{z}$ direction. We also
plot the corresponding 3D representation of the crossing branches in the
$k_{x}$-$k_{y}$ plane. It is clear that the crossing point possesses quadratic
in-plane dispersion in Fig. 2(e), which is consistent with our model analysis.

Fig. 3: (a) The distribution of the THWP (red dots) and SWPs (blue dots) in
momentum space. (b) The phase difference evolution of $C_{6}$ rotation
operation eigenvalues contributed by two phonon branches 26 and 27 along
$\Gamma$-A. (c) The distribution of Berry curvature in the $k_{x}$-$k_{y}$
plane. $\overline{\Gamma}$ \- $\overline{\textrm{M}}$ \-
$\overline{\textrm{V}}$ represents a (001) surface path through the
projections of THWPs and SWPs .

We also find six SWPs contributed from 26 and 27 phonon branches at the
$k_{z}$ = 0 plane, and the schematic diagram about the momentum positions of
two THWPs and six SWPs in the first BZ are shown in Fig. 3(a). Under the
rotation of $C_{6}$ symmetry operator, these six SWPs are equivalent, and
first-principles calculations show that their Chern number are +1. According
to the no-go theorem, we can also infer that the Chern numbers of the two
THWPs along the $k_{z}$-axis are -3. The momentum positions and more detailed
information about these nodes are presented in Table S2 of the SM.

Furthermore, in order to explicitly obtain the chirality of THWP, we study the
phase difference [i.e., $3/\pi*arg(E_{n_{1}}/E_{n_{2}})$] evolution of the
$C_{6}$ eigenvalues of two phonon branches in Fig. 3(b). We find that there
exists a phase change at the $\overline{k}$ point, confirming the existence of
a THWP with $\mathcal{C}$ = -3. We next examine the distribution of Berry
curvature contributed by the 26th and 27th phonon branches in the
$k_{x}$-$k_{y}$ plane. As shown in Fig. 3(c), the Berry curvature near
topological nontrivial points shows convergent and divergent field morphology,
which correspond to the chirality of THWPs and SWPs, respectively.

Fig. 4: (a)The phonon LDOS projected on the (001) surface BZ along
$\overline{\textrm{V}}$ \- $\overline{\Gamma}$ \- $\overline{\textrm{M}}$ \-
$\overline{\textrm{V}}$. (b) The isofrequency contours of (001) surface and
(c) its corresponding enlarged view of the middle part at 21.37 THz, where
$W_{1}$ and $W_{2}$ represent the projection of THWPs and SWPs, respectively.
(d) The phonon LDOS projected on the semi-infinite (001) surface BZ along the
loop $C_{1}$.

To illustrate the exotic topological features of THWPs, we calculate the
phonon local density of states (LDOS) and projected isofrequency surface
contours on the (001) surface. The phonon surface states, which start at the
projection of the THWPs at $\overline{\Gamma}$ and end at the projection of
SWPs locating at $\overline{\Gamma}$-$\overline{\textrm{V}}$, are clearly
visible in Fig. 4(a). Moreover, the (001) surface states further display
quadratic dispersions of the THWPs, showing consistency with the 3D phonon
dispersion in Fig. 2(e). As shown in Fig. 4(b), two THWPs located at
$\Gamma$-A are projected into the center of the surface BZ [denoted by
$W_{1}$], forming a terminal point with total $\mathcal{C}$ = -6, while the
other six SWPs are projected into the internal general point of the surface BZ
[denoted by $W_{2}$] with $\mathcal{C}$ = +1. We can further determine that
the six non-trivial terminal points corresponding to six SWPs in the
isofrequency surface contours with $\omega$ = 21.37 THz in Fig. 4(b). And we
can see that six branches of surface arcs start at $W_{2}$, and finally
converge at $W_{1}$. These long surface arcs that connect $W_{1}$ and $W_{2}$
exhibit a sextuple-helicoid nature. Unlike the QWPs that usually accompanies
the double-helicoid surface state, each THWP induces the simultaneous
appearance of three other SWPs, forming the triple-helicoid surface arc
structure. The THWPs can only appear on the $C_{6}$ invariant axis, and its
(001) projection is a superposition of two THWPs. Therefore, we can see
sextuple-helicoid surface states, which is in perfect agreement with our
theoretical prediction. To visualize the helicoidal surface states, we
calculate the surface LDOS along one clockwise loops $C_{1}$ [see Fig. 4(c)]
in Fig. 4(d). For the loop $C_{1}$, the six leftmoving chiral edge modes are
consistent with the chirality of $W_{1}$, further confirming our results.

In summary, we present a class of symmetry enforced THWP with unique
topological properties, which is protected by $6_{3}$ screw rotation symmetry
in chiral SGs 173 and 182. Our work uncovers all THWPs in the spinless system
and proposes that their nontrivial surface states connect a THWP with
$\mathcal{C}=\pm 3$ and three SWPs with $\mathcal{C}=\mp 1$. In addition, we
provide an ideal candidate which possesses two THWPs locating at $C_{6}$
invariant line and six SWPs locating at the $k_{z}=0$ plane, leading to
sextuple-helicoid surface arcs. The multiple surface arcs can provide one-way
phonon propagation channels, suggesting potential applications in topological
phonon devices. Our work not only proposes a class of quasiparticles but also
provides an idea for detection of unconventional quasiparticles in realistic
materials.

This work is supported by the National Key R&D Program of China (Grant No.
2022YFA1403700), the National Natural Science Foundation of China (Grant No.
11974160), the Science, Technology, and Innovation Commission of Shenzhen
Municipality (Grant No. RCYX20200714114523069), and the Center for
Computational Science and Engineering at Southern University of Science and
Technology.

Note added. $-$Recently, we became aware of a similar work by Wang et al.Wu et
al. (2021).

## References

  * Burkov and Balents (2011) A. A. Burkov and L. Balents, Phys. Rev. Lett. 107, 127205 (2011).
  * Fang et al. (2012) C. Fang, M. J. Gilbert, X. Dai, and B. A. Bernevig, Phys. Rev. Lett. 108, 266802 (2012).
  * Yuan et al. (2018) X. Yuan, Z. Yan, C. Song, M. Zhang, Z. Li, C. Zhang, Y. Liu, W. Wang, M. Zhao, Z. Lin, et al., Nat. Commun. 9, 1854 (2018).
  * Park et al. (2021) S. Park, Y. Hwang, H. C. Choi, and B. J. Yang, Nat. Commu. 12, 6781 (2021).
  * Zhang et al. (2018) T. Zhang, Z. Song, A. Alexandradinata, H. Weng, C. Fang, L. Lu, and Z. Fang, Phys. Rev. Lett. 120, 016401 (2018).
  * Miao et al. (2018) H. Miao, T. T. Zhang, L. Wang, D. Meyers, A. H. Said, Y. L. Wang, Y. G. Shi, H. M. Weng, Z. Fang, and M. P. M. Dean, Phys. Rev. Lett. 121, 035302 (2018).
  * Young et al. (2012) S. M. Young, S. Zaheer, J. C. Y. Teo, C. L. Kane, E. J. Mele, and A. M. Rappe, Phys. Rev. Lett. 108, 140405 (2012).
  * Liu et al. (2014) Z. K. Liu, B. Zhou, Y. Zhang, Z. J. Wang, H. M. Weng, D. Prabhakaran, S. K. Mo, Z. X. Shen, Z. Fang, X. Dai, et al., Science 343, 864 (2014).
  * Armitage et al. (2018) N. P. Armitage, E. J. Mele, and A. Vishwanath, Rev. Mod. Phys. 90, 015001 (2018).
  * Cai et al. (2020) X. Cai, L. Ye, C. Qiu, M. Xiao, R. Yu, M. Ke, and Z. Liu, Light: Sci. Appl. 9, 38 (2020).
  * Chen et al. (2021) Z. J. Chen, R. Wang, B. W. Xia, B. B. Zheng, Y. J. Jin, Y. J. Zhao, and H. Xu, Phys. Rev. Lett. 126, 185301 (2021).
  * Kim et al. (2015) Y. Kim, B. J. Wieder, C. L. Kane, and A. M. Rappe, Phys. Rev. Lett. 115, 036806 (2015).
  * Yu et al. (2015) R. Yu, H. Weng, Z. Fang, X. Dai, and X. Hu, Phys. Rev. Lett. 115, 036807 (2015).
  * Jin et al. (2018) Y. J. Jin, Z. J. Chen, B. W. Xia, Y. J. Zhao, R. Wang, and H. Xu, Phys. Rev. B 98, 220103 (2018).
  * Liu et al. (2021a) G. Liu, Y. Jin, Z. Chen, and H. Xu, Phys. Rev. B 104, 024304 (2021a).
  * Liang et al. (2016) Q. F. Liang, J. Zhou, R. Yu, Z. Wang, and H. Weng, Phys. Rev. B 93, 085427 (2016).
  * Wu et al. (2018) W. Wu, Y. Liu, S. Li, C. Zhong, Z. M. Yu, X. L. Sheng, Y. X. Zhao, and S. A. Yang, Phys. Rev. B 97, 115125 (2018).
  * Wang et al. (2021) X. Wang, F. Zhou, T. Yang, M. Kuang, Z. M. Yu, and G. Zhang, Phys. Rev. B 104, L041104 (2021).
  * Wan et al. (2011) X. Wan, A. M. Turner, A. Vishwanath, and S. Y. Savrasov, Phys. Rev. B 83, 205101 (2011).
  * Zyuzin and Burkov (2012) A. A. Zyuzin and A. A. Burkov, Phys. Rev. B 86, 115133 (2012).
  * Son and Spivak (2013) D. T. Son and B. Z. Spivak, Phys. Rev. B 88, 104412 (2013).
  * Huang et al. (2015) X. Huang, L. Zhao, Y. Long, P. Wang, D. Chen, Z. Yang, H. Liang, M. Xue, H. Weng, Z. Fang, et al., Phys. Rev. X 5, 031023 (2015).
  * Weng et al. (2015) H. Weng, C. Fang, Z. Fang, B. A. Bernevig, and X. Dai, Phys. Rev. X 5, 011029 (2015).
  * Lv et al. (2015a) B. Q. Lv, H. M. Weng, B. B. Fu, X. P. Wang, H. Miao, J. Ma, P. Richard, X. C. Huang, L. X. Zhao, G. F. Chen, et al., Phys. Rev. X 5, 031013 (2015a).
  * Lu et al. (2015) L. Lu, Z. Wang, D. Ye, L. Ran, L. Fu, J. D. Joannopoulos, and M. Solja$\check{\textrm{c}}$i$\acute{\textrm{c}}$, Science 349, 622 (2015).
  * Xu et al. (2015) S. Y. Xu, I. Belopolski, N. Alidoust, M. Neupane, G. Bian, C. Zhang, R. Sankar, G. Chang, Z. Yuan, C. C. Lee, et al., Science 349, 613 (2015).
  * Lv et al. (2015b) B. Q. Lv, N. Xu, H. M. Weng, J. Z. Ma, P. Richard, X. C. Huang, L. X. Zhao, G. F. Chen, C. E. Matt, F. Bisti, et al., Nat. Phys. 11, 724 (2015b).
  * Xia et al. (2019a) B. W. Xia, Y. J. Jin, J. Z. Zhao, Z. J. Chen, B. B. Zheng, Y. J. Zhao, R. Wang, and H. Xu, Phys. Rev. Lett. 122, 057205 (2019a).
  * Soluyanov et al. (2015) A. A. Soluyanov, D. Gresch, Z. Wang, Q. Wu, M. Troyer, X. Dai, and B. A. Bernevig, Nature 527, 495 (2015).
  * Deng et al. (2016) K. Deng, G. Wan, P. Deng, K. Zhang, S. Ding, E. Wang, M. Yan, H. Huang, H. Zhang, Z. Xu, et al., Nat. Phys. 12, 1105 (2016).
  * Tamai et al. (2016) A. Tamai, Q. S. Wu, I. Cucchi, F. Y. Bruno, S. Riccò, T. K. Kim, M. Hoesch, C. Barreteau, E. Giannini, C. Besnard, et al., Phys. Rev. X 6, 031021 (2016).
  * Yu et al. (2016) Z. M. Yu, Y. Yao, and S. A. Yang, Phys. Rev. Lett. 117, 077202 (2016).
  * Xia et al. (2019b) B. W. Xia, R. Wang, Z. J. Chen, Y. J. Zhao, and H. Xu, Phys. Rev. Lett. 123, 065501 (2019b).
  * Jin et al. (2022) Y. J. Jin, Y. Xu, Z. J. Chen, and H. Xu, Phys. Rev. B 105, 035141 (2022).
  * Zheng et al. (2020) B. Zheng, B. Xia, R. Wang, Z. Chen, J. Zhao, Y. Zhao, and H. Xu, Phys. Rev. B 101, 100303 (2020).
  * Li et al. (2021a) X. P. Li, K. Deng, B. Fu, Y. Li, D. S. Ma, J. Han, J. Zhou, S. Zhou, and Y. Yao, Phys. Rev. B 103, L081402 (2021a).
  * Ding et al. (2022) G. Ding, F. Zhou, Z. Zhang, Z. M. Yu, and X. Wang, Phys. Rev. B 105, 134303 (2022).
  * Fang et al. (2003) Z. Fang, N. Nagaosa, K. S. Takahashi, A. Asamitsu, R. Mathieu, T. Ogasawara, H. Yamada, M. Kawasaki, Y. Tokura, and K. Terakura, Science 302, 92 (2003).
  * Tsirkin et al. (2017) S. S. Tsirkin, I. Souza, and D. Vanderbilt, Phys. Rev. B 96, 045102 (2017).
  * Chang et al. (2017) M. L. Chang, M. Xiao, W. J. Chen, and C. T. Chan, Phys. Rev. B 95, 125136 (2017).
  * Wang et al. (2020) R. Wang, B. W. Xia, Z. J. Chen, B. B. Zheng, Y. J. Zhao, and H. Xu, Phys. Rev. Lett. 124, 105303 (2020).
  * Huang et al. (2020) Z. Huang, Z. Chen, B. Zheng, and H. Xu, npj Comput. Mater. 6, 87 (2020).
  * Yu et al. (2022) Z. M. Yu, Z. Zhang, G. B. Liu, W. Wu, X. P. Li, R. W. Zhang, S. A. Yang, and Y. Yao, Sci. Bull. 67, 375 (2022).
  * Jin et al. (2021) Y. J. Jin, Z. J. Chen, X. L. Xiao, and H. Xu, Phys. Rev. B 103, 104101 (2021).
  * Zhang et al. (2020) T. Zhang, R. Takahashi, C. Fang, and S. Murakami, Phys. Rev. B 102, 125148 (2020).
  * Cui et al. (2021) C. Cui, X. P. Li, D. S. Ma, Z. M. Yu, and Y. Yao, Phys. Rev. B 104, 075115 (2021).
  * Liu et al. (2021b) Q. B. Liu, Z. Wang, and H. H. Fu, Phys. Rev. B 103, L161303 (2021b).
  * Li et al. (2021b) H. Li, T. Zhang, A. Said, Y. Fu, G. Fabbris, D. G. Mazzone, J. Zhang, J. Lapano, H. N. Lee, H. C. Lei, et al., Phys. Rev. B 103, 184301 (2021b).
  * Nielsen and Ninomiya (1981a) H. Nielsen and M. Ninomiya, Nucl. Phys. B 185, 20 (1981a).
  * Nielsen and Ninomiya (1981b) H. Nielsen and M. Ninomiya, Nucl. Phys. B 193, 173 (1981b).
  * Wang et al. (2017a) L. Wang, S. K. Jian, and H. Yao, Phys. Rev. B 96, 075110 (2017a).
  * Furusaki (2017) A. Furusaki, Sci. Bull. 62, 788 (2017), ISSN 2095-9273.
  * Wang et al. (2017b) S. S. Wang, Y. Liu, Z. M. Yu, X. L. Sheng, and S. A. Yang, Nat. Commun. 8, 1844 (2017b).
  * Zheng et al. (2021) B. Zheng, F. Zhan, X. Wu, R. Wang, and J. Fan, Phys. Rev. B 104, L060301 (2021).
  * Chen et al. (2022) Z. J. Chen, Z. J. Xie, Y. J. Jin, G. Liu, and H. Xu, Phys. Rev. Mater. 6, 034202 (2022).
  * (56) See Supplemental Material for the computational method, momentum positions of triple hourglass Weyl point, and the results of CaTa4O11 (space group 182), which includes Refs. [59-68].
  * Rosenzweig and Morosin (1966) A. Rosenzweig and B. Morosin, Acta Crystallogr. 20, 758 (1966).
  * Wu et al. (2021) X. T. Wang, F. Zhou, Z. Y. Zhang, Z. M. Yu and Y. G. Yao, arXiv: 2209.08592v1.
  * Kohn and Sham (1965) W. Kohn and L. J. Sham, Phys. Rev. 140, A1133 (1965).
  * Kresse and Furthmüller (1996) G. Kresse and J. Furthmüller, Phys. Rev. B 54, 11169 (1996).
  * Kresse and Furthmüller (1996) G. Kresse and J. Furthmüller, Comp. Mater. Sci. 6, 15 (1996).
  * Perdew et al. (1996) J. P. Perdew, K. Burke, and M. Ernzerhof, Phys. Rev. Lett. 77, 3865 (1996).
  * Kresse and Joubert (1999) G. Kresse and D. Joubert, Phys. Rev. B 59, 1758 (1999).
  * Ceperley and Alder (1980) D. M. Ceperley and B. J. Alder, Phys. Rev. Lett. 45, 566 (1980).
  * Togo and Tanaka (2015) A. Togo and I. Tanaka, Scripta Mater. 108, 1 (2015).
  * Wu et al. (2018) Q. Wu, S. Zhang, H. F. Song, M. Troyer, and A. A. Soluyanov, Comput. Phys. Commun. 224, 405 (2018).
  * Sancho et al. (1984) M. P. L. Sancho, J. M. L. Sancho, and J. Rubio, J. Phys. F: Met. Phys. 14, 1205 (1984).
  * Jahnberg (1970) L. Jahnberg, J. Solid State Chem. 1, 454 (1970).

Supplemental Material for

“Triple Hourglass Weyl phonons”

A. Calculation methods

The calculations for the realistic materials were based on the framework of
density functional theory (DFT) Kohn and Sham (1965) using the Vienna _ab-
initio_ Simulation Package (VASP) Kresse and Furthmüller (1996); Kresse and
Furthmüller (1996). The generalized gradient approximation (GGA) with the
Perdew-Burke-Ernzerhof revised for solids (PBE-sol) formalism was employed for
the exchange-correlation function Perdew et al. (1996). The projector
augmented wave method was employed to treat core-valence interactionsKresse
and Joubert (1999); Ceperley and Alder (1980). For all calculations, the
energy and force convergence criteria were set to be $10^{-7}$ eV and
$10^{-3}$ eV/A, respectively. The plane-wave expansion was truncated with a
cutoff energy of 520 eV, and the full Brillouin zone (BZ) was sampled by
$8\times 8\times 8$ Monkhorst-Pack grid. For phonon spectra calculations, we
used the PHONOPY code to construct the force constant matrices and generate
the symmetry information Togo and Tanaka (2015). The finite displacement
method was used to generate interatomic force constants in a $5\times 5\times
2$ supercell. In order to calculate the phonon surface states, we constricted
the tight-binding model Hamiltonian using the WannierTools package Wu et al.
(2018) combined with the iterative Green function method Sancho et al. (1984).

B. The summary of space groups with triple Weyl phonons

Table S1: The complete list of the triple Weyl phonons (TWPs) in 230 SGs. The first columns indicate the space group (SG) number and symbol, and the second column indicates the corresponding momentum location. The third column show the corresponding irreducible representations. The fourth column shows the generators of the k line. SG |  Location |  IRs |  Generator
---|---|---|---
168($P6$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|000\\}$
169($P6_{1}$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{1}{6}\\}$
170($P6_{5}$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{5}{6}\\}$
171($P6_{2}$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{2}{6}\\}$
172($P6_{4}$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{4}{6}\\}$
173($P6_{3}$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{3}{6}\\}$
177($P622$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|000\\}$
178($P6_{1}22$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{1}{6}\\}$
179($P6_{5}22$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{5}{6}\\}$
180($P6_{2}22$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{2}{6}\\}$
181($P6_{4}22$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{4}{6}\\}$
182($P6_{3}22$) |  $\Gamma-\textrm{A}$ |  $R_{1}R_{4}/R_{2}R_{5}/R_{3}R_{6}$ |  $\widetilde{C}_{6z}\equiv\\{C_{6z}|00\frac{3}{6}\\}$

C. The momentum positions and more detailed information about THWPs and WPs in
LiIO3

In this section, Fig. S1 shows the related atom vibration of LiIO3. Table S2
shows the momentum positions and more detailed information about THWPs and WPs
in LiIO3. Fig. S2 shows the (100) surface states and surface arcs of LiIO3.

Fig. S1: The related displacements from the phonon branches 26 (a,c,e,f) and 27 (b,d,f,h) at $\Gamma$, M, K, and A, respectively. The length of the arrow represents the relative magnitude of the vibration.  Fig. S2: (a)The bulk BZ and the corresponding (100) surface BZ. (b) The phonon LDOS projected on the (100) surface. (c) The isofrequency isofrequency contours of (100) surface at 21.37 THz.  Table S2:  Phonon band index, positions, Chern number, and Multiplicity of the WPs in LiIO3. Phonon branchs | Momentum position | $\mathcal{C}$ | Multiplicity
---|---|---|---
26-27 | ( 0.00000000 0.00000000 0.05243162) | -3 | 2
26-27 | ( 0.00000000 0.00000000 -0.05243162) | -3 | 2
26-27 | ( 0.07186095 0.16722398 0.00000000) | 1 | 6
26-27 | ( -0.16722398 0.23908493 0.00000000) | 1 | 6
26-27 | ( 0.23908493 -0.07186095 0.00000000) | 1 | 6
26-27 | ( -0.23908493 0.07186095 0.00000000) | 1 | 6
26-27 | ( -0.07186095 -0.16722398 0.00000000) | 1 | 6
26-27 | ( 0.16722398 -0.23908493 0.00000000) | 1 | 6

D. The THWPs of the candidate CaTa4O11 crystallized in SG 182

As shown in Fig. S3(a), CaTa4O11 crystallizes in a hexagonal lattice with
nonsymmorphic space group $P6_{2}22$ (No. 182). In our calculations, the
relaxed lattice constants of CaTa4O11 are a = 6.2007 A and c = 12.3232 A,
which agree well with the experimental values a = 6.213, and c = 12.265
Jahnberg (1970).The hexagonal bulk BZ and its corresponding (001) surface BZs
are given in Fig. S3(b). The phonon dispersion curves along the high-symmetry
directions are illustrated in Fig. S3(c). The enlarged views of the THWP are
shown in Fig. S3(d). The phonon local density of states (LDOS) and projected
isofrequency surface contours on (001) surface are shown Fig. S3(e). We can
see that the phonon surface states connect the projections of the THWP and
single WPs in the first BZ. These phonon surface states confirm the nontrivial
phonon topology of THWPs in CaTa4O11. The momentum positions and more detailed
information about these nodes are presented in Table S3.

Table S3:  Phonon band index, positions, Chern number, and Multiplicity of the WPs in CaTa4O11. Phonon branchs | Momentum position | $\mathcal{C}$ | Multiplicity
---|---|---|---
40-41 | ( 0.00000000 0.00000000 0.33108401) | -3 | 2
40-41 | ( 0.00000000 0.00000000 -0.33108401) | -3 | 2
40-41 | ( 0.27203327 0.27203327 0.00000000) | 1 | 6
40-41 | ( 0.27203327 -0.54406654 0.00000000) | 1 | 6
40-41 | ( -0.27203327 -0.27203327 0.00000000) | 1 | 6
40-41 | ( -0.54406654 0.27203327 0.00000000) | 1 | 6
40-41 | ( -0.27203327 0.54406654 0.00000000) | 1 | 6
40-41 | ( -0.54406654 -0.27203327 0.00000000) | 1 | 6
Fig. S3: (a) The primitive cell of CaTa4O11 with SG 182. (b) The bulk BZ and
the corresponding (001) surface BZ. (c) Phonon spectrum. (d) Phonon
dispersions along $\Gamma$-A contributed from phonon branches 39 to 42, which
corresponding to the red box in (c). (e) The phonon LDOS projected on the
(001) surface BZ along $\overline{\textrm{K}}$ \- $\overline{\Gamma}$ \-
$\overline{\textrm{K}}$.


${\mathit{C_{{\mathrm{1}}}}}$${\mathit{C^{\prime}_{{\mathrm{1}}}}}$${\mathit{C_{{\mathrm{2}}}}}$${\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})}$${\mathit{C^{\prime\prime}_{{\mathrm{1}}}}}$$\scriptstyle{R}$$\scriptstyle{A_{\tau}}$$\scriptstyle{R}$$\scriptstyle{R}$$\scriptstyle{\tau}$$\scriptstyle{A_{\tau}}$

Let us first show that the reductions of $\mathit{C_{{\mathrm{2}}}}$ can be
matched by $\mathit{C_{{\mathrm{1}}}}$. The only possible reduction from
$\mathit{C_{{\mathrm{2}}}}$, given our assumptions, is
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})$.
We claim that the empty reduction sequence from $\mathit{C_{{\mathrm{1}}}}$
matches it, that is, that
$(\mathit{C_{{\mathrm{1}}}},\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*}))\in
R$. By definition of $R$, this goal means that $\mathit{C_{{\mathrm{1}}}}$ and
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]$
are bisimilar in $\mathit{P_{{\mathrm{1}}}}$. But the latter configuration is
the same as
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}}[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}],\xi,\tilde{\xi}^{*})$,
which is bisimilar to $\mathit{C_{{\mathrm{2}}}}$ by the invariant of
assumption transparency, and thus to $\mathit{C_{{\mathrm{1}}}}$ by
transitivity. Conversely, we show that the reductions of
$\mathit{C_{{\mathrm{1}}}}$ can be matched by $\mathit{C_{{\mathrm{2}}}}$.
Suppose a reduction
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$.
The configuration
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]$
is bisimilar to $\mathit{C_{{\mathrm{1}}}}$ (same reasoning as in the previous
paragraph), so there is a matching state
$\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$ such that
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})[\mathit{P_{{\mathrm{2}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{1}}}}]\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$
in $\mathit{P_{{\mathrm{1}}}}$ with
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime\prime}_{{\mathrm{1}}}})\in
R_{\mathit{P_{{\mathrm{1}}}}}$. We can transpose this reduction in
$\mathit{P_{{\mathrm{2}}}}$:
$\mathsf{deoptimize}(\mathit{C_{{\mathrm{2}}}},\xi,\tilde{\xi}^{*})\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$
in $\mathit{P_{{\mathrm{2}}}}$, and thus
$\mathit{C_{{\mathrm{2}}}}\overset{~{}\mathit{A}_{\tau}\phantom{*}}{\longrightarrow^{\smash{\mkern-2.0mu*}}}\mathit{C^{\prime\prime}_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$.
This matches the reduction of $\mathit{C_{{\mathrm{1}}}}$, given that our
assumption
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime\prime}_{{\mathrm{1}}}})\in
R_{\mathit{P_{{\mathrm{1}}}}}$ exactly means that
$(\mathit{C^{\prime}_{{\mathrm{1}}}},\mathit{C^{\prime\prime}_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}])\in
R$. ∎

##  6\. Optimization Correctness

The proofs of the optimizations from Section 4 are easier than the proofs for
deoptimization invariants in the previous section (although, as program
transformations, they seem more elaborate). This comes from the fact that the
classical optimizations rewrite an existing version and interact little with
deoptimization.

###  6.1. Constant Propagation

We say that given a version $\mathit{V}$, a _static environment_ $SE$ for
label $\mathit{L}$ maps a subset of the variables in scope at $\mathit{L}$ to
values. A static environment is _valid_ , written $SE\vDash\mathit{L}$, if for
any configuration $\mathit{C}$ over $\mathit{L}$ reachable from the start of
$\mathit{V}$ we have that $SE$ is a subset of the lexical environment
$\mathit{E}$. Constant propagation can use a classic work-queue data-flow
algorithm to compute a valid static environment $SE$ at each label
$\mathit{L}$. It then replaces, in the instruction at $\mathit{L}$, each
expression or simple expression that can be evaluated in $SE$ by its value.
This is speculative since assumption predicates of the form
$\mathit{x}=\mathit{lit}$ populate the static environment with the binding
$\mathit{x}\rightarrow\mathit{lit}$.

###### Lemma 6.1.

For any version $\mathit{V_{{\mathrm{1}}}}$, let $\mathit{V_{{\mathrm{2}}}}$
be the result of constant propagation. $\mathit{V_{{\mathrm{1}}}}$ and
$\mathit{V_{{\mathrm{2}}}}$ are bisimilar.

###### Proof.

The relation $R$ to use here for bisimulation is the one that relates each
reachable $\mathit{C_{{\mathrm{1}}}}$ in
$\mathsf{reachable}(\mathit{P_{{\mathrm{1}}}})$ to the corresponding state
$\mathit{C_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{C_{{\mathrm{1}}}}[\mathit{V_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{V_{{\mathrm{2}}}}]$
in $\mathsf{reachable}(\mathit{P_{{\mathrm{2}}}})$. Consider two related
$\mathit{C_{{\mathrm{1}}}},\mathit{C_{{\mathrm{2}}}}$ over $\mathit{L}$, and
$SE$ be the valid static environment at $\mathit{L}$ inferred by our constant
propagation algorithm. Reducing the next instruction of
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$ will produce the
same result, given that they only differ by substitutions of subexpressions by
values that are valid under the static environment $SE$, and thus under
$\mathit{E}$. If
$\mathit{C_{{\mathrm{1}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
then
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$,
and conversely. ∎

The restriction of our bisimulation $R$ to reachable configurations introduced
is crucial for the proof to work. Indeed, a configuration that is not
reachable may _not_ respect the static environment $SE$. Consider the
following example, with $\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{1}$}}$
on the left and $\mathsf{V\kern-0.5pt\scalebox{0.83}{$\mathsf{2}$}}$ on the
right.

$\displaystyle{\small\begin{array}[]{lll}&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}&\textsf{{var}}~{}\mathsf{x}\nobreak=\nobreak
1\\\ &&\textsf{{print}}\,\mathsf{x}+\mathsf{x}\\\ &&\textsf{{return}}\,3\\\
\end{array}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\small\begin{array}[]{lll}&\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}&\textsf{{var}}~{}\mathsf{x}\nobreak=\nobreak
1\\\ &&\textsf{{print}}\,2\\\ &&\textsf{{return}}\,3\\\ \end{array}}$

Now consider a pair of configurations at
$\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{1}$}}$ with the binding
$\mathsf{x}\rightarrow 0$ in the environment.

$\displaystyle\mathit{C_{{\mathrm{1}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\langle\mathit{P}\,\mathit{P}(\mathit{F},\mathit{V_{{\mathrm{1}}}})\,\mathit{L_{{\mathrm{1}}}}\,K^{*}\;\mathit{M}\,[\mathsf{x}\rightarrow
0]\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\mathit{C_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\langle\mathit{P}\,\mathit{P}(\mathit{F},\mathit{V_{{\mathrm{2}}}})\,\mathit{L_{{\mathrm{1}}}}\,K^{*}\;\mathit{M}\,[\mathsf{x}\rightarrow
0]\rangle$

They would be related by the relation $R$ used by the proof, yet they are not
bisimilar: we have
$\mathit{C_{{\mathrm{1}}}}\overset{\textsf{print}~{}0}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$
as the only transition of $\mathit{C_{{\mathrm{1}}}}$ in
$\mathit{V_{{\mathrm{1}}}}$, and
$\mathit{C_{{\mathrm{2}}}}\overset{\textsf{print}~{}2}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
as the only transition of $\mathit{C_{{\mathrm{2}}}}$ in
$\mathit{V_{{\mathrm{2}}}}$.

###  6.2. Unreachable Code Elimination

The following two lemmas are trivial: the simple version-change mapping
between configurations on the two version is clearly a bisimulation. In the
first case, this comes from the case that
$\textsf{{branch}}~{}\textsf{{true}}~{}\mathit{L_{{\mathrm{1}}}}~{}\mathit{L_{{\mathrm{2}}}}$
and $\textsf{{goto}}\,\mathit{L_{{\mathrm{1}}}}$ reduce in the example same
way. In the second case, unreachable configurations are not even considered by
the proof.

###### Lemma 6.2.

Replacing
$\textsf{{branch}}~{}\textsf{{true}}~{}\mathit{L_{{\mathrm{1}}}}~{}\mathit{L_{{\mathrm{2}}}}$
by $\textsf{{goto}}\,\mathit{L_{{\mathrm{1}}}}$ or
$\textsf{{branch}}~{}\textsf{{false}}~{}\mathit{L_{{\mathrm{1}}}}~{}\mathit{L_{{\mathrm{2}}}}$
by $\textsf{{goto}}\,\mathit{L_{{\mathrm{2}}}}$ results in an equivalent
program.

###### Lemma 6.3.

Removing an unreachable label results in an equivalent program.

###  6.3. Function Inlining

Assume that the function $\mathit{F}$ has active version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{callee}$}}$. If the new version
contains a call to $\mathit{F}$,
$\textsf{{call}}~{}\mathsf{res}\nobreak=\nobreak{\mathit{F}}(\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{e_{\mathit{n}}})$
with return label $\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}$ (the
label after the call), inlining removes the call and instead:

  * •

declares a fresh mutable return variable
$\textsf{{var}}~{}\mathsf{res}\nobreak=\nobreak\textsf{{nil}}$;

  * •

for the formal variables $\mathit{x},..$ of $\mathit{F}$, defines the argument
variables
$\textsf{{var}}~{}\mathit{x}_{{\mathrm{1}}}\nobreak=\nobreak\mathit{se_{{\mathrm{1}}}},..,\textsf{{var}}~{}\mathit{x}_{\mathit{n}}\nobreak=\nobreak\mathit{se_{\mathit{n}}}$;

  * •

inserts the instructions from
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{callee}$}}$, replacing each
instruction $\textsf{{return}}\,\mathit{e}$ by the sequence:
$\mathsf{res}\nobreak\leftarrow\nobreak\mathit{e};~{}\textsf{{drop}}\,\mathit{x}_{{\mathrm{1}}};~{}...~{};~{}\textsf{{drop}}\,\mathit{x}_{\mathit{n}};~{}\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{ret}$}}$

###### Theorem 6.4.

The inlining transformation presented returns a version equivalent to the
caller version.

###### Proof.

The key idea of the proof is that any environment $E$ in the inlined
instruction stream can be split into two disjoint parts: an environment
corresponding to the caller function, $E_{\mathsf{caller}}$, and an
environment corresponding to the callee, $E_{\mathsf{callee}}$. To build the
bisimulation, we relate the inlined version, on one hand, with the callee on
the other hand, _when_ the callee was called by the called at the inlined call
point. This takes two forms:

  * •

If a configuration is currently executing in the callee, and has the caller on
the top of the call stack with the expected return address, we relate it to a
configuration in the inlined version (at the same position in the callee). The
environment of the inlined version is exactly the union of the callee
environment (the environment of the configuration) and the caller environment
(found on the call stack).

  * •

If the stack contains a caller frame above a callee frame, we relate this to a
single frame in the inlined version; again, there is a bidirectional
correspondence between inlined environment and a pair of a caller and callee
environment.

To check that this relation is a bisimulation, there are three interesting
cases:

  * •

If a transition is purely within the callee’s code on one side, and within the
inlined version of the callee on the other, it suffices to check that the
environment decomposition is preserved. During the execution of inlinee,
$E_{\mathsf{caller}}$ never changes, given that the instruction coming from
the callee do not have the caller’s variable in scope—and thus cannot mutate
them.

  * •

If the transition is a call of the callee from the caller on one side, and the
entry into the declaration of the return variable
$\textsf{{var}}~{}\mathsf{res}\nobreak=\nobreak\textsf{{nil}}$ on the other,
we step through the silent transitions that bind the call parameters
$\textsf{{var}}~{}\mathit{x}_{{\mathrm{1}}}\nobreak=\nobreak\mathit{e_{{\mathrm{1}}}},..,\textsf{{var}}~{}\mathit{x}_{\mathit{n}}\nobreak=\nobreak\mathit{e_{\mathit{n}}}$
and get to a state in the inlined function corresponding to the start of the
callee.

  * •

If the transition is a $\textsf{{return}}\,\mathit{e}$ of the callee to the
caller on one side, and the entry into the result assignment
$\mathsf{res}\nobreak\leftarrow\nobreak\mathit{e}$ on the other, we similarly
step through the $\textsf{{drop}}\,\mathit{x}$ for each $\mathit{x}$ in the
callee’s environment, and get to related state on the label $ret$ following
the function call.

∎

###  6.4. Unrestricted Deoptimization

Consider $\mathit{P_{{\mathrm{1}}}}$ containing an assume at
$\mathit{L_{{\mathrm{1}}}}$, followed by $\mathit{i_{\mathit{m}}}$ at
$\mathit{L_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}(\mathit{L_{{\mathrm{1}}}}\kern-1.0pt+\kern-2.0pt1)$.
Let $\mathit{i_{\mathit{m}}}$ be such it has a unique successor, is the unique
predecessor of $\mathit{L_{{\mathrm{1}}}}$, and is not a function call, has no
side-effect, does not modify the heap (array write or creation), and does not
modify the variables mentioned in the assume. Under these conditions, we can
move the assume immediately after the successor of $\mathit{i_{\mathit{m}}}$.
Let us name $\mathit{P_{{\mathrm{2}}}}$ the program modified in this way.

###### Lemma 6.5.

Given a program $\mathit{P_{{\mathrm{1}}}}$, and $\mathit{P_{{\mathrm{2}}}}$
obtained by permuting an assume instruction $\mathit{L_{{\mathrm{1}}}}$ after
$\mathit{i_{\mathit{m}}}$ at $\mathit{L_{{\mathrm{2}}}}$ under the conditions
above, $\mathit{P_{{\mathrm{1}}}}$ and $\mathit{P_{{\mathrm{2}}}}$ are
bisimilar.

###### Proof.

The applicability restrictions are specific enough that we can reason
precisely about the structure of reductions around the permuted instructions.
Consider a configuration $\mathit{C_{{\mathrm{1}}}}$ over the assume at
$\mathit{L_{{\mathrm{1}}}}$ in $\mathit{P_{{\mathrm{1}}}}$, and the
corresponding configuration
$\mathit{C_{{\mathrm{2}}}}\mathrel{\stackrel{{\scriptstyle\mathsf{def}}}{{=}}}\mathit{C_{{\mathrm{1}}}}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}][\mathit{L_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{L_{{\mathrm{2}}}}]$
over $\mathit{L_{{\mathrm{2}}}}$ in $\mathit{P_{{\mathrm{2}}}}$. Instruction
$\mathit{i_{\mathit{m}}}$ has a single successor, so there is only one
possible reduction rule. Since $\mathit{i_{\mathit{m}}}$ is not an I/O
instruction, it must be a silent action. Hence there is a unique
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ such that
$\mathit{C_{{\mathrm{2}}}}\overset{\mathit{A}_{\tau}}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
holds, and furthermore $\mathit{A}_{\tau}$ is $\tau$. Configurations
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$ are over
the same assume. Let $\mathit{E_{{\mathrm{1}}}}$ and
$\mathit{E_{{\mathrm{2}}}}$ be environments of $\mathit{C_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ respectively, and $\mathit{E^{\prime}}$
be their common sub-environment that contain only the variables mentioned in
the assume ($\mathit{i_{\mathit{m}}}$ does not modify its variables). If all
tests in the assume instruction are true under $\mathit{E^{\prime}}$, then
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$ silently
reduce to $\mathit{C^{\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$.
$\mathit{C^{\prime}_{{\mathrm{1}}}}$ is over $\mathit{i_{\mathit{m}}}$ at
$\mathit{L_{{\mathrm{2}}}}$, so it reduces
$\mathit{C^{\prime}_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$;
notice that $\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$ are over the labels
$(\mathit{L_{{\mathrm{2}}}}\kern-1.0pt+\kern-2.0pt1)$ in
$\mathit{P_{{\mathrm{1}}}}$ and
$(\mathit{L_{{\mathrm{1}}}}\kern-1.0pt+\kern-2.0pt1)$ in
$\mathit{P_{{\mathrm{2}}}}$, which are equal. If not all tests of the assume
are true under $\mathit{E^{\prime}}$, then both $\mathit{C_{{\mathrm{1}}}}$
and $\mathit{C^{\prime}_{{\mathrm{2}}}}$ deoptimize. The deoptimized
configurations are the same

  * •

their function, version and label are the same: the assume’s deoptimization
target;

  * •

they have the same call stack: it only depends on the call stack of
$\mathit{C_{{\mathrm{1}}}}$ and the interpretation of the assume’s extra
frames under $\mathit{E^{\prime}}$;

  * •

they have the same heap, as we assumed that $\mathit{i_{\mathit{m}}}$ does not
modify the heap;

  * •

they have the same deoptimized environment: it only depends on
$\mathit{E^{\prime}}$.

Let us call $\mathit{C_{{\mathrm{0}}}}$ the configuration resulting from
either deoptimization transitions.

We establish bisimilarity using definition a relation $R$ and proving it is a
bisimulation. The following diagrams are useful to follow the definition of
$R$ and the proofs.

${\mathit{L_{{\mathrm{1}}}}:\mathit{C_{{\mathrm{1}}}}}$${\mathit{L_{{\mathrm{2}}}}:\mathit{C^{\prime}_{{\mathrm{1}}}}}$${\mathit{C^{\prime\prime}_{{\mathrm{1}}}}}$${\mathit{L_{{\mathrm{2}}}}:\mathit{C_{{\mathrm{2}}}}}$${\mathit{L_{{\mathrm{1}}}}:\mathit{C^{\prime}_{{\mathrm{2}}}}}$${\mathit{C^{\prime\prime}_{{\mathrm{2}}}}}$assume$\scriptstyle{\mathit{i_{\mathit{m}}}}$$\scriptstyle{R}$$\scriptstyle{\mathit{i_{\mathit{m}}}}$assume$\scriptstyle{R}$$\scriptstyle{R}$$\scriptstyle{R}$
${\mathit{L_{{\mathrm{1}}}}:\mathit{C_{{\mathrm{1}}}}}$${\mathit{C_{{\mathrm{0}}}}}$${\mathit{L_{{\mathrm{2}}}}:\mathit{C_{{\mathrm{2}}}}}$${\mathit{L_{{\mathrm{1}}}}:\mathit{C^{\prime}_{{\mathrm{2}}}}}$${\mathit{C_{{\mathrm{0}}}}}$$\scriptstyle{\mathsf{deoptimize}}$$\scriptstyle{R}$$\scriptstyle{\mathit{i_{\mathit{m}}}}$$\scriptstyle{R}$$\scriptstyle{\mathsf{deoptimize}}$

We define $R$ as the smallest relation such that:

  1. (1)

For any $\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$ as above,
$\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C^{\prime}_{{\mathrm{1}}}}$ are
related to $\mathit{C_{{\mathrm{2}}}}$.

  2. (2)

For any $\mathit{C_{{\mathrm{1}}}}$ and $\mathit{C_{{\mathrm{2}}}}$ as above
such that $\mathit{C_{{\mathrm{1}}}}$ passes the assume tests (does not
deoptimize), both $\mathit{C^{\prime}_{{\mathrm{2}}}}$ and
$\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$ are related to
$\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$.

  3. (3)

For any $\mathit{C}$ over $\mathit{P_{{\mathrm{1}}}}$ that is over neither
$\mathit{L_{{\mathrm{1}}}}$ nor $\mathit{L_{{\mathrm{2}}}}$, $\mathit{C}$ and
$\mathit{C}[\mathit{P_{{\mathrm{1}}}}\nobreak\leftarrow\nobreak\mathit{P_{{\mathrm{2}}}}]$
are related.

We now prove that $R$ is a bisimulation. Any pair of configurations that are
not over either $\mathit{L_{{\mathrm{1}}}}$ or $\mathit{L_{{\mathrm{2}}}}$
come from the case (3), so they are identical and it is immediate that they
match each other. The interesting cases are for matching pairs of
configurations over $\mathit{L_{{\mathrm{1}}}}$ or
$\mathit{L_{{\mathrm{2}}}}$.

In the case where no deoptimization happens, the reductions in
$\mathit{P_{{\mathrm{2}}}}$ are either
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$,
where both configurations are related to $\mathit{C_{{\mathrm{1}}}}$, or
$\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$
which is matched by
$\mathit{C_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$.
The reductions in $\mathit{P_{{\mathrm{1}}}}$ are either
$\mathit{C_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$,
which is matched by
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$
and
$\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$,
or
$\mathit{C^{\prime}_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime\prime}_{{\mathrm{1}}}}$,
which are both related to $\mathit{C^{\prime\prime}_{{\mathrm{2}}}}$.

In the case where a deoptimization happens, the only reduction in
$\mathit{P_{{\mathrm{1}}}}$ is
$\mathit{C_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C_{{\mathrm{0}}}}$,
which is matched by
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C_{{\mathrm{0}}}}$
and
$\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C_{{\mathrm{0}}}}$.
The reductions in $\mathit{P_{{\mathrm{2}}}}$ are
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$,
which are matched by the empty reduction on $\mathit{C_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime}_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C_{{\mathrm{0}}}}$
are matched by
$\mathit{C_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C_{{\mathrm{0}}}}$.

Finally, we show preservation of the assumption transparency invariant. We
have to establish the invariant for $\mathit{P_{{\mathrm{2}}}}$, assuming the
invariant for $\mathit{P_{{\mathrm{2}}}}$. We have to show that
$\mathit{C_{{\mathrm{0}}}}$ and $\mathit{C^{\prime}_{{\mathrm{2}}}}$ are
bisimilar. $\mathit{C_{{\mathrm{0}}}}$ is bisimilar to
$\mathit{C_{{\mathrm{1}}}}$ (this is the transparency invariant on
$\mathit{P_{{\mathrm{1}}}}$), and $\mathit{C_{{\mathrm{1}}}}$ and
$\mathit{C^{\prime}_{{\mathrm{2}}}}$ are bisimilar because they are related by
the bisimulation $R$. ∎

###  6.5. Predicate Hoisting

Hoisting predicates takes a version $\mathit{V_{{\mathrm{1}}}}$, an expression
$\mathit{e}$, and two labels
$\mathit{L_{{\mathrm{1}}}},\mathit{L_{{\mathrm{2}}}}$, such that the
instruction at $\mathit{L_{{\mathrm{1}}}},\mathit{L_{{\mathrm{2}}}}$ are both
assume instructions and $\mathit{e}$ is a part of the predicate list at
$\mathit{L_{{\mathrm{1}}}}$. The pass copies $\mathit{e}$ from
$\mathit{L_{{\mathrm{1}}}}$ to $\mathit{L_{{\mathrm{2}}}}$, if all variables
mentioned in $\mathit{e}$ are in scope at $\mathit{L_{{\mathrm{2}}}}$. If,
after this step the $\mathit{e}$ can be constant folded to true at
$\mathit{L_{{\mathrm{1}}}}$ by the optimization from Section 4.1, then it is
removed from $\mathit{L_{{\mathrm{1}}}}$, otherwise the whole version stays
unchanged.

###### Lemma 6.6.

Let $\mathit{V_{{\mathrm{2}}}}$ be the result of hoisting $\mathit{e}$ from
$\mathit{L_{{\mathrm{1}}}}$ to $\mathit{L_{{\mathrm{2}}}}$ in
$\mathit{V_{{\mathrm{1}}}}$. $\mathit{V_{{\mathrm{1}}}}$ and
$\mathit{V_{{\mathrm{2}}}}$ are bisimilar.

###### Proof.

Copying is bisimilar due to the assumption transparency invariant and to the
fact that the constant-folded version is bisimilar due to Lemma 6.1. ∎

###  6.6. Assume Composition

Let
$\mathit{V_{{\mathrm{1}}}},\mathit{V_{{\mathrm{2}}}},\mathit{V_{{\mathrm{3}}}}$
be three versions of a function $\mathit{F}$ with instruction streams
$\mathit{I_{{\mathrm{1}}}},\mathit{I_{{\mathrm{2}}}},\mathit{I_{{\mathrm{3}}}}$,
and
$\mathit{L_{{\mathrm{1}}}},\mathit{L_{{\mathrm{2}}}},\mathit{L_{{\mathrm{3}}}}$
labels, such that
$\mathit{I_{{\mathrm{1}}}}(\mathit{L_{{\mathrm{1}}}})=\textsf{{assume}}~{}\mathit{e_{{\mathrm{1}}}}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{2}}}}.\kern-0.5pt\mathit{L_{{\mathrm{2}}}}~{}\mathit{VA}_{{\mathrm{1}}}$
and
$\mathit{I_{{\mathrm{2}}}}(\mathit{L_{{\mathrm{2}}}})=\textsf{{assume}}~{}\mathit{e_{{\mathrm{2}}}}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{3}}}}.\kern-0.5pt\mathit{L_{{\mathrm{3}}}}~{}\mathit{VA}_{{\mathrm{2}}}$.
The composition pass creates a new program $\mathit{P_{{\mathrm{2}}}}$ from
$\mathit{P_{{\mathrm{1}}}}$ identical but the assume
$\mathit{P_{{\mathrm{2}}}}(\mathit{F}.\mathit{V_{{\mathrm{1}}}}.\mathit{L_{{\mathrm{1}}}})$
is replaced by
$\textsf{{assume}}~{}\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V_{{\mathrm{3}}}}.\kern-0.5pt\mathit{L_{{\mathrm{3}}}}~{}\mathit{VA}_{{\mathrm{2}}}\circ\mathit{VA}_{{\mathrm{1}}}$
where
$([{\mathit{x}_{{\mathrm{1}}}=\mathit{e_{{\mathrm{1}}}},\,..\,,\mathit{x}_{\mathit{n}}=\mathit{e_{\mathit{n}}}\kern
0.33005pt}]\circ\mathit{VA})$ is defined as
$[x_{1}=e_{1}\\{\frac{\mathit{VA}(y)}{y}\forall
y\in\mathit{VA}\\},..,x_{n}=e_{n}\\{\frac{\mathit{VA}(y)}{y}\forall
y\in\mathit{VA}\\}]$.

###### Lemma 6.7.

Let $\mathit{P_{{\mathrm{2}}}}$ be the result of composing assume instructions
at $\mathit{L_{{\mathrm{1}}}}$ and $\mathit{L_{{\mathrm{2}}}}$.
$\mathit{P_{{\mathrm{1}}}}$ and $\mathit{P_{{\mathrm{2}}}}$ are bisimilar.

###### Proof.

For
$\mathit{C_{{\mathrm{1}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{1}}}}$,
$\mathit{C_{{\mathrm{2}}}}\overset{\tau}{\longrightarrow}\mathit{C^{\prime}_{{\mathrm{2}}}}$
over $\mathit{L_{{\mathrm{1}}}}$ in $\mathit{P_{{\mathrm{1}}}}$,
$\mathit{P_{{\mathrm{2}}}}$, we distinguish four cases:

  1. (1)

If $\mathit{e_{{\mathrm{1}}}}$ and $\mathit{e_{{\mathrm{2}}}}$ both hold, the
assume does not deoptimize in $\mathit{P_{{\mathrm{1}}}}$ and
$\mathit{P_{{\mathrm{2}}}}$ and they behave identically.

  2. (2)

If $\mathit{e_{{\mathrm{1}}}}$ and $\mathit{e_{{\mathrm{2}}}}$ both fail, the
original program deoptimizes twice; the modified $\mathit{P_{{\mathrm{2}}}}$
only once. Assuming deoptimizing under the combined varmap
$\mathit{M}\,\mathit{E}\,\mathit{VA}_{{\mathrm{2}}}\circ\mathit{VA}_{{\mathrm{1}}}\rightsquigarrow\mathit{E^{\prime\prime}}$
produces an environment equivalent to
$\mathit{M}\,\mathit{E}\,\mathit{VA}_{{\mathrm{1}}}\rightsquigarrow\mathit{E^{\prime}}$
and
$\mathit{M}\,\mathit{E^{\prime}}\,\mathit{VA}_{{\mathrm{2}}}\rightsquigarrow\mathit{E^{\prime\prime}}$
the final configuration is identical. Since the extra intermediate step is
silent, both programs are bisimilar.

  3. (3)

If $\mathit{e_{{\mathrm{1}}}}$ fails and $\mathit{e_{{\mathrm{2}}}}$ holds, we
deoptimize to $\mathit{V_{{\mathrm{3}}}}$ in $\mathit{P_{{\mathrm{2}}}}$, but
to $\mathit{V_{{\mathrm{2}}}}$ in $\mathit{P_{{\mathrm{1}}}}$. As shown in
case (2) the deoptimized configuration $\mathit{C^{\prime}_{{\mathrm{2}}}}$
over $\mathit{L_{{\mathrm{3}}}}$ is equivalent to a post-deoptimization
configuration of $\mathit{C^{\prime}_{{\mathrm{1}}}}$, which, due to
assumption transparency is bisimilar to $\mathit{C^{\prime}_{{\mathrm{1}}}}$
itself.

  4. (4)

If $\mathit{e_{{\mathrm{1}}}}$ holds and $\mathit{e_{{\mathrm{2}}}}$ fails,
deoptimize to $\mathit{V_{{\mathrm{3}}}}$ in $\mathit{P_{{\mathrm{2}}}}$ but
not in $\mathit{P_{{\mathrm{1}}}}$. Again $\mathit{C^{\prime}_{{\mathrm{2}}}}$
is equivalent to a post-deoptimization state, which is, transitively,
bisimilar to $\mathit{C^{\prime}_{{\mathrm{1}}}}$.

Since a well-formed assume has only unique names in the deoptimization
metadata, it is simple to show the assumption in (2) with a substitution
lemma. ∎

##  7\. Discussion

Our formalization raises new questions and makes apparent certain design
choices. In this section, we present insights into the design space for JIT
implementations.

${\small\begin{array}[]{lll}&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}&\textsf{{branch}}~{}\mathsf{z}\neq
0~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body}$}}&\textsf{{call}}~{}\mathsf{x}\nobreak=\nobreak{\scalebox{0.97}{$\mathsf{dostuff}$}}(\,)\\\
&&\textsf{{var}}~{}\mathsf{y}\nobreak=\nobreak\mathsf{x}+13\\\
&&\textsf{{assume}}~{}\mathit{e}~{}\mathbf{else}~{}\mathit{F}.\kern-0.5pt\mathit{V}.\kern-0.5pt\mathit{L}~{}[{\mathsf{x}=\mathsf{x},\mathsf{y}=\mathsf{x}+13\kern
0.29704pt}]\\\ &&\textsf{{drop}}\,\mathsf{y}\\\
&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}&\dots\\\ \end{array}}$

Figure 18. Deoptimization keeps variables alive.

#### The Cost of Assuming

Assumptions restrict optimizations. Variables needed for deoptimization must
be kept alive. Consider Figure 18, where an assume is at the end of a loop. As
$\mathsf{y}$ is not modified, it can be removed. There is enough information
to reconstruct it if needed. On the other hand, $\mathsf{x}$ cannot be
synthesized out of thin air because it is computed in another function.
Additionally, assume restricts code motion in two cases. First, side-effecting
code cannot be moved over an assume. Second, assume instructions cannot be
hoisted over instructions that interfere with variables mentioned in metadata.
It is possible to move assume forward, since data dependencies can be resolved
by taking a snapshot of the environment at the original location. For the
reverse effect, we support hoisting the predicate from one assume to another
(see Section 4.5). Moving assume instructions up is tricky and also
unnecessary, since in combination those two primitives allow moving checks to
any position. In the above example, if $e$ is invariant in the loop body and
there is an assume before
$\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}$, the predicate can be
hoisted out of the loop. If the assume is only relevant for a subset of the
instructions after the current location, it can be moved down as a whole.

#### Lazy Deoptimization

The runtime cost of an assume is the cost of monitoring the predicates.
Suppose we speculate that the contents of an array remain unchanged throughout
a loop. An implementation would have to check every single element of the
array. An eager strategy where predicates are checked at every iteration is
wasteful. It is more efficient to associate checks to operations that may
invalidate the predicates, such as array writes, to invalidate the assumption,
a strategy sometimes known as _lazy deoptimization_. We could implement
dependencies by separating

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{stuck}$}(\,\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@gray@fill{.5&&\textsf{{call}}~{}\mathsf{debug}\nobreak=\nobreak{\scalebox{0.97}{$\mathsf{debug}$}}(\,)\\\
\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<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{h}$}}\\\
\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 19. Long running execution.

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{cont}$}(\mathsf{x}\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{opt}$}}\\\
\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&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{h}$}}\\\
\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 20. Switching to optimized code.

${\small\begin{array}[]{l}\scalebox{0.97}{$\mathsf{undo}$}(\,\kern
0.35994pt)\\\ \begin{array}[]{llll}\kern 1.5pt\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s123}$}}\\\
\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}}~{}\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}},\mathit{e_{{\mathrm{3}}}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{undo}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s12}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{0}$}}~{}[{\dots\kern
0.29704pt}]\\\ \end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s12}$}}\\\
\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}}~{}\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}~{}\mathbf{else}~{}\scalebox{0.97}{$\mathsf{undo}$}.\kern-0.5pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s1}$}}.\kern-0.5pt\mathsf{L\kern-0.25pt\scalebox{0.83}{$\mathsf{0}$}}~{}[{\dots\kern
0.29704pt}]\\\ \end{array}\vspace{0.25em}\\\ \,\hskip
7.11317pt\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s1}$}}\\\
\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}]\\\ \end{array}\vspace{0.25em}\\\ \end{array}\\\ \end{array}}}}}$

Figure 21. Undoing an isolated predicate.

assumptions from runtime checks. Specifically, let
$\mathsf{GUARDS}[{13}]=\textsf{{true}}$ be the runtime check, where the global
array $\mathsf{GUARDS}$ is a collection of all remote assumptions that can be
invalidated by an operation, such as an array assignment. In terms of
correctness, both eager and lazy deoptimization are similar; however, we would
need to prove correctness of the dependency mechanism that modifies the global
array.

#### Jumping Into Optimized Code

We have shown how to transfer control out of optimized code. The inverse
transition, jumping into optimized code, is interesting as well. Consider
executing the long running loop of Figure 21. The value of $\mathsf{debug}$ is
constant in the loop, yet execution is stuck in the long running function and
must branch on each iteration. A JIT can compile an optimized version that
speculates on $\mathsf{debug}$, but it may only use it on the next invocation.
Ideally, the JIT would jump into the newly optimized code from the slow loop;
this is known as _hot loop transfer_. Specifically, the next time
$\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{o}$}}$ is reached, control is
transferred to an equivalent location in the optimized version. To do so,
continuation-passing style can be used to compile a staged continuation
function from the beginning of the loop where $\mathsf{debug}$ is known to be
false. The optimized continuation might look like  $\mathsf{cont}$ in Figure
21. In some sense, this is easier than deoptimization because it strengthens
assumptions rather than weakening them and all the values needed to construct
the state at the target version are readily available.

#### Fine-Grained Deoptimization

Instead of blindly removing all assumptions on deoptimization, it is possible
to undo only failing assumptions while preserving the rest. As shown in Figure
21, if $\mathit{e_{{\mathrm{2}}}}$ fails in version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s123}$}}$, one can jump to the
last version that did not rely on this predicate. By deoptimizing to version
$\mathsf{V\kern-0.25pt\scalebox{0.87}{$\mathsf{s1}$}}$, assumption
$\mathit{e_{{\mathrm{3}}}}$ must be discarded. However,
$\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{3}}}}$ still hold, so we would
like to preserve optimizations based on those assumptions. Using the technique
mentioned above, execution can be transferred to a version
$\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{s13}$}}$ that reintroduces
$\mathit{e_{{\mathrm{3}}}}$. The overall effect is that we remove only the
invalidated assumption and its optimizations. We are not aware of an existing
implementation that explores such a strategy.

${\small\begin{array}[]{lll}&&\dots\\\
&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}&\textsf{{branch}}~{}\mathit{e}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body}$}}&\mathsf{x}\nobreak\leftarrow\nobreak
0\\\ &&\dots\\\
&&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}\\\
&\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}&\dots\\\ \end{array}}$

Figure 22. Loop with a dead store.

#### Simulating a Tracing JIT

A tracing JIT (Bala et al., 2000; Gal et al., 2009) records instructions that
are executed in a trace. Branches and redundant checks can be discarded from
the trace. Typically, a trace corresponds to a path through a hot loop. On
subsequent runs the trace is executed directly. The JIT ensures that execution
follows the same path, otherwise it deoptimizes back to the original program.
In this context Guo and Palsberg (2011) develop a framework for reasoning
about optimizations applied to traces. One of their results is that dead store
elimination is unsound, because the trace is only a partial view of the entire
program. For example, a variable $\mathsf{x}$ might be assigned to within a
trace, but never used. However, it is unsound to remove the assignment,
because $x$ might be used outside the trace. We can simulate their tracing
formalism in sourir. Consider a variant of their running example shown in
Figure 22, a trace of the loop $\textbf{while}\;e\;(x\leftarrow 0;\;\ldots)$
embedded in a larger context. Instead of a JIT that records instructions,
assume only branch targets are recorded. For this example, suppose the two
targets $\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body}$}}$ and
$\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}$ are recorded, which
means the loop body executed once and then exited. In other words, the loop
condition $\mathit{e}$ was true the first time and false the second time. The
compiler could unroll the loop twice and assert $\mathit{e}$ for the first
iteration and $\neg\mathit{e}$ for the second iteration (left). Then
unreachable code elimination yields the right hand side, resembling a trace.

${\small\begin{array}[]{lll}&&\dots\\\ &&\textsf{{assume}}~{}\mathit{e}~{}\mathbf{else}~{}\mathsf{F}.\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{loop}$}}~{}[{\mathsf{x}=\mathsf{x},\dots\kern 0.29704pt}]\\\ &&\textsf{{branch}}~{}\mathit{e}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body_{0}}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}\\\ &\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body_{0}}$}}&\mathsf{x}\nobreak\leftarrow\nobreak 0\\\ &&\dots\\\ &&\textsf{{assume}}~{}\neg\mathit{e}~{}\mathbf{else}~{}\mathsf{F}.\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{loop}$}}~{}[{\mathsf{x}=\mathsf{x},\dots\kern 0.29704pt}]\\\ &&\textsf{{branch}}~{}\mathit{e}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body_{1}}$}}~{}\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}\\\ &\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{body_{1}}$}}&\mathsf{x}\nobreak\leftarrow\nobreak 0\\\ &&\dots\\\ &&\textsf{{goto}}\,\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{loop}$}}\\\ &\mathsf{L\kern-0.25pt\scalebox{0.87}{$\mathsf{done}$}}&\dots\\\ \end{array}}$ | ${\small\begin{array}[]{lll}&&\dots\\\ &&\textsf{{assume}}~{}\mathit{e}~{}\mathbf{else}~{}\mathsf{F}.\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{loop}$}}~{}[{\mathsf{x}=\mathsf{x},\dots\kern 0.29704pt}]\\\ &&\mathsf{x}\nobreak\leftarrow\nobreak 0\\\ &&\dots\\\ &&\textsf{{assume}}~{}\neg\mathit{e}~{}\mathbf{else}~{}\mathsf{F}.\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{loop}$}}~{}[{\mathsf{x}=\mathsf{x},\dots\kern 0.29704pt}]\\\ &&\dots\\\ \end{array}}$
---|---

Say $\mathsf{x}$ is not accessed after the store in this optimized version. In
sourir, it is obvious why dead store elimination of $\mathsf{x}$ would be
unsound: the deoptimization metadata indicates that $\mathsf{x}$ is needed for
deoptimization and the store operation can only be removed it can be replayed.
In this specific example, a constant propagation pass could update the
metadata to materialize the write of $0$, only when deoptimizing at the second
assume. But, before the code can be reduced, loop unrolling might result in
intermediate versions that are much larger than the original program. In
contrast, tracing JITs can handle this case without the drastic expansion in
code size (Gal et al., 2009), but lose more information about instructions
outside of the trace.

##  8\. Conclusions

Speculative optimizations are key to just-in-time optimization of dynamic
languages. As these optimizations depend on predicates about the program
state, the language implementation must monitor the validity of predicates and
be ready to deoptimize the program if a predicate is invalidated. While, many
modern compiler rely on this approach, the interplay between optimization and
deoptimization often remains opaque.

Our contribution is to show that when the predicates and the deoptimization
metadata are reified in the program representation, it becomes quite easy to
define correct program transformations that are deoptimization aware. In this
work we extend the intermediate representation with one new instruction,
assume, which plays the double role of checking for the validity of predicates
and specifying the actions required to deoptimize the program. Program
transformations can inspect both the predicates that are being monitored and
the deoptimization metadata and transform them when needed. The formalization
presented here is for one particular intermediate language that we hope to be
representative of a typical dynamic language. We present a bisimulation proof
between multiple versions of the same function, optimized under different
assumptions. We formalize deoptimization invariants between versions and show
that they enable very simple proofs for standard compiler optimizations,
constant folding, unreachable code elimination, and function inlining. We also
prove correct three optimizations that are specifically dealing with
deoptimizations, namely unrestricted deoptimization, predicate hoisting, and
assume composition.

There are multiple avenues of future investigation. The optimizations
presented here rely on intraprocedural analysis and the granularity of
deoptimization is a whole function. If we were to extend this work to
interprocedural analysis, it would become much trickier to determine what
functions are to be invalidated as a speculation in one function may allow
optimizations in many other functions. The current representation forces to
check predicates before each use, but some predicates are cheaper to check by
monitoring operations that could invalidate them. To do this would require
changes to our model as the assume instruction would need to be split between
a monitor and a deoptimization point. Lastly, the expressive power of
predicates is an interesting question as there is a clear trade-off — richer
predicates may allow more optimizations but are likely to be costlier to
monitor.

###### Acknowledgements.

Jean-Marie Madiot provided guidance on the use and limitations of various
notions of bisimulation. In particular, he suggested adding a non-silent stop
transition to recover equi-termination from weak bisimilarity. Francesco Zappa
Nardelli helped with the motivation and presentation of our work. We thank
Sewell et al. (2007) for writing and maintaining Ott. Our work supported by
the National Science Foundation under Grants CCF–1544542, CCF–1318227,
CCF–1618732, ONR award 503353, and the European Research Council (ERC) under
the European Union’s Horizon 2020 research and innovation program (grant
agreement 695412). Any opinions, findings, and conclusions expressed in this
material may be those of the authors and likely do not reflect the views of
our funding agencies.

## References

  * (1)
  * Bala et al. (2000) Vasanth Bala, Evelyn Duesterwald, and Sanjeev Banerjia. 2000\.  Dynamo: A Transparent Dynamic Optimization System. In Programming Language Design and Implementation (PLDI).  https://doi.org/10.1145/349299.349303
  * Bebenita et al. (2010) Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter. 2010\.  SPUR: A Trace-based JIT Compiler for CIL. In Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA).  https://doi.org/10.1145/1869459.1869517
  * Béra et al. (2016) Clément Béra, Eliot Miranda, Marcus Denker, and Stéphane Ducasse. 2016.  Practical validation of bytecode to bytecode JIT compiler dynamic deoptimization.  Journal of Object Technology (JOT) 15, 2 (2016).  https://doi.org/10.5381/jot.2016.15.2.a1
  * Chromium (2017) Project Chromium. 2017\.  V8 JavaScript Engine.  https://chromium.googlesource.com/v8/v8.git.
  * D’Elia and Demetrescu (2016) Daniele Cono D’Elia and Camil Demetrescu. 2016.  Flexible on-stack replacement in LLVM. In Code Generation and Optimization (CGO).  https://doi.org/10.1145/2854038.2854061
  * Dissegna et al. (2014) Stefano Dissegna, Francesco Logozzo, and Francesco Ranzato. 2014.  Tracing Compilation by Abstract Interpretation. In Principles of Programming Languages (POPL).  https://doi.org/10.1145/2535838.2535866
  * Duboscq et al. (2014) Gilles Duboscq, Thomas Würthinger, and Hanspeter Mössenböck. 2014\.  Speculation without regret: reducing deoptimization meta-data in the Graal compiler. In Principles and Practices of Programming on the Java Platform (PPPJ).  https://doi.org/10.1145/2647508.2647521
  * 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 Virtual Machines and Intermediate Languages (VMIL).  https://doi.org/10.1145/2542142.2542143
  * Fink and Qian (2003) Stephen J. Fink and Feng Qian. 2003.  Design, Implementation and Evaluation of Adaptive Recompilation with On-stack Replacement. In Code Generation and Optimization (CGO).  https://doi.org/10.1109/CGO.2003.1191549
  * 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/1542476.1542528
  * Guo and Palsberg (2011) Shu-yu Guo and Jens Palsberg. 2011.  The Essence of Compiling with Traces. In Principles of Programming Languages (POPL).  https://doi.org/10.1145/1926385.1926450
  * Hölzle et al. (1992) Urs Hölzle, Craig Chambers, and David Ungar. 1992\.  Debugging Optimized Code with Dynamic Deoptimization. In Programming Language Design and Implementation (PLDI).  https://doi.org/10.1145/143095.143114
  * Ishizaki et al. (2000) Kazuaki Ishizaki, Motohiro Kawahito, Toshiaki Yasue, Hideaki Komatsu, and Toshio Nakatani. 2000\.  A Study of Devirtualization Techniques for a Java Just-In-Time Compiler. In Object-oriented Programming Systems, Language, and Applications (OOPSLA).  https://doi.org/10.1145/353171.353191
  * Kildall (1973) Gary A. Kildall. 1973\.  A Unified Approach to Global Program Optimization. In Principles of Programming Languages (POPL).  https://doi.org/10.1145/512927.512945
  * Leroy and Blazy (2008) Xavier Leroy and Sandrine Blazy. 2008.  Formal verification of a C-like memory model and its uses for verifying program transformations.  Journal of Automated Reasoning 41, 1 (2008).  https://doi.org/10.1007/s10817-008-9099-0
  * Myreen (2010) Magnus O. Myreen. 2010\.  Verified Just-in-time Compiler on x86. In Principles of Programming Languages (POPL).  https://doi.org/10.1145/1706299.1706313
  * Odaira and Hiraki (2005) Rei Odaira and Kei Hiraki. 2005.  Sentinel PRE: Hoisting Beyond Exception Dependency with Dynamic Deoptimization. In Code Generation and Optimization (CGO).  https://doi.org/10.1109/CGO.2005.32
  * Paleczny et al. (2001) Michael Paleczny, Christopher Vick, and Cliff Click. 2001\.  The Java Hotspot Server Compiler. In Java Virtual Machine Research and Technology (JVM).  http://www.usenix.org/events/jvm01/full_papers/paleczny/paleczny.pdf
  * Sabry and Felleisen (1992) Amr Sabry and Matthias Felleisen. 1992.  Reasoning About Programs in Continuation-passing Style. In LISP and Functional Programming (LFP).  https://doi.org/10.1145/141471.141563
  * Schneider and Bolz (2012) David Schneider and Carl Friedrich Bolz. 2012.  The efficient handling of guards in the design of RPython’s tracing JIT. In Workshop on Virtual Machines and Intermediate Languages (VMIL).  https://doi.org/10.1145/2414740.2414743
  * Sewell et al. (2007) Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. 2007\.  Ott: Effective Tool Support for the Working Semanticist. In International Conference on Functional Programming (ICFP).  https://doi.org/10.1145/1291151.1291155
  * Soman and Krintz (2006) Sunil Soman and Chandra Krintz. 2006.  Efficient and General On-Stack Replacement for Aggressive Program Specialization. In Software Engineering Research and Practice (SERP).
  * Wang et al. (2015) Kunshan Wang, Yi Lin, Stephen M. Blackburn, Michael Norrish, and Antony L. Hosking. 2015.  Draining the Swamp: Micro Virtual Machines as Solid Foundation for Language Development. In Summit on Advances in Programming Languages (SNAPL), Vol. 32.  https://doi.org/10.4230/LIPIcs.SNAPL.2015.321
  * Zheng et al. (2017) Yudi Zheng, Lubomír Bulej, and Walter Binder. 2017\.  An Empirical Study on Deoptimization in the Graal Compiler. In European Conference on Object-Oriented Programming (ECOOP).  https://doi.org/10.4230/LIPIcs.ECOOP.2017.30