From a91d6a307564e519b0ba871ad18dfa3fd9197189 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sun, 4 Mar 2018 22:33:53 +0100
Subject: [PATCH] Add hot path stitching

---
 math.sty   |  3 ++
 slides.tex | 98 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 99 insertions(+), 2 deletions(-)

diff --git a/math.sty b/math.sty
index 8ec1567..faa1ac1 100644
--- a/math.sty
+++ b/math.sty
@@ -41,6 +41,7 @@
 \newcommand{\natset}{\mathbb{N}}
 \newcommand{\relset}{\mathbb{Z}}
 \newcommand{\funcspace}{\mathcal{F}}
+\newcommand{\powerset}{\mathcal{P}}
 
 % Probas
 \newcommand{\prob}{\mathbb{P}}
@@ -65,6 +66,8 @@
 
 \newcommand{\argmin}{\operatorname{argmin}}
 
+\newcommand{\ifft}{\textit{iff.}}
+
 
 % Preuve par équivalence - puces
 \newcommand{\impliesbullet}{\ovalbox{$\implies$}}
diff --git a/slides.tex b/slides.tex
index 70b7ee3..a246622 100644
--- a/slides.tex
+++ b/slides.tex
@@ -12,6 +12,7 @@
 \usepackage{my_listings}
 \usepackage{math}
 \usepackage{tikz}
+\usetikzlibrary{shapes, arrows}
 \setbeamertemplate{navigation symbols}{}
 
 \newcommand{\wrt}{\textit{wrt.}}
@@ -29,6 +30,11 @@
 \newcommand{\states}{\operatorname{State}}
 \newcommand{\traces}{\operatorname{Trace}}
 \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*\oldmacro{}%
 \let\oldmacro\insertshorttitle%
@@ -223,7 +229,95 @@
 \section{Abstract interpretation}
 
 \begin{frame}{AbsInt hot path extraction}
-    %TODO
+    \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$
+    \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}
@@ -236,7 +330,7 @@
     %TODO
 \end{frame}
 
-\section*{Conclusion}
+\section*{}
 
 \begin{frame}[shrink]{Conclusion}
     \begin{columns}[c]