% vim: spell spelllang=en

\documentclass[11pt,xcolor={usenames,dvipsnames}]{beamer}
\usetheme{Warsaw}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{my_listings}
\usepackage{math}
\usepackage{tikz}
\usetikzlibrary{shapes, arrows}
\setbeamertemplate{navigation symbols}{}

\newcommand{\wrt}{\textit{wrt.}}

\newcommand{\progs}{\mathbb{P}}
\newcommand{\labels}{\mathbb{L}}
\newcommand{\values}{\mathbb{K}}
\newcommand{\vars}{\mathcal{V}}
\newcommand{\exprs}{\text{Expr}}
\newcommand{\bexprs}{\text{BExpr}}
\newcommand{\actions}{\mathbb{A}}
\newcommand{\commands}{\mathbb{C}}
\newcommand{\askip}{\operatorname{skip}}
\newcommand{\stores}{\operatorname{Store}}
\newcommand{\states}{\operatorname{State}}
\newcommand{\traces}{\operatorname{Trace}}
\newcommand{\types}{\operatorname{Type}}
\newcommand{\state}[2]{\langle{} #1, #2 \rangle{}}
\newcommand{\guard}[1]{\operatorname{guard} E_{#1}}
\newcommand{\gu}[1]{\operatorname{G} E_{#1}}
\newcommand{\extr}[1]{\operatorname{extr}_{#1}}

\newcommand{\hot}[1]{\operatorname{hot}_{#1}}
\newcommand{\evexpT}[2]{\mathbf{E}^t\left(#1\right)_{#2}}
\newcommand{\tracesOf}{\mathbf{T}}

\newcommand*\oldmacro{}%
\let\oldmacro\insertshorttitle%
\renewcommand*\insertshorttitle{%
   \oldmacro\hfill%
   \insertframenumber\,/\,\inserttotalframenumber}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{Théophile \textsc{Bastian}}
\title[Tracing Compilation by Abstract Interpretation]
    {Tracing Compilation by Abstract Interpretation \\
    {\small{}S. Dissegna, F. Logozzo, F. Ranzato}}
\date{March 7, 2018}

\begin{document}

\begin{frame}
    \addtocounter{framenumber}{-1}
	\titlepage{}

    Slides: \url{https://tiny.tobast.fr/m2-absint-slides} \\
    Article: \url{https://tiny.tobast.fr/m2-absint-article}
\end{frame}

\begin{frame}
    \addtocounter{framenumber}{-1}
    \tableofcontents
\end{frame}

\section{Just-In-Time compilation}

\begin{frame}{Just-In-Time (JIT) compilation}
    \begin{itemize}
        \item Dynamic languages: \alert{hard to compile} (rely on runtime)
        \item Yet \alert{ubiquitous}: javascript, python, \ldots
        \item Idea: compile \alert{at runtime} the \alert{most used} program
            parts
        \item Used in browsers (JS), PyPy (Python), most JVMs (Java), \ldots
    \end{itemize}

    \vspace{1em}

    \begin{center}
        \begin{tikzpicture}[xscale=0.6, fill=GreenYellow]
            \fill (-8, 0) rectangle (-4, 2)
                node[pos=.5] {Source code};
            \fill (-2, 0) rectangle (2, 2)
                node[pos=.5] {Byte code};
            \fill (4, 0) rectangle (8, 2)
                node[pos=.5, align=center] {Byte/machine\\code};

            \draw[->, line width=2] (-4,1) -- (-2,1);
            \draw[->, line width=2] (2,1) -- (4,1);
            \node [rotate=60, anchor=west] at (-3.75, 1.1) {Bytecode compiler};
            \node [rotate=60, anchor=west] at (2.25, 1.1) {JIT compiler};

            \draw[RubineRed, line width=1] (0, 2) -- (0, 4);
            \draw[RubineRed, line width=1, dotted] (0, 0) -- (0, 2);
            \draw[RubineRed, line width=1] (0, -0.2) -- (0, 0);

            \node [rotate=90, anchor=south, RubineRed] at (-0.1, 3) {Offline};
            \node [rotate=-90, anchor=south, RubineRed] at (0.1, 3) {Runtime};
        \end{tikzpicture}
    \end{center}
\end{frame}

\begin{frame}{How is it done?}
    \begin{itemize}
        \item (In most cases) strong \alert{interaction} interpreter
            $\leftrightarrow$ JIT compiler
            \vspace{1em}
        \item \textit{Article claim}: mostly done using \alert{hot paths}
            within loops (in a single function); most speedup is \alert{type
            specialization}.
            \begin{itemize}
                \item Hot path: path \alert{used $\geq N$ times} at runtime in
                    a \alert{given} (abstract) \alert{store state}
            \end{itemize}
            \pause{}
        \item \alert{Wrong}. But, heh, we'll deal with it nevertheless. \\
            {\small (Inlining, translation to machine code, global
            optimizations, lock elimination, non-volatile-write
            elimination/propagation, \ldots)}
    \end{itemize}
\end{frame}

\section{Study setup}

\begin{frame}{Study objectives}
    \begin{itemize}
        \item Formalism to see JIT as AbsInt (\textit{online source
            transformation})
            \begin{itemize}
                \item Hot path extraction
                \item Type specialization
            \end{itemize}
            \vspace{1em}

        \item Formalism to extract observables from code\\
            $\leadsto$ compare observables with/without JIT\\
            $\leadsto$ prove correctness
            \vspace{1em}

        \item Can be extended with virtually any feature
    \end{itemize}
\end{frame}

\begin{frame}{Studied language}
    \begin{columns}[c]
        \column{0.5\textwidth}
        \begin{itemize}
            \item $\labels$: program labels
            \item $\values$: literal values
            \item $\vars$: variables
            \item $(\progs := \commands \text{ list})$: programs
        \end{itemize}
        \begin{align*}
            C &::= L : A \to L' &\commands \\
            A &::=
                (x := E)\,\vert\,B\,\vert\,\askip &\actions \\
            E, E' &::= v\,\vert\,x\,\vert\,E + E' &\exprs \\
            B, B' &::= \top\,\vert\,\bot\,\vert\,E \leq E' & \bexprs \\
                &\qquad\vert\,\lnot B\,\vert\,B \wedge B'
        \end{align*}

        \column{0.5\textwidth}
        \begin{itemize}
            \item Conditional:
                \begin{align*}
                    l_0&: b_0 \to l_{t} \\
                    l_0&: \lnot b_0 \to l_{f}
                \end{align*}
            \item Turing-complete
            \item Supposed to model some bytecode
        \end{itemize}
    \end{columns}
\end{frame}

\begin{frame}{Types, rough semantics}
    \hspace*{-1em}\textbf{Types \& values}

    \begin{columns}[c]
        \column{0.6\textwidth}
        \begin{itemize}
            \item $\values\,:=\,\relset \cup \set{a, \ldots, z}^\ast$
            \item Types: Int, String, Undef, $\emptyset$, $\Omega$
            \item Undef: error type
        \end{itemize}

        \column{0.4\textwidth}
        \begin{center}
            \begin{tikzpicture}{c}
                \node (E) at (0, 0) {$\emptyset$};
                \node (I) at (-1.5, 1) {Int};
                \node (S) at (0, 1) {String};
                \node (U) at (1.5, 1) {Undef};
                \node (T) at (0, 2) {$\Omega$};
                \draw[->] (E) -- (I);
                \draw[->] (E) -- (S);
                \draw[->] (E) -- (U);
                \draw[<-] (T) -- (I);
                \draw[<-] (T) -- (S);
                \draw[<-] (T) -- (U);
            \end{tikzpicture}
        \end{center}
    \end{columns}

    \vspace{1em}
    \hspace*{-1em}\textbf{Semantics}

    \begin{columns}[c]
        \column{.5\textwidth}

        \begin{itemize}
            \item Type-dependant $+$:
                \begin{itemize}
                    \item $+_{String}$: concatenation
                    \item $+_{Int}$: usual $+$
                    \item $+_{Str, Int}$: yields Undef
                \end{itemize}
        \end{itemize}

        \column{.5\textwidth}
        \begin{align*}
            \stores &:= \vars \to \values & \rho \\
            \states &:= \commands \times \stores & \state{C}{\rho} \\
            \traces &:= \states^\ast
        \end{align*}
    \end{columns}
\end{frame}

\section{Abstract interpretation}

\begin{frame}{AbsInt hot path extraction}
    \begin{itemize}
        \item \textbf{Assertion:} a hot path is necessarily a (whole) loop body
        \item Introduce a function \alert{$\hot{N}$} selecting $N$-hot paths
            from a trace
        \item $\alpha^N_{hot} : \powerset(\traces) \to \powerset(\traces^\#)$
            is an \alert{abstraction}, a corresponding $\gamma$ can be derived
            \vspace{1em}

        \item Note: a $\traces^\#$ \alert{includes} (abstract) \alert{stores},
            allowing optimisations on the hot path
    \end{itemize}
\end{frame}

\begin{frame}{Hot path stitching}
    \begin{itemize}
        \item For $a \in \stores^\#$, introduce \alert{$\guard{a}$} $\in
            \bexprs$, true \ifft{} $\rho \in \gamma(a)$

        \item \alert{Optimized path}: duplicate hot path, guard each operation,
            fallback to original path

        \item Formally define an operator \alert{$\extr{hp}(P)$} extracting the
            hot path $hp$ from the program $P$
            \vspace{1em}

        \item Once the hot path is extracted, it can be \alert{optimized}
            \wrt{} known store restrictions.
    \end{itemize}
\end{frame}

\begin{frame}{Hot path stitching sketch}
    \begin{center}
        \begin{tikzpicture}{c}
            \node [ellipse, fill=CarnationPink] (B0) at (0, 0) {$B_0$};
            \node [rectangle, fill=CarnationPink] (A1) at (3.5, 0) {$A_1$};
            \node [rectangle, fill=CarnationPink] (An) at (8, 0) {$A_n$};
            \draw [dotted, line width=1] (-2, 0) -- (-1.5, 0);
            \draw [->, line width=1] (-1.5, 0) -- (B0);
            \draw [->, line width=1] (B0) -- (A1);
            \draw [->, line width=1, BrickRed] (B0) -- ++ (0, 0.6);
            \draw [->, line width=1] (A1) -- ++ (1, 0);
            \draw [dotted] (A1) ++ (1, 0) -- (An) ++ (-1, 0);
            \draw [<-, line width=1] (An) -- ++ (-1, 0);
            \draw [->, line width=1] (An.south) -- ++ (0, -0.4) -| (B0);
        \end{tikzpicture}

        \vspace{1em}
        {\Huge $\Downarrow$}
        \vspace{1em}

        \begin{tikzpicture}{c}
            \node (Exit) at (-0.2, 2.4) {};

            \node [ellipse, fill=CarnationPink] (B0) at (-0.2, 0) {$B_0$};
            \node [rectangle, fill=CarnationPink] (A1) at (3.5, 0) {$A_1$};
            \node [rectangle, fill=CarnationPink] (An) at (7.5, 0) {$A_n$};
            \draw [->, line width=1] (B0) -- (A1);
            \draw [->, line width=1, BrickRed] (B0) -- (Exit);
            \draw [->, line width=1] (A1) -- ++ (1, 0);
            \draw [dotted] (A1) ++ (1, 0) -- (An) ++ (-1, 0);
            \draw [<-, line width=1] (An) -- ++ (-1, 0);


            \node [ellipse, fill=GreenYellow] (GB0) at (-1.3, 1.5)
                {$\gu{a_0}$};
            \node [ellipse, fill=GreenYellow] (EB0) at (0.5, 1.5) {$B_0$};
            \node [ellipse, fill=GreenYellow] (GA1) at (2.5, 1.5)
                {$\gu{a_1}$};
            \node [rectangle, fill=GreenYellow] (EA1) at (4, 1.5) {$A_1$};
            \node [ellipse, fill=GreenYellow] (GAn) at (6.5, 1.5)
                {$\gu{a_n}$};
            \node [rectangle, fill=GreenYellow] (EAn) at (8, 1.5) {$A_n$};

            \draw [dotted, line width=1] (GB0) -- ++ (-1.3, 0);
            \draw [<-, line width=1] (GB0) -- ++ (-1, 0);

            \draw[->, line width=1] (GB0) -- (EB0);
            \draw[->, line width=1] (EB0) -- (GA1);
            \draw[->, line width=1] (GA1) -- (EA1);
            \draw[->, line width=1] (EA1) -- ++(0.8, 0);
            \draw[dotted, line width=1] (EA1)++(0.8, 0) -- (GAn);
            \draw[<-, line width=1] (GAn) -- ++ (-1.3, 0);
            \draw[->, line width=1] (GAn) -- (EAn);

            \draw[line width=1, BrickRed] (EB0) |- (-0.2, 2);
            \draw[->, line width=1, BrickRed] (GB0) |- (B0);
            \draw[line width=1, BrickRed] (GA1) -- ++ (0, -1.5);
            \draw[line width=1, BrickRed] (GAn) -- ++ (0, -1.5);

            \draw[line width=1] (An.south) -- ++ (0, -0.4) -| (GB0.west);
            \draw[line width=1] (EAn.south) -- ++ (0, -1.9) -| (GB0.west);
        \end{tikzpicture}
    \end{center}
\end{frame}

\begin{frame}{Value type specialization}
    \begin{itemize}
        \item Seen again as \alert{abstract interpretation}: define $\alpha,
            \gamma$.
        \item First, consider \alert{abstract type stores} $\stores^t := \vars
            \to \types$
            \begin{itemize}
                \item Clearly a valid abstract domain for $\stores$
            \end{itemize}

        \item Then, an operator \alert{$\evexpT{E}{\rho}$} $: \exprs \to
            \stores^t \to \types$ typing an expression (possibly to Undef or
            $\Omega$)

        \item Finally, define type specialization \alert{$TS_{hp}$} as the
            substitution in $hp$ of $+$ by its typed alternative, if possible
            \\
            {\small (\ie{} $\evexpT{E + E'}{\rho} \in \set{\text{Int},
            \text{String}}$)}
    \end{itemize}
\end{frame}

\section{Correctness proof}

\begin{frame}{Correctness proof sketch}
    \begin{itemize}
        \item Idea: define (cf. Cousot) correctness of transformation as
            \alert{observational equivalence} of source and transformed
            programs \alert{\wrt{} some abstraction} $\alpha:
            \powerset(\traces) \to \powerset(\stores^\ast)$.
        \item That is, if $\alpha$ derives the abstraction, $\tracesOf$
            extracts the program traces and $Tr$ transforms it, we want
            \[ \alpha(\tracesOf(P)) = \alpha(\tracesOf(Tr(P))) \]
        \item Heavy but safe: $\alpha = \alpha_{sc}$, \alert{store changes}
            \[
                sc(s_1 s_2 \sigma) := \left\{
                    \begin{array}{l l}
                        St(s_1) \cdot sc(s_2 \sigma), &
                            St(s_1) \neq St(s_2) \\
                        sc(s_2 \sigma), &
                            St(s_1) = St(s_2)
                    \end{array}
                    \right.
            \]
        \item Lighter: same, but only at \alert{loop entry/exit points}
    \end{itemize}
\end{frame}

\begin{frame}{Correctness proof sketch, trace extraction}
    \begin{block}{Theorem}
        Trace extraction is correct \wrt{} $\alpha_{sc}$, that is, $\forall P,
        \forall hp$,
        \[ \alpha_{sc}(\tracesOf(P)) = \alpha_{sc}(\tracesOf(\extr{hp}(P))) \]
    \end{block}
    \begin{itemize}
        \item Proved by mapping $\sigma \in \traces$ to its correct trace
            through $tr_{hp}(\sigma)$ in $\extr{hp}(P) =: P_{hp}$

        \item Then show that
            \begin{enumerate}[i]
                \item $tr_{hp}(\tracesOf(P)) \subseteq \tracesOf(P_{hp})$
                \item $\alpha_{sc}(\tracesOf(P_{hp}))
                    \subseteq \alpha_{sc}(\tracesOf(P))$
                \item $\alpha_{sc} \circ tr_{hp} = \alpha_{sc}$
            \end{enumerate}
    \end{itemize}
\end{frame}

\begin{frame}{Correctness proof sketch, type specialization}
    \begin{block}{Theorem}
        Type specialization is correct (at traces level)
    \end{block}

    \begin{itemize}
        \item Define $tt(\sigma)$ erasing type specialization (\eg{}
            $+_{\text{Int}} \mapsto +$).
        \item Then, $tt(\tracesOf(TS_{hp}(stitch_P(hp)))) =
            \tracesOf(stitch_P(hp))$
    \end{itemize}

    \begin{block}{Theorem}
        Stitching type specialization to a hot path is correct \wrt{}
        $\alpha_{sc}$.
    \end{block}

    (directly follows)
\end{frame}

\section*{}

\begin{frame}[shrink]{Conclusion}
    \begin{columns}[c]
        \column{.8 \textwidth}
        \begin{exampleblock}{Pros}
            \begin{itemize}
                \item Opens the way for \alert{AbsInt formalism} in JIT
                \item Provides an (implemented?) \alert{framework} for JIT
                    study
            \end{itemize}
        \end{exampleblock}

        \begin{alertblock}{Cons}
            \begin{itemize}
                \item \alert{Overly restrictive} in JIT features,
                    \alert{pretends otherwise}
                \item Unusably \alert{small toy language}
                \item Absurdly \alert{hard to read} toy language
                \item Proof \wrt{} some $\alpha$ which does not handle effects
                \item Please, stop claiming every line or two that your paper
                    is better than Guo and Palsberg's
            \end{itemize}
        \end{alertblock}

        \column{.2 \textwidth}
        \begin{figure}
            \centering
            \hspace*{-1em}
            \includegraphics[width=1.4\textwidth]{img/absint.jpg}
        \end{figure}
    \end{columns}
\end{frame}

\end{document}