\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{slides}
\usepackage{langs}
\usepackage{graph}
%\usepackage{grammar}
\usepackage{soul}
\usepackage{data}
\usepackage{proof}

% beamer stuff 
\renewcommand{\slidecaption}{Canterbury, 22.2.2016}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\newcommand\grid[1]{%
\begin{tikzpicture}[baseline=(char.base)]
  \path[use as bounding box]
    (0,0) rectangle (1em,1em);
  \draw[red!50, fill=red!20]
    (0,0) rectangle (1em,1em);
  \node[inner sep=1pt,anchor=base west]
    (char) at (0em,\gridraiseamount) {#1};
\end{tikzpicture}}
\newcommand\gridraiseamount{0.12em}

\makeatletter
\newcommand\Grid[1]{%
  \@tfor\z:=#1\do{\grid{\z}}}
\makeatother	

\newcommand\Vspace[1][.3em]{%
  \mbox{\kern.06em\vrule height.3ex}%
  \vbox{\hrule width#1}%
  \hbox{\vrule height.3ex}}

\def\VS{\Vspace[0.6em]}



\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\
  \Large POSIX Lexing with Derivatives\\[-1.5mm] 
  \Large of Regular Expressions\\[-1mm] 
  %\normalsize Or, How to Find Bugs with the\\[-5mm] 
  %\normalsize Isabelle Theorem Prover
  \end{tabular}}\bigskip\bigskip\bigskip

  \normalsize
  \begin{center}
  \begin{tabular}{c}
  \small Christian Urban\\
  \small King's College London\\
  \\
  \\
  Joint work with Fahad Ausaf and Roy Dyckhoff
  \end{tabular}
  \end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.2]{isabelle.png}
  \end{center}
  \mbox{}\\[-20mm]\mbox{}

  \begin{itemize}
  \item Isabelle interactive theorem prover; 
  some proofs are automatic -- most however need help
  \item the learning curve is steep; you often have to fight the 
  theorem prover\ldots no different in other ITPs
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Why Bother?}

Surely regular expressions must have been implemented and 
studied to death, no?

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={{\tt a}s},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,5,...,30},
    xmax=30,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=8cm,
    height=6cm, 
    legend entries={Python,Ruby},  
    legend pos=north west,
    legend cell align=left  
]
\addplot[blue,mark=*, mark options={fill=white}] 
  table {re-python.data};
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
  table {re-ruby.data};  
\end{axis}
\end{tikzpicture}
\end{center}

evil regular expressions: \bl{$({\tt a}?)^n \cdot {\tt a}^n$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\Large Isabelle Theorem Prover}

\begin{itemize}
\item started to use Isabelle after my PhD (in 2000)

\item the thesis included a rather complicated 
  ``pencil-and-paper'' proof for a 
  termination argument (sort of $\lambda$-calculus)\medskip
 
\item me, my supervisor, the examiners did not find any problems\medskip 
 \begin{center}
  \begin{tabular}{@ {}c@ {}}
  \includegraphics[scale=0.38]{barendregt.jpg}\\[-2mm]
  \footnotesize Henk Barendregt
  \end{tabular}
  \hspace{2mm}
  \begin{tabular}{@ {}c@ {}}
  \includegraphics[scale=0.20]{andrewpitts.jpg}\\[-2mm]
  \footnotesize Andrew Pitts
  \end{tabular}
  \end{center}
  
\item people were building their work on my result      
  
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{\Large Nominal Isabelle}

\begin{itemize}
\item implemented a package for the Isabelle prover 
in order to reason conveniently about binders 
 
\begin{center}
\large\bl{$\lambda \alert{x}.\,M$} \hspace{10mm}
\bl{$\forall \alert{x}.\,P\,x$}
\end{center}\bigskip\bigskip\bigskip\bigskip
\bigskip\bigskip\bigskip\pause\pause
  
  
\item when finally being able to formalise the proof from my PhD, I found that the main result
      (termination) is correct, but a central lemma needed to
      be generalised
\end{itemize}

\only<2->{
\begin{textblock}{3}(13,5)
\includegraphics[scale=0.33]{skeleton.jpg}
\end{textblock}}

\begin{textblock}{3}(5.3,7)
\onslide<1->{
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};
\end{tikzpicture}}
\end{textblock}

\begin{textblock}{3}(8.7,7)
\onslide<1->{
\begin{tikzpicture}
\node at (0,0) [single arrow, shape border rotate=90, fill=red,text=red]{\mbox{a}};
\end{tikzpicture}}
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\Large Variable Convention}


\begin{center}
\begin{bubble}[10cm]
  \color{gray}  
  \small
  {\bf\mbox{}Variable Convention:}\\[1mm] 
  If $M_1,\ldots,M_n$ occur in a certain mathematical context
  (e.g. definition, proof), then in these terms all bound variables 
  are chosen to be different from the free variables.\\[2mm]
  
  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
\end{bubble}
\end{center}

\mbox{}\\[-8mm]
\begin{itemize}


\item instead of proving a property for \alert{\bf all} bound
variables, you prove it only for \alert{\bf some}\ldots?

\item feels like it is used in 90\% of papers in PT and FP
(9.9\% use de-Bruijn indices)

\item this is mostly OK, but in some corner-cases you can use it
to prove \alert{\bf false}\ldots we fixed this!
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
\begin{frame}[c]
\frametitle{}

\begin{tabular}{c@ {\hspace{2mm}}c}
\\[6mm]
\begin{tabular}{c}
\includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
{\footnotesize Bob Harper}\\[-2mm]
{\footnotesize}
\end{tabular}
\begin{tabular}{c}
\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
{\footnotesize Frank Pfenning}\\[-2mm]
{\footnotesize}
\end{tabular} &

\begin{tabular}{p{6cm}}
\raggedright
{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
$\sim$31pp}
\end{tabular}\\

\\[0mm]
  
\begin{tabular}{c}
\includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
{\footnotesize Andrew Appel}\\[-2.5mm]
{\footnotesize}
\end{tabular} &

\begin{tabular}{p{6cm}}
\raggedright
{relied on their proof in a\\ {\bf security} critical application}
\end{tabular}
\end{tabular}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}
\frametitle{Proof-Carrying Code}

\begin{textblock}{10}(2.5,2.2)
\begin{block}{Idea:}
\begin{center}
\begin{tikzpicture}
\draw[help lines,cream] (0,0.2) grid (8,4);
  
\draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
\node[anchor=base] at (6.5,2.8) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user: untrusted code\end{tabular}};

\draw[line width=1mm, red] (0.1,0.6) rectangle (2.1,4);
  \node[anchor=base] at (1.1,2.3) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  developer ---\\ web server\end{tabular}};
  
\onslide<3->{
  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
  \node[anchor=base,white] at (6.5,1.1) 
     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

  \node at (3.6,3.0) [single arrow, fill=red,text=white, 
                      minimum height=3.4cm]{\bf code};
  \onslide<2->{
  \node at (3.6,1.3) [single arrow, fill=red,text=white, 
                      minimum height=3.4cm]{\bf certificate};
  \node at (3.6,1.9) {\small\color{gray}{\mbox{}\hspace{-1mm}a proof in LF}};
}

  
\end{tikzpicture}
\end{center}
\end{block}
\end{textblock}

\begin{textblock}{15}(2,12)
\small
\begin{itemize}
\item<3-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
803 loc in C including 2 library functions)\\[-3mm]
\item<3-> 167 loc in C implement a type-checker
\end{itemize}
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}<2->[squeeze]
  \frametitle{} 
  
  \begin{columns}
  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
                     draw=black!50, top color=white, bottom color=black!20]
  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
                     draw=red!70, top color=white, bottom color=red!50!black!20]
  
  \begin{column}{0.8\textwidth}
  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}
  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
  { \&[-10mm] 
    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
    \node (proof1) [node1] {\large Proof}; \&
    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
    
    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
     
    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
  
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
  
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
  \end{tikzpicture}

  \end{textblock}
  \end{column}
  \end{columns}


  \begin{textblock}{3}(12,3.6)
  \onslide<4->{
  \begin{tikzpicture}
  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
  \end{tikzpicture}}
  \end{textblock}
  
  \begin{textblock}{0}(0.4,12.8)
  \onslide<6->{
  \begin{bubble}[11cm]
  \small Each time one needs to check $\sim$31pp~of 
  informal paper proofs.
  You have to be able to keep definitions 
  and proofs consistent.
  \end{bubble}}
  \end{textblock}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  \begin{frame}[c]
%  \frametitle{\Large Lessons Learned}
%
%  \begin{itemize}
%  \item using a theorem prover we were able to keep a large 
%  proof consistent with changes in the definitions\bigskip
%  \item it took us some 10 days to get to the error\ldots
%  probably the same time Harper and Pfenning needed to \LaTeX{}
%  their paper\bigskip 
%  \item once there, we ran circles around them
%  \end{itemize}
%
%  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Real-Time Scheduling} 

  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
    
  \only<1>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
  }
  \only<2>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (5,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
  }
  \only<3>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
   \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
   \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
  }
  \only<4>{
   \node at (2.5,0.9) {\small locks a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<5>{
   \node at (2.5,0.9) {\small locks a resource};
   \draw[fill, blue!50] (1,0) rectangle (4,0.6);
   \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
  }
  \only<6>{
   \node at (2.5,0.9) {\small locks a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<7>{
   \node at (2.5,0.9) {\small locks a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<8>{
   \node at (2.5,0.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<9>{
   \node at (2.5,0.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<10>{
   \node at (2.5,0.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<11>{
   \node at (2.5,0.9) {\small locks a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
   \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
  }
  \only<12>{
   \node at (2.5,0.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
   \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
   \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
   \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
  }
  \only<13>{
   \node at (2.5,0.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<14>{
   \node at (2.5,3.9) {\small locks a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<15>{
   \node at (2.5,3.9) {\small locks a resource};  
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
   \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 
  }


  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}

  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<3->{
  \begin{bubble}[8cm]%
  RT-Scheduling: You want to avoid that a 
  high-priority process is starved indefinitely.
  \end{bubble}}
  \end{textblock}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process \bl{$L$} temporarily inherit 
    the high priority of \bl{$H$} until \bl{$L$} leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked, \bl{$L$} ``returns to its original 
    priority level.''\\
    \mbox{}\hfill\footnotesize
    \begin{tabular}{p{6cm}@{}}
    L.~Sha, R.~Rajkumar, and J.~P.~Lehoczky. 
    {\it Priority Inheritance Protocols: An Approach to 
    Real-Time Synchronization}. IEEE Transactions on 
    Computers, 39(9):1175–1185, 1990
    \end{tabular}\bigskip\normalsize\pause
  
  \item Proved correct, reviewed in a respectable journal....what could possibly be wrong?
    
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
  \only<1>{
    \draw[fill, blue!50] (1,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<2>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<3>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
  }
  \only<4>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (4,3) rectangle (5,3.6);
    \node at (4.5,3.3) {\small $B$};
  }
  \only<5>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};
    \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
  }
  \only<6>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$}; 
  }
  \only<7>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
    \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
  }
  \only<8>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<9>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<10>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
  }
  \only<11>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
    \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
    \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
  }

  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}
  
  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<11>{
  \begin{bubble}[8cm]%
  Scheduling: You want to avoid that a high 
  priority process is starved indefinitely.
  \end{bubble}}
  \end{textblock}


  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process \bl{$L$} temporarily inherit 
    the high priority of \bl{$H$} until \bl{$L$} leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked, \bl{$L$} returns to its original 
    priority level. \alert{\bf BOGUS}\pause\bigskip
  \item \ldots \bl{$L$} needs to switch to the highest 
    \alert{\bf remaining} priority of the threads that it blocks.
  \end{itemize}\bigskip

  \small this error is already known since around 1999

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.25]{p3.jpg}
  \end{center}

   \begin{itemize}
  \item by Rajkumar, 1991
  \item \it ``it resumes the priority it had at the point of entry into the critical 
  section''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
     
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.25]{p2.jpg}
  \end{center}

   \begin{itemize}
  \item by Jane Liu, 2000
  \item {\it ``The job $J_l$ executes at its inherited 
    priority until it releases $R$; at that time, the 
    priority of $J_l$ returns to its priority 
    at the time when it acquires the resource $R$.''}\medskip
  \item \small gives pseudo code and totally bogus data structures  
  \item \small interesting part is ``{\it left as an exercise}''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
     
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.15]{p1.pdf}
  \end{center}

  \begin{itemize}
  \item by Laplante and Ovaska, 2011 (\$113.76)
  \item \it ``when $[$the task$]$ exits the critical section that
        caused the block, it reverts to the priority it had
        when it entered that section'' 
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.22]{p5.jpg}
  \end{center}

  \begin{itemize}
  \item by Silberschatz, Galvin and Gagne (9th edition, 2013)
  \item \it ``Upon releasing the
  lock, the $[$low-priority$]$ thread will revert to its original
  priority.''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
    
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Priority Scheduling}

  \begin{itemize}
  \item a scheduling algorithm that is widely used in real-time operating systems
  \item has been ``proved'' correct by hand in a paper in 1990
  \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
  
  \item we (generalised) the algorithm and then {\bf really} proved that it is correct	
  \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)
  \item our implementation was faster than their reference implementation
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  \begin{frame}[c]
%  \frametitle{\Large{}Mars Pathfinder Mission 1997}
%
%  \begin{center}
%  \includegraphics[scale=0.15]{marspath1.png}
%  \includegraphics[scale=0.16]{marspath3.png}
%  \includegraphics[scale=0.3]{marsrover.png}
%  \end{center}
%  
%  \begin{itemize}
%  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
%  \item a scheduling algorithm was not used in the OS at the 
%  beginning; PIP was enabled after the cause was identified
%  \end{itemize}
%
%  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Lessons Learned}

  \begin{itemize}
  \item our proof-technique is adapted from security 
  protocols\bigskip
 
  \item do not venture outside your field of expertise 
  \includegraphics[scale=0.03]{smiley.jpg}
  \bigskip

  \item we solved the single-processor case; the multi-processor 
  case: no idea!
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Regular Expressions}


\begin{textblock}{6}(2,5)
  \begin{tabular}{rrl@ {\hspace{13mm}}l}
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}   & null\\
           & \bl{$\mid$} & \bl{$\epsilon$}      & empty string\\
           & \bl{$\mid$} & \bl{$c$}             & character\\
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$} & sequence\\
           & \bl{$\mid$} & \bl{$r_1 + r_2$}     & alternative / choice\\
           & \bl{$\mid$} & \bl{$r^*$}           & star (zero or more)\\
  \end{tabular}
  \end{textblock}
  
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}

\large
If \bl{$r$} matches the string \bl{$c\!::\!s$}, what is a regular 
expression that matches just \bl{$s$}?\bigskip\bigskip\bigskip\bigskip

\small
\bl{$der\,c\,r$} gives the answer, Brzozowski (1964), Owens (2005)
``\ldots have been lost in the sands of time\ldots''
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{}


\ldots{}whether a regular expression can match the empty string:
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
\bl{$nullable(\varnothing)$}      & \bl{$\dn$} & \bl{$false$}\\
\bl{$nullable(\epsilon)$}           & \bl{$\dn$} &  \bl{$true$}\\
\bl{$nullable (c)$}                    & \bl{$\dn$} &  \bl{$false$}\\
\bl{$nullable (r_1 + r_2)$}       & \bl{$\dn$} &  \bl{$nullable(r_1) \vee nullable(r_2)$} \\ 
\bl{$nullable (r_1 \cdot r_2)$} & \bl{$\dn$} &  \bl{$nullable(r_1) \wedge nullable(r_2)$} \\
\bl{$nullable (r^*)$}                 & \bl{$\dn$} & \bl{$true$} \\
\end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}The Derivative of a Rexp\end{tabular}}

\begin{center}
\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
  \bl{$der\, c\, (\varnothing)$}      & \bl{$\dn$} & \bl{$\varnothing$} & \\
  \bl{$der\, c\, (\epsilon)$}           & \bl{$\dn$} & \bl{$\varnothing$} & \\
  \bl{$der\, c\, (d)$}                     & \bl{$\dn$} & \bl{if $c = d$ then $\epsilon$ else $\varnothing$} & \\
  \bl{$der\, c\, (r_1 + r_2)$}        & \bl{$\dn$} & \bl{$der\, c\, r_1 + der\, c\, r_2$} & \\
  \bl{$der\, c\, (r_1 \cdot r_2)$}  & \bl{$\dn$}  & \bl{if $nullable (r_1)$}\\
  & & \bl{then $(der\,c\,r_1) \cdot r_2 + der\, c\, r_2$}\\ 
  & & \bl{else $(der\, c\, r_1) \cdot r_2$}\\
  \bl{$der\, c\, (r^*)$}          & \bl{$\dn$} & \bl{$(der\,c\,r) \cdot (r^*)$} &\medskip\\\pause

  \bl{$\textit{ders}\, []\, r$}     & \bl{$\dn$} & \bl{$r$} & \\
  \bl{$\textit{ders}\, (c\!::\!s)\, r$} & \bl{$\dn$} & \bl{$\textit{ders}\,s\,(der\,c\,r)$} & \\
  \end{tabular}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={\pcode{a}s},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,200,...,1000},
    xmax=1000,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=9.5cm,
    height=7cm, 
    legend entries={Python,Ruby,Scala V1,Scala V2},  
    legend pos=north west,
    legend cell align=left  
]
\addplot[blue,mark=*, mark options={fill=white}] 
  table {re-python.data};
