Add hot path stitching
This commit is contained in:
parent
7ad40c8cf3
commit
a91d6a3075
2 changed files with 99 additions and 2 deletions
3
math.sty
3
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$}}
|
||||
|
|
|
|||
98
slides.tex
98
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]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue