--- 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<presentation>{
+ \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<presentation>{
+\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<presentation>{
\begin{frame}[c]
\frametitle{Trusted Third Party}