\addplot[brown,mark=pentagon*, mark options={fill=white}] 
  table {re-ruby.data};  
\addplot[red,mark=triangle*,mark options={fill=white}] 
  table {re1.data};  
\addplot[green,mark=square*,mark options={fill=white}] 
  table {re2b.data};
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{\begin{tabular}{c}\bl{$({\tt a}?)^n \cdot {\tt a}^n$}\end{tabular}}

\begin{center}
\begin{tikzpicture}
\begin{axis}[
    xlabel={\pcode{a}s},
    ylabel={time in secs},
    enlargelimits=false,
    xtick={0,3000,...,12000},
    xmax=12000,
    ymax=35,
    ytick={0,5,...,30},
    scaled ticks=false,
    axis lines=left,
    width=9cm,
    height=7cm
]
\addplot[green,mark=square*,mark options={fill=white}] table {re2b.data};
\addplot[black,mark=square*,mark options={fill=white}] table {re3.data};
\end{axis}
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Correctness}

It is a relative easy exercise in a theorem prover:

\begin{center}
\bl{$matches(r, s)$}  if and only if  \bl{$s \in L(r)$} 
\end{center}\bigskip

\small
\bl{$matches(r, s) \dn nullable(ders(r, s))$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{POSIX Regex Matching}

Two rules:

\begin{itemize}
\item Longest match rule (``maximal munch rule''): The 
longest initial substring matched by any regular expression 
is taken as the next token.

\begin{center}
\bl{$\texttt{\Grid{iffoo\VS bla}}$}
\end{center}\medskip

\item Rule priority:
For a particular longest initial substring, the first regular
expression that can match determines the token.

\begin{center}
\bl{$\texttt{\Grid{if\VS bla}}$}
\end{center}
\end{itemize}\bigskip\pause

\small
\hfill Kuklewicz: most POSIX matchers are buggy\\
\footnotesize
\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{POSIX Regex Matching}

\begin{itemize}

\item Sulzmann \& Lu came up with a beautiful
idea for how to extend the simple regular expression 
matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip\bigskip

\begin{tabular}{@{\hspace{4cm}}c@{}}
  \includegraphics[scale=0.14]{sulzmann.jpg}\\[-2mm]
  \hspace{0cm}\footnotesize Martin Sulzmann
\end{tabular}\bigskip\bigskip

\item the idea: define an inverse operation to the derivatives
\end{itemize}



\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Regexes and Values}

