# HG changeset patch # User Christian Urban # Date 1352798970 0 # Node ID 2522dea979d03056674a40b00469bfddef67537f # Parent 2895a7550754c445b4dc2d464f3a662ad8d9cb18 updated diff -r 2895a7550754 -r 2522dea979d0 slides07.pdf Binary file slides07.pdf has changed diff -r 2895a7550754 -r 2522dea979d0 slides07.tex --- a/slides07.tex Tue Nov 13 09:05:52 2012 +0000 +++ b/slides07.tex Tue Nov 13 09:29:30 2012 +0000 @@ -17,6 +17,8 @@ \usepackage{graphicx} \usetikzlibrary{shapes} \usetikzlibrary{shadows} +\usetikzlibrary{plotmarks} + \isabellestyle{rm} \renewcommand{\isastyle}{\rm}% @@ -94,6 +96,124 @@ \renewcommand{\slidecaption}{APP 07, King's College London, 13 November 2012} \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions \newcommand{\bl}[1]{\textcolor{blue}{#1}} + + +% The data files, written on the first run. +\begin{filecontents}{re-python.data} +1 0.029 +5 0.029 +10 0.029 +15 0.032 +16 0.042 +17 0.042 +18 0.055 +19 0.084 +20 0.136 +21 0.248 +22 0.464 +23 0.899 +24 1.773 +25 3.505 +26 6.993 +27 14.503 +28 29.307 +#29 58.886 +\end{filecontents} + +\begin{filecontents}{re1.data} +1 0.00179 +2 0.00011 +3 0.00014 +4 0.00026 +5 0.00050 +6 0.00095 +7 0.00190 +8 0.00287 +9 0.00779 +10 0.01399 +11 0.01894 +12 0.03666 +13 0.07994 +14 0.08944 +15 0.02377 +16 0.07392 +17 0.22798 +18 0.65310 +19 2.11360 +20 6.31606 +21 21.46013 +\end{filecontents} + +\begin{filecontents}{re2.data} +1 0.00240 +2 0.00013 +3 0.00020 +4 0.00030 +5 0.00049 +6 0.00083 +7 0.00146 +8 0.00228 +9 0.00351 +10 0.00640 +11 0.01217 +12 0.02565 +13 0.01382 +14 0.02423 +15 0.05065 +16 0.06522 +17 0.02140 +18 0.05176 +19 0.18254 +20 0.51898 +21 1.39631 +22 2.69501 +23 8.07952 +\end{filecontents} + +\begin{filecontents}{re-internal.data} +1 0.00069 +301 0.00700 +601 0.00297 +901 0.00470 +1201 0.01301 +1501 0.01175 +1801 0.01761 +2101 0.01787 +2401 0.02717 +2701 0.03932 +3001 0.03470 +3301 0.04349 +3601 0.05411 +3901 0.06181 +4201 0.07119 +4501 0.08578 +\end{filecontents} + +\begin{filecontents}{re3.data} +1 0.001605 +501 0.131066 +1001 0.057885 +1501 0.136875 +2001 0.176238 +2501 0.254363 +3001 0.37262 +3501 0.500946 +4001 0.638384 +4501 0.816605 +5001 1.00491 +5501 1.232505 +6001 1.525672 +6501 1.757502 +7001 2.092784 +7501 2.429224 +8001 2.803037 +8501 3.463045 +9001 3.609 +9501 4.081504 +10001 4.54569 +\end{filecontents} + + \begin{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -409,6 +529,122 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}[c] + \frametitle{Priority Inheritance Protocol} + + \begin{itemize} + \item an algorithm that is widely used in real-time operating systems + \item hash been ``proved'' correct by hand in a paper in 1983 + \item but the first algorithm turned out to be incorrect, despite the ``proof''\bigskip\pause + + \item we specified the algorithm and then proved that the specification makes + ``sense'' + \item we implemented our specification in C on top of PINTOS (Stanford) + \item our implementation was much more efficient than their reference implementation + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\mode{ +\begin{frame}[c] +\frametitle{Regular Expression Matching} +\tiny + +\begin{tabular}{@ {\hspace{-6mm}}cc} +\begin{tikzpicture}[y=.1cm, x=.15cm] + %axis + \draw (0,0) -- coordinate (x axis mid) (30,0); + \draw (0,0) -- coordinate (y axis mid) (0,30); + %ticks + \foreach \x in {0,5,...,30} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \foreach \y in {0,5,...,30} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + %labels + \node[below=0.3cm] at (x axis mid) {\bl{a}s}; + \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; + + %plots + \draw[color=blue] plot[mark=*, mark options={fill=white}] + file {re-python.data}; + \only<1->{ + \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] + file {re1.data};} + \only<1->{ + \draw[color=green] plot[mark=square*, mark options={fill=white} ] + file {re2.data};} + + %legend + \begin{scope}[shift={(4,20)}] + \draw[color=blue] (0,0) -- + plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\footnotesize Python}; + \only<1->{\draw[yshift=6mm, color=red] (0,0) -- + plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\footnotesize Scala V1};} + \only<1->{ + \draw[yshift=12mm, color=green] (0,0) -- + plot[mark=square*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\footnotesize Scala V2 with simplifications};} + \end{scope} +\end{tikzpicture} & + +\begin{tikzpicture}[y=.35cm, x=.00045cm] + %axis + \draw (0,0) -- coordinate (x axis mid) (10000,0); + \draw (0,0) -- coordinate (y axis mid) (0,6); + %ticks + \foreach \x in {0,2000,...,10000} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \foreach \y in {0,1,...,6} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + %labels + \node[below=0.3cm] at (x axis mid) {\bl{a}s}; + \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; + + %plots + \draw[color=blue] plot[mark=*, mark options={fill=white}] + file {re-internal.data}; + \only<1->{ + \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] + file {re3.data};} + + %legend + \begin{scope}[shift={(2000,4)}] + \draw[color=blue] (0,0) -- + plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\footnotesize Scala Internal}; + \only<1->{ + \draw[yshift=6mm, color=red] (0,0) -- + plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) + node[right]{\footnotesize Scala V3};} + \end{scope} +\end{tikzpicture} +\end{tabular}\bigskip\pause +\normalsize +\begin{itemize} +\item I needed a proof in order to make sure my program is correct +\end{itemize}\pause + +\begin{center} +\bl{End Digression.\\ (Our small proof is 0.0005\% of the OS-proof.)} +\end{center} + +\end{frame}} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}[c] \frametitle{Trusted Third Party}