453 lines
16 KiB
TeX
453 lines
16 KiB
TeX
% 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}
|