Regular expressions and their corresponding values:

\begin{center}
\begin{columns}
\begin{column}{3cm}
\begin{tabular}{@{}rrl@{}}
  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\
           & \bl{$\mid$} & \bl{$\epsilon$}   \\
           & \bl{$\mid$} & \bl{$c$}          \\
           & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
           & \bl{$\mid$} & \bl{$r_1 + r_2$}   \\
  \\
           & \bl{$\mid$} & \bl{$r^*$}         \\
  \\
  \end{tabular}
\end{column}
\begin{column}{3cm}
\begin{tabular}{@{\hspace{-7mm}}rrl@{}}
  \bl{$v$} & \bl{$::=$}  & \\
           &             & \bl{$Empty$}   \\
           & \bl{$\mid$} & \bl{$Char(c)$}          \\
           & \bl{$\mid$} & \bl{$Seq(v_1,v_2)$}\\
           & \bl{$\mid$} & \bl{$Left(v)$}   \\
           & \bl{$\mid$} & \bl{$Right(v)$}  \\
           & \bl{$\mid$} & \bl{$[]$}      \\
           & \bl{$\mid$} & \bl{$[v_1,\ldots\,v_n]$} \\
  \end{tabular}
\end{column}
\end{columns}
\end{center}\pause

There is also a notion of a string behind a value: \bl{$|v|$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Sulzmann \& Lu Matcher}

We want to match the string \bl{$abc$} using \bl{$r_1$}:

\begin{center}
\begin{tikzpicture}[scale=2,node distance=1.3cm,every node/.style={minimum size=8mm}]
\node (r1)  {\bl{$r_1$}};
\node (r2) [right=of r1] {\bl{$r_2$}};
\draw[->,line width=1mm]  (r1) -- (r2) node[above,midway] {\bl{$der\,a$}};\pause
\node (r3) [right=of r2] {\bl{$r_3$}};
\draw[->,line width=1mm]  (r2) -- (r3) node[above,midway] {\bl{$der\,b$}};\pause
\node (r4) [right=of r3] {\bl{$r_4$}};
\draw[->,line width=1mm]  (r3) -- (r4) node[above,midway] {\bl{$der\,c$}};\pause
\draw (r4) node[anchor=west] {\;\raisebox{3mm}{\bl{$\;\;nullable?$}}};\pause
\node (v4) [below=of r4] {\bl{$v_4$}};
\draw[->,line width=1mm]  (r4) -- (v4);\pause
\node (v3) [left=of v4] {\bl{$v_3$}};
\draw[->,line width=1mm]  (v4) -- (v3) node[below,midway] {\bl{$inj\,c$}};\pause
\node (v2) [left=of v3] {\bl{$v_2$}};
\draw[->,line width=1mm]  (v3) -- (v2) node[below,midway] {\bl{$inj\,b$}};\pause
\node (v1) [left=of v2] {\bl{$v_1$}};
\draw[->,line width=1mm]  (v2) -- (v1) node[below,midway] {\bl{$inj\,a$}};\pause
\draw[->,line width=0.5mm]  (r3) -- (v3);
\draw[->,line width=0.5mm]  (r2) -- (v2);
\draw[->,line width=0.5mm]  (r1) -- (v1);
\draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{\bl{$mkeps$}}};
\end{tikzpicture}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t,squeeze]
\frametitle{Sulzmann \& Lu Paper}

\begin{itemize}
\item I have no doubt the algorithm is correct --- 
  the problem, I do not believe their proof.

  \begin{center}
  \begin{bubble}[10cm]\small
  ``How could I miss this? Well, I was rather careless when 
  stating this Lemma :)\smallskip
 
  Great example how formal machine checked proofs (and 
  proof assistants) can help to spot flawed reasoning steps.''
  \end{bubble}
  \end{center}\pause
  
  \begin{center}
  \begin{bubble}[10cm]\small
  ``Well, I don't think there's any flaw. The issue is how to 
  come up with a mechanical proof. In my world mathematical 
  proof $=$ mechanical proof doesn't necessarily hold.''
  \end{bubble}
  \end{center}\pause
  
