summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tex/presentation/Makefile28
-rw-r--r--tex/presentation/presentation.pdfbin0 -> 175078 bytes
-rw-r--r--tex/presentation/presentation.tex336
-rw-r--r--tex/presentation/references.bib156
4 files changed, 520 insertions, 0 deletions
diff --git a/tex/presentation/Makefile b/tex/presentation/Makefile
new file mode 100644
index 0000000..0d171d7
--- /dev/null
+++ b/tex/presentation/Makefile
@@ -0,0 +1,28 @@
+all: presentation.pdf
+
+.PHONY: remote clean
+remote:
+ ssh honours "mkdir -p tmp/tex/presentation"
+ rm -f presentation.pdf
+ rsync -r . "honours:tmp/tex/presentation"
+ ssh honours "cd tmp/tex/presentation; make clean; make"
+ scp "honours:tmp/tex/presentation/presentation.pdf" .
+
+presentation.pdf: presentation.tex
+ pdflatex presentation
+ bibtex presentation
+ pdflatex presentation
+ pdflatex presentation
+
+clean:
+ rm -f `find . -name '*.log'`
+ rm -f `find . -name '*.dvi'`
+ rm -f `find . -name '*.ps'`
+ rm -f `find . -name '*.aux'`
+ rm -f `find . -name '*.blg'`
+ rm -f `find . -name '*.bbl'`
+ rm -f `find . -name '*.toc'`
+ rm -f `find . -name '*.lof'`
+ rm -f `find . -name '*.lot'`
+ rm -f `find . -name '*.out'`
+ rm -f `find . -name '*~'`
diff --git a/tex/presentation/presentation.pdf b/tex/presentation/presentation.pdf
new file mode 100644
index 0000000..f19baee
--- /dev/null
+++ b/tex/presentation/presentation.pdf
Binary files differ
diff --git a/tex/presentation/presentation.tex b/tex/presentation/presentation.tex
new file mode 100644
index 0000000..914ba66
--- /dev/null
+++ b/tex/presentation/presentation.tex
@@ -0,0 +1,336 @@
+\documentclass{beamer}
+
+\title{Implementing and Evaluating a Strategy-Iteration Based Static Analyser within the LLVM framework}
+\author{Carlo Zancanaro}
+\def\sid{309222257}
+\def\supervisor{Bernhard Scholz}
+
+\usepackage[numbers]{natbib}
+\usepackage{mdframed}
+\usepackage{algorithmicx}
+\usepackage{tikz}
+\usepackage{pgfplots}
+\pgfplotsset{compat=1.4}
+\algblockx[While]{While}{EndWhile}{\textbf{while}~}{\textbf{endwhile}}
+
+\newcommand\Z{\mathbb{Z}}
+\newcommand\CZ{\overline{\Z}}
+\def\newblock{\hskip .11em plus .33em minus .07em} % important line
+
+\begin{document}
+
+\begin{frame}
+ \maketitle
+\end{frame}
+
+\section{Introduction}
+\begin{frame}{Bugs are bad}
+ \begin{itemize}
+ \item<1->
+ Money - recently Knight Capital, US\$440 million lost in a day
+ \item<2->
+ Time - 50\% of development time is spent debugging\cite{debugging-book}
+ \item<3->
+ Security - buffer overflows and other security flaws
+ \item<4->
+ Lives - X-ray machines, helicopters, cars
+ \end{itemize}
+\end{frame}
+\begin{frame}{Static analysis is good}
+ \begin{itemize}
+ \item<1->
+ The more bugs we can catch at compile time, the better
+ \item<2->
+ We can't catch all bugs - Rice's theorem\cite{Rice}
+ \end{itemize}
+\end{frame}
+
+\section{Prior work}
+\begin{frame}[fragile]{Modelling programs}
+ \begin{center}
+ \begin{mdframed}
+ \begin{algorithmic}
+ \State $x = 0$
+ \State $y = 1$
+ \While {$x < 8$}
+ \Comment{value at start of this line}
+ \State $x = x + 2$
+ \State $y = y + 2$
+ \EndWhile
+ \end{algorithmic}
+ \end{mdframed}
+ \end{center}
+ \begin{align*}
+ \only<1>{~ \\ ~}
+ \only<2>{x &= \{0\} \\ y &= \{1\}}
+ \only<3>{x &= \{0, 2\} \\ y &= \{1, 3\}}
+ \only<4>{x &= \{0, 2, 4\} \\ y &= \{1, 3, 5\}}
+ \only<5>{x &= \{0, 2, 4, 6\} \\ y &= \{1, 3, 5, 7\}}
+ \only<6>{x &= \{0, 2, 4, 6, 8\} \\ y &= \{1, 3, 5, 7, 9\}}
+ \end{align*}
+\end{frame}
+
+\begin{frame}{Abstract interpretation}
+ Basic idea: simplify your domain
+
+ Instead of arbitrary subsets of $\Z$, something less precise:
+
+ \begin{itemize}
+ \item
+ signs\cite{CousotCousot77-1}: $x \in \{ \Z, \Z^+, \Z^-, 0\}$
+ \item
+ ranges\cite{CousotCousot77-1}: $x \le a; -x \le b, ~a,b \in \Z$
+ \item
+ zones\cite{mine:padoII}: $x - y \le c; \pm x \le c ~c \in Z$
+ \end{itemize}
+\end{frame}
+\begin{frame}[fragile]{Abstract interpretation}
+ \begin{figure}
+ \begin{tikzpicture}[scale=0.6,dot/.style={circle,fill,inner sep=1pt}]
+ \draw (0,0) -- coordinate (x axis mid) (10,0);
+ \draw (0,0) -- coordinate (y axis mid) (0,10);
+
+ \foreach \x in {0,...,10}
+ \draw (\x,1pt) -- (\x,-3pt)
+ node[anchor=north] {\x};
+ \node[anchor=west] at (10,0) {$x$};
+ \foreach \y in {0,...,10}
+ \draw (1pt,\y) -- (-3pt,\y)
+ node[anchor=east] {\y};
+ \node[anchor=south] at (0,10) {$y$};
+
+ \foreach \v in {0,...,4}
+ \node [dot,radius=0.2pt] at (0 + 2*\v,1 + 2*\v) { };
+
+ \draw [draw=black, fill=gray, fill opacity=0.2]
+ (0,1) -- (0,9) -- (8,9) -- (8,1) -- (0,1);
+ \end{tikzpicture}
+ \caption{Comparison between concrete and abstract domains}
+ \end{figure}
+\end{frame}
+
+\begin{frame}{$\max$-strategy improvement}
+ \begin{itemize}
+ \item
+ Transform a program into equations
+ \item
+ Solve equations
+ \end{itemize}
+\end{frame}
+
+\begin{frame}[fragile]{$\max$-strategy example}
+ \begin{center}
+ \begin{mdframed}
+ \begin{algorithmic}
+ \State $x = 0$
+ \Comment $A$
+ \While {$x \le 8$} \Comment $B$
+ \State $x = x + 2$
+ \EndWhile
+ \State print$(x)$ \Comment $C$
+ \end{algorithmic}
+ \end{mdframed}
+ \end{center}
+ \alt<1>{\begin{align*}
+ ub(x)_A &\ge \infty \\
+ ub(x)_B &\ge 0 \\
+ ub(x)_B &\ge \min(ub(x)_B, 8) + 2 \\
+ ub(x)_C &\ge ub(x)_B
+ \end{align*}
+ }{\begin{align*}
+ ub(x)_A &= \infty \\
+ ub(x)_B &= \max(0, \min(ub(x)_B, 8) + 2) \\
+ ub(x)_C &= ub(x)_B \\
+ ~
+ \end{align*}}
+ \only<2>{}
+\end{frame}
+
+\begin{frame}[fragile]{$\max$-strategies}
+ A $\max$-strategy is a decision about which argument in a
+ $\max$-expression to choose.
+ \begin{align*}
+ ub(x)_A &= \infty \\
+ ub(x)_B &= \max(\alert<2>{0}, \alert<3>{\min(ub(x)_B, 8) + 2}) \\
+ ub(x)_C &= ub(x)_B
+ \end{align*}
+\end{frame}
+
+\begin{frame}[fragile]{Solver}
+ \begin{figure}
+ \begin{tikzpicture}
+ \node [rectangle, draw, align=center](max) at (0,0) {Maximiser \\ improve strategy};
+ \node [rectangle, draw, align=center](min) at (0,-3) {Minimiser \\ find assignment};
+
+ \path[]
+ (min) edge[bend left,arrows={-latex}]
+ node[anchor=east]{variable assignment}
+ (max)
+
+ (max) edge[bend left,arrows={-latex}]
+ node[anchor=west]{$\max$-strategy}
+ (min);
+ \end{tikzpicture}
+ \caption{The high-level structure of the solver presented in
+ \cite{Gawlitza:2007:PFC:1762174.1762203}}
+ \end{figure}
+\end{frame}
+
+\section{Contribution}
+\begin{frame}[fragile]{Solver - enhancements}
+ The big idea: take into account data-dependencies
+ \begin{align*}
+ \alert<4>{x} &\alert<4>{= \max(0, \min(x - 1, \alert<3>{y}))} \\
+ \alert<2-4>{y} &= \max(0, x + 5, x) \\
+ z &= \max(0, z + 1, x)
+ \end{align*}
+\end{frame}
+
+\begin{frame}[fragile]{Solver - enhancements}
+ \begin{figure}
+ \begin{tikzpicture}
+ \node [rectangle, draw, align=center](max) at (0,0) {Maximiser \\ improve strategy};
+ \node [rectangle, draw, align=center](min) at (0,-3) {Minimiser \\ find assignment};
+
+ \path[]
+ (min) edge[bend left,arrows={-latex}]
+ node[anchor=east,align=right]{variable assignment \\ change set}
+ (max)
+
+ (max) edge[bend left,arrows={-latex}]
+ node[anchor=west,align=left]{$\max$-strategy \\ change set}
+ (min);
+ \end{tikzpicture}
+ \caption{The high-level structure of our enhanced solver}
+ \end{figure}
+\end{frame}
+
+\section{Results}
+\begin{frame}{Implementation}
+ \begin{itemize}
+ \item
+ Implemented in C++
+ \item
+ Integrated into the LLVM/Clang static analysis framework
+ \end{itemize}
+\end{frame}
+
+\begin{frame}{Example system}
+ \begin{align*}
+ x_0 &= \max(-\infty, 0) \\
+ x_1 &= \max(-\infty, x_0) \\
+ x_2 &= \max(-\infty, x_1) \\
+ ... &~ ... \\
+ x_n &= \max(-\infty, x_{n-1})
+ \end{align*}
+\end{frame}
+
+\begin{frame}{Runtime improvements}
+ \begin{figure}
+ \begin{tikzpicture}
+ \begin{loglogaxis}[%
+ scale only axis,
+ width=9cm,
+ height=5cm,
+ xmin=1, xmax=65536,
+ xlabel=size of equation system,
+ ymin=0, ymax=40,
+ ylabel=time (in seconds),
+ axis on top]
+ \addplot[
+ ybar,
+ bar width=0.5cm,
+ bar shift=0in,
+ fill=red,
+ draw=black]
+ plot coordinates{
+ (1,0.000021982 )
+ (2,0.000037083 )
+ (4,0.000090918 )
+ (8,0.000331411 )
+ (16,0.001678790 )
+ (32,0.010238535 )
+ (64,0.069774912 )
+ (128,0.520062180 )
+ (256,3.983806321 )
+ (512,31.469653195 )
+ };
+
+ \end{loglogaxis}
+ \end{tikzpicture}
+ \caption{Performance of the naive algorithm}
+ \end{figure}
+\end{frame}
+
+\begin{frame}{Runtime improvements}
+ \begin{figure}
+ \begin{tikzpicture}
+ \begin{loglogaxis}[%
+ scale only axis,
+ width=9cm,
+ height=5cm,
+ xmin=1, xmax=65536,
+ xlabel=size of equation system,
+ ymin=0, ymax=40,
+ ylabel=time (in seconds),
+ axis on top]
+ \addplot[
+ ybar,
+ bar width=0.5cm,
+ bar shift=0in,
+ fill=red,
+ draw=black]
+ plot coordinates{
+ (1,0.000044508 )
+ (2,0.000063953 )
+ (4,0.000094303 )
+ (8,0.000176679 )
+ (16,0.000312958 )
+ (32,0.000642421 )
+ (64,0.001194996 )
+ (128,0.002451839 )
+ (256,0.004786286 )
+ (512,0.009280946 )
+ (1024,0.019159827 )
+ (2048,0.038067689 )
+ (4096,0.080535540 )
+ (8192,0.151181571 )
+ (16384,0.339113750 )
+ (32768,0.593622054 )
+ (65536,1.217525509 )
+ };
+
+ \end{loglogaxis}
+ \end{tikzpicture}
+ \caption{Performance of our improved algorithm}
+ \end{figure}
+\end{frame}
+
+\section{Future work}
+\begin{frame}{Future work}
+ \begin{itemize}
+ \item
+ Still slightly over-approximating dependencies
+ \item
+ LLVM/Clang integration is only a proof-of-concept
+ \end{itemize}
+\end{frame}
+
+\begin{frame}[fragile,allowframebreaks]{References}
+ \phantomsection
+ \bibliographystyle{abbrvnat}
+ \bibliography{references}
+\end{frame}
+
+\begin{frame}{Contributions}
+ \begin{itemize}
+ \item
+ Improvement of $\max$-strategy iteration algorithm, leveraging
+ sparsity of variable dependencies
+ \item
+ Implementation of a $\max$-strategy iteration based static
+ analyser in the LLVM/Clang framework
+ \end{itemize}
+\end{frame}
+
+\end{document}
diff --git a/tex/presentation/references.bib b/tex/presentation/references.bib
new file mode 100644
index 0000000..29f2972
--- /dev/null
+++ b/tex/presentation/references.bib
@@ -0,0 +1,156 @@
+@article{DBLP:tr/trier/MI96-11,
+ author = {Christian Fecht and
+ Helmut Seidl},
+ title = {An Even Faster Solver for General Systems of Equations},
+ journal = {Universit{\"a}t Trier, Mathematik/Informatik, Forschungsbericht},
+ volume = {96-11},
+ year = {1996},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@inproceedings{CousotCousot77-1,
+ author = {Cousot, P{.} and Cousot, R{.}},
+ title = {Abstract interpretation: a unified lattice model for static
+ analysis of programs by construction or approximation of
+ fixpoints},
+ pages = {238--252},
+ booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT
+ Symposium on Principles of Programming Languages},
+ address = {Los Angeles, California},
+ publisher = {ACM Press, New York, NY},
+ year = 1977,
+}
+@article{mine:hosc06,
+ author = {Min\'e, A{.}},
+ title = {The Octagon Abstract Domain},
+ journal = {Higher-Order and Symbolic Computation},
+ editor = {O. Danvy},
+ publisher = {Springer},
+ year = {2006},
+ volume = {19},
+ number = {1},
+ pages = {31--100},
+ note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf}}
+}
+@inproceedings{mine:padoII,
+ author = {Min\'e, A{.}},
+ title = {A New Numerical Abstract Domain Based on Difference-Bound Matrices},
+ booktitle = {Proc. of the 2d Symp. on Programs as Data Objects (PADO II)},
+ series = {Lecture Notes in Computer Science},
+ year = {2001},
+ month = {May},
+ pages = {155--172},
+ volume = {2053},
+ publisher = {Springer},
+ location = {Aarhus, Danemark},
+ note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-padoII.pdf}}
+}
+@inproceedings{DBLP:conf/vmcai/SankaranarayananSM05,
+ author = {Sriram Sankaranarayanan and
+ Henny B. Sipma and
+ Zohar Manna},
+ title = {Scalable Analysis of Linear Systems Using Mathematical Programming},
+ booktitle = {VMCAI},
+ year = {2005},
+ pages = {25-41},
+ ee = {http://dx.doi.org/10.1007/978-3-540-30579-8_2},
+ bibsource = {DBLP, http://dblp.uni-trier.de}
+}
+@inproceedings{Dor:2001:CCS:647170.718291,
+ author = {Dor, Nurit and Rodeh, Michael and Sagiv, Shmuel},
+ title = {Cleanness Checking of String Manipulations in C Programs via
+ Integer Analysis},
+ booktitle = {Proceedings of the 8th International Symposium on Static
+ Analysis},
+ series = {SAS '01},
+ year = {2001},
+ isbn = {3-540-42314-1},
+ pages = {194--212},
+ numpages = {19},
+ url = {http://dl.acm.org/citation.cfm?id=647170.718291},
+ acmid = {718291},
+ publisher = {Springer-Verlag},
+ address = {London, UK, UK},
+}
+@INPROCEEDINGS{Yovine98modelchecking,
+ author = {Sergio Yovine},
+ title = {Model checking timed automata},
+ booktitle = {In European Educational Forum: School on Embedded
+ Systems},
+ year = {1998},
+ pages = {114--152},
+ publisher = {Springer-Verlag}
+}
+@inproceedings{Gawlitza:2007:PFC:1762174.1762203,
+ author = {Gawlitza, Thomas and Seidl, Helmut},
+ title = {Precise fixpoint computation through strategy iteration},
+ booktitle = {Proceedings of the 16th European conference on Programming},
+ series = {ESOP'07},
+ year = {2007},
+ isbn = {978-3-540-71314-2},
+ location = {Braga, Portugal},
+ pages = {300--315},
+ numpages = {16},
+ url = {http://dl.acm.org/citation.cfm?id=1762174.1762203},
+ acmid = {1762203},
+ publisher = {Springer-Verlag},
+ address = {Berlin, Heidelberg},
+}
+@article{tarski,
+ author = {Tarski, Alfred},
+ title = {A lattice-theoretical fixpoint theorem and its
+ applications.},
+ year = {1955}
+}
+@incollection {springerlink,
+ author = {Christensen, Aske and Mø, Anders and Schwartzbach, Michael},
+ affiliation = {BRICS Denmark},
+ title = {Precise Analysis of String Expressions},
+ booktitle = {Static Analysis},
+ series = {Lecture Notes in Computer Science},
+ editor = {Cousot, Radhia},
+ publisher = {Springer Berlin / Heidelberg},
+ isbn = {978-3-540-40325-8},
+ keyword = {Computer Science},
+ pages = {1076-1076},
+ volume = {2694},
+ year = {2003}
+}
+% http://www.mrtc.mdh.se/projects/wcet/benchmarks.html
+@InProceedings{Gustafsson:WCET2010:Benchmarks,
+ author = {Jan Gustafsson and Adam Betts and Andreas Ermedahl and Bj{\"{o}}rn Lisper},
+ title = {The {M{\"a}lardalen} {WCET} Benchmarks -- Past, Present and Future},
+ booktitle = WCET2010,
+ OPTcrossref = {},
+ OPTkey = {},
+ pages = {137--147},
+ year = {2010},
+ editor = {Bj{\"o}rn Lisper},
+ OPTvolume = {},
+ OPTnumber = {},
+ OPTseries = {},
+ address = {Brussels, Belgium},
+ month = jul,
+ OPTorganization = {},
+ publisher = {OCG},
+ OPTnote = {},
+ OPTannote = {}
+}
+@misc{fixpoint-slides,
+ author = {Helmut Seidl},
+ title = {Lecture Slides in Program Optimisation},
+ url = {http://www2.in.tum.de/~seidl/Courses/WS2011/Optimierung/all2011.pdf},
+ urldate = {2012-11-04},
+ year = {2011}
+}
+@article{Rice,
+ author = {H. Rice},
+ title = {Classes of Recursively Enumerable Sets and their
+ Decision problems},
+ year = {1953},
+ journal = {Transactions of the American Mathematical Society},
+ volume = {83}
+}
+@book{debugging-book,
+ title = {Why Programs Fail: A Guide to Systematic Debugging},
+ author = {Andreas Zeller}
+}