
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<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}