\end{itemize}

  \only<3>{%
  \begin{textblock}{11}(1,4.4)
  \begin{center}
  \begin{bubble}[10.9cm]\small\centering
  \includegraphics[scale=0.37]{msbug.png}
  \end{bubble}
  \end{center}
  \end{textblock}}
  

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{\begin{tabular}{c}The Proof Idea\\[-1mm] by Sulzmann \& Lu
\end{tabular}}

\begin{itemize}
\item introduce an inductively defined ordering relation 
\bl{$v \succ_r v'$} which captures the idea of POSIX matching

\item the algorithm returns the maximum of all possible
 values that are possible for a regular expression.\pause
 \bigskip\small
 
\item the idea is from a paper by Cardelli \& Frisch about 
greedy matching (greedy $=$ preferring instant gratification to delayed
repletion):

\item e.g.~given \bl{$(a + (b + ab))^*$} and string \bl{$ab$}

\begin{center}
\begin{tabular}{ll}
greedy: & \bl{$[Left(a), Right(Left(b)]$}\\
POSIX:  & \bl{$[Right(Right(a, b)))]$}  
\end{tabular}
\end{center} 
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{}
\centering


\bl{\infer{\vdash Empty : \epsilon}{}}\hspace{15mm}
\bl{\infer{\vdash Char(c): c}{}}\bigskip

\bl{\infer{\vdash Seq(v_1, v_2) : r_1\cdot r_2}{\vdash v_1 : r_1 \quad \vdash v_2 : r_2}}
\bigskip

\bl{\infer{\vdash Left(v) : r_1 + r_2}{\vdash v : r_1}}\hspace{15mm}
\bl{\infer{\vdash Right(v): r_1 + r_2}{\vdash v : r_2}}\bigskip

\bl{\infer{\vdash [] : r^*}{}}\hspace{15mm}
\bl{\infer{\vdash [v_1,\ldots, v_n] : r^*}
          {\vdash v_1 : r \quad\ldots\quad \vdash v_n : r}}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}<1>[c]
\frametitle{}
\small

\begin{tabular}{@{}lll@{}}
\bl{$POSIX(v, r)$} & \bl{$\dn$} & \bl{$\vdash v : r$}\\ 
 & &   \bl{$\wedge \;\;(\forall v'.\;\; \vdash v' : r \,\wedge\, |v'| = |v| 
     \Rightarrow v \succ_{\alert<2>{r}} v')$}
\end{tabular}\bigskip\bigskip\bigskip


\centering

\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
   {v_1 = v'_1 \quad v_2 \succ_{\alert<2>{r_2}} v'_2}}\hspace{3mm}
\bl{\infer{Seq(v_1, v_2) \succ_{\alert<2>{r_1\cdot r_2}} Seq(v'_1, v'_2)}
   {v_1 \not= v'_1 \quad v_1 \succ_{\alert<2>{r_1}} v'_1}}
\bigskip

\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
          {v \succ_{\alert<2>{r_1}} v'}}\hspace{15mm}
\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
          {v \succ_{\alert<2>{r_2}} v'}}\bigskip\medskip

\bl{\infer{Left(v) \succ_{\alert<2>{r_1 + r_2}} Right(v')}
          {length |v|  \ge length |v'|}}\hspace{15mm}
\bl{\infer{Right(v) \succ_{\alert<2>{r_1 + r_2}} Left(v')}
          {length |v| >  length |v'|}}\bigskip

\bl{$\big\ldots$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Problems}

\begin{itemize}
\item Sulzmann: \ldots Let's assume \bl{$v$} is not 
    a $POSIX$ value, then there must be another one
    \ldots contradiction.\bigskip\pause

\item Exists?

\begin{center}
\bl{$L(r) \not= \varnothing \;\Rightarrow\; POSIX(v, r)$}
\end{center}\bigskip\bigskip\pause

\item in the sequence case, the induction hypotheses require
\bl{$|v_1| = |v'_1|$} and \bl{$|v_2| = |v'_2|$}, 
but you only know

\begin{center}
\bl{$|v_1| \;@\; |v_2| = |v'_1| \;@\; |v'_2|$}
\end{center}\pause\small

\item although one begins with the assumption that the two 
values have the same flattening, this cannot be maintained 
as one descends into the induction (alternative, sequence)
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Our Solution}

\begin{itemize}
\item direct definition of what a POSIX value is, using
\bl{$s \in r \to v$}:

\begin{center}
\bl{\infer{[] \in \epsilon \to Empty}{}}\hspace{15mm}
\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip

\bl{\infer{s \in r_1 + r_2 \to Left(v)}
          {s \in r_1 \to v}}\hspace{10mm}
\bl{\infer{s \in r_1 + r_2 \to Right(v)}
          {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip

\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}
          {\small\begin{array}{l}
           s_1 \in r_1 \to v_1 \\
           s_2 \in r_2 \to v_2 \\
           \neg(\exists s_3\,s_4.\; s_3 \not= []
           \wedge s_3 @ s_4 = s_2 \wedge
           s_1 @ s_3 \in L(r_1) \wedge
           s_4 \in L(r_2))
           \end{array}}}
           
\bl{\ldots}           
\end{center}
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
  \frametitle{\Large\begin{tabular}{@{}c@{}}Pencil-and-Paper Proofs\\[-1mm] 
  in CS are normally incorrect\end{tabular}}

\begin{itemize}
\item case in point, in one of Roy's proofs he made the 
incorrect inference

\begin{center}
if \bl{$\forall s.\; |v_2| \alert{\not}\in L(der\,c\,r_1) \cdot s$}
then \bl{$\forall s.\; c\,|v_2| \alert{\not}\in L(r_1) \cdot s$}
\end{center}\bigskip

while 

\begin{center}
if \bl{$\forall s.\; |v_2| \in L(der\,c\,r_1) \cdot s$}
then \bl{$\forall s.\; c\,|v_2| \in L(r_1) \cdot s$}
\end{center}

is correct

\end{itemize}


\begin{textblock}{11}(12,11)
\includegraphics[scale=0.15]{roy.jpg}
\end{textblock}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Proofs in Math~vs.~in CS}
  
  \alert{\bf My theory on why CS-proofs are often buggy}
  \\[-10mm]\mbox{}
  
  \begin{center}
  \begin{tabular}{@{}cc@{}}
  \begin{tabular}{@{}p{5.6cm}} 
  \includegraphics[scale=0.43]{icosahedron.png}\\[2mm] 
  {\bf Math}: \\
  \raggedright\small
  in math, ``objects'' can be ``looked'' at from all 
  ``angles'';\\\smallskip 
  non-trivial proofs, but it seems
  difficult to make mistakes
  \end{tabular} &
  \begin{tabular}{p{5cm}} 
  \includegraphics[scale=0.2]{sel4callgraph.jpg}\\[3mm]
  \raggedright
  {\bf Code in CS}: \\
  \raggedright\small
  the call-graph of the seL4 microkernel OS;\\\smallskip 
  easy to make mistakes\\ \mbox{}\\
  \end{tabular}
  \end{tabular}
  \end{center}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Conclusion}

\begin{itemize}
\item we strengthened the POSIX definition of Sulzmann \& Lu
  in order to get the inductions through, his proof
  contained small gaps but had also fundamental flaws\bigskip

\item its a nice exercise for theorem proving
\item some optimisations need to be aplied to the
 algorithm in order to become fast enough
\item can be used for lexing, small little functional 
 program
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[b]
  \frametitle{
  \begin{tabular}{c}
  \mbox{}\\[13mm]
  \alert{\Large Thank you very much again}\\
  \alert{\Large for the invitation!}\\
  \alert{\Large Questions?}
  \end{tabular}}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\end{document}


%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: 

