# HG changeset patch # User Christian Urban # Date 1465901900 -3600 # Node ID a35041d5707c74a33fecde30cd4a2458c652e111 # Parent 5fa8344a51762ee2b4d3cff0c81b3d837e1e871e updated slides diff -r 5fa8344a5176 -r a35041d5707c Slides/slides01.pdf Binary file Slides/slides01.pdf has changed diff -r 5fa8344a5176 -r a35041d5707c Slides/slides01.tex --- a/Slides/slides01.tex Sat Jun 11 13:28:45 2016 +0100 +++ b/Slides/slides01.tex Tue Jun 14 11:58:20 2016 +0100 @@ -66,7 +66,7 @@ \begin{frame}[c] \begin{center} - \includegraphics[scale=0.2]{isabelle.png} + \includegraphics[scale=0.2]{pics/isabelle.png} \end{center} \mbox{}\\[-20mm]\mbox{} @@ -133,12 +133,12 @@ \item me, my supervisor, the examiners did not find any problems\medskip \begin{center} \begin{tabular}{@ {}c@ {}} - \includegraphics[scale=0.38]{barendregt.jpg}\\[-2mm] + \includegraphics[scale=0.38]{pics/barendregt.jpg}\\[-2mm] \footnotesize Henk Barendregt \end{tabular} \hspace{2mm} \begin{tabular}{@ {}c@ {}} - \includegraphics[scale=0.20]{andrewpitts.jpg}\\[-2mm] + \includegraphics[scale=0.20]{pics/andrewpitts.jpg}\\[-2mm] \footnotesize Andrew Pitts \end{tabular} \end{center} @@ -172,7 +172,7 @@ \only<2->{ \begin{textblock}{3}(13,5) -\includegraphics[scale=0.33]{skeleton.jpg} +\includegraphics[scale=0.33]{pics/skeleton.jpg} \end{textblock}} \begin{textblock}{3}(5.3,7) @@ -235,12 +235,12 @@ \begin{tabular}{c@ {\hspace{2mm}}c} \\[6mm] \begin{tabular}{c} -\includegraphics[scale=0.11]{harper.jpg}\\[-2mm] +\includegraphics[scale=0.11]{pics/harper.jpg}\\[-2mm] {\footnotesize Bob Harper}\\[-2mm] {\footnotesize} \end{tabular} \begin{tabular}{c} -\includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm] +\includegraphics[scale=0.37]{pics/pfenning.jpg}\\[-2mm] {\footnotesize Frank Pfenning}\\[-2mm] {\footnotesize} \end{tabular} & @@ -254,7 +254,7 @@ \\[0mm] \begin{tabular}{c} -\includegraphics[scale=0.36]{appel.jpg}\\[-2mm] +\includegraphics[scale=0.36]{pics/appel.jpg}\\[-2mm] {\footnotesize Andrew Appel}\\[-2.5mm] {\footnotesize} \end{tabular} & @@ -822,7 +822,7 @@ \begin{frame}[c] \begin{center} - \includegraphics[scale=0.25]{p3.jpg} + \includegraphics[scale=0.25]{pics/p3.jpg} \end{center} \begin{itemize} @@ -838,7 +838,7 @@ \begin{frame}[c] \begin{center} - \includegraphics[scale=0.25]{p2.jpg} + \includegraphics[scale=0.25]{pics/p2.jpg} \end{center} \begin{itemize} @@ -858,7 +858,7 @@ \begin{frame}[c] \begin{center} - \includegraphics[scale=0.15]{p1.pdf} + \includegraphics[scale=0.15]{pics/p1.pdf} \end{center} \begin{itemize} @@ -875,7 +875,7 @@ \begin{frame}[c] \begin{center} - \includegraphics[scale=0.22]{p5.jpg} + \includegraphics[scale=0.22]{pics/p5.jpg} \end{center} \begin{itemize} @@ -906,24 +906,6 @@ \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] @@ -934,7 +916,7 @@ protocols\bigskip \item do not venture outside your field of expertise - \includegraphics[scale=0.03]{smiley.jpg} + \includegraphics[scale=0.03]{pics/smiley.jpg} \bigskip \item we solved the single-processor case; the multi-processor @@ -1143,7 +1125,7 @@ matcher to POSIX matching/lexing (FLOPS 2014)\bigskip\bigskip\bigskip \begin{tabular}{@{\hspace{4cm}}c@{}} - \includegraphics[scale=0.14]{sulzmann.jpg}\\[-2mm] + \includegraphics[scale=0.14]{pics/sulzmann.jpg}\\[-2mm] \hspace{0cm}\footnotesize Martin Sulzmann \end{tabular}\bigskip\bigskip @@ -1263,7 +1245,7 @@ \begin{textblock}{11}(1,4.4) \begin{center} \begin{bubble}[10.9cm]\small\centering - \includegraphics[scale=0.37]{msbug.png} + \includegraphics[scale=0.37]{pics/msbug.png} \end{bubble} \end{center} \end{textblock}} @@ -1329,32 +1311,32 @@ \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 +%\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{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}} 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{\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$} +%\bl{$\big\ldots$} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1450,7 +1432,7 @@ \begin{textblock}{11}(12,11) -\includegraphics[scale=0.15]{roy.jpg} +\includegraphics[scale=0.15]{pics/roy.jpg} \end{textblock} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1463,7 +1445,7 @@ \begin{center} \begin{tabular}{@{}cc@{}} \begin{tabular}{@{}p{5.6cm}} - \includegraphics[scale=0.43]{icosahedron.png}\\[2mm] + \includegraphics[scale=0.43]{pics/icosahedron.png}\\[2mm] {\bf Math}: \\ \raggedright\small in math, ``objects'' can be ``looked'' at from all @@ -1472,7 +1454,7 @@ difficult to make mistakes \end{tabular} & \begin{tabular}{p{5cm}} - \includegraphics[scale=0.2]{sel4callgraph.jpg}\\[3mm] + \includegraphics[scale=0.2]{pics/sel4callgraph.jpg}\\[3mm] \raggedright {\bf Code in CS}: \\ \raggedright\small diff -r 5fa8344a5176 -r a35041d5707c Slides/slides02.pdf Binary file Slides/slides02.pdf has changed diff -r 5fa8344a5176 -r a35041d5707c Slides/slides02.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/slides02.tex Tue Jun 14 11:58:20 2016 +0100 @@ -0,0 +1,1543 @@ +\documentclass[dvipsnames,14pt,t]{beamer} +\usepackage{slides} +\usepackage{langs} +\usepackage{graph} +%\usepackage{grammar} +\usepackage{soul} +\usepackage{data} +\usepackage{proof} + +% beamer stuff +\renewcommand{\slidecaption}{SMAL, 23.3.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\\ + \\ + \small joint work with Fahad Ausaf and Roy Dyckhoff + \end{tabular} + \end{center} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c] +\frametitle{Why Bother?} + +\begin{itemize} +\item Surely regular expressions must have been studied and + implemented to death by now, no?\medskip\pause + +\item \ldots{}well, take for example the ``evil'' regular + expression \bl{$({\tt a}^?)^n \cdot {\tt a}^n$} to match + strings \bl{$\underbrace{{\tt a}\ldots{\tt a}}_n$} +\end{itemize}\smallskip + +\begin{center} +\begin{tikzpicture} +\begin{axis}[ + xlabel={strings of {\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=7cm, + height=5cm, + 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} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{frame}[c] + + \begin{center} + \includegraphics[scale=0.2]{pics/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{\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 + (SN for a 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]{pics/barendregt.jpg}\\[-2mm] + \footnotesize Henk Barendregt + \end{tabular} + \hspace{2mm} + \begin{tabular}{@ {}c@ {}} + \includegraphics[scale=0.20]{pics/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]{pics/skeleton.jpg} +\end{textblock}} + +\begin{textblock}{3}(5.3,7) +\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) +\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 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]{pics/harper.jpg}\\[-2mm] +{\footnotesize Bob Harper}\\[-2mm] +{\footnotesize} +\end{tabular} +\begin{tabular}{c} +\includegraphics[scale=0.37]{pics/pfenning.jpg}\\[-2mm] +{\footnotesize Frank Pfenning}\\[-2mm] +{\footnotesize} +\end{tabular} & + +\begin{tabular}{p{6cm}} +\raggedright +{published a proof on LF in\\ {\bf ACM Transactions on + Computational Logic}, 2005, +$\sim$31pp} +\end{tabular}\\ + +\\[0mm] + +\begin{tabular}{c} +\includegraphics[scale=0.36]{pics/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<2->{ + \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}; + +\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}{14}(2,11) +\small +\begin{itemize} +\item<2-> Appel's checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; +803 loc in C including 2 library functions)\\[-3mm] +\item<2-> 167 loc in C implement a type-checker\\ (proved correct by Harper and Pfenning) +\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---impossible without tool support. + 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 by using a theorem prover we were able to keep a large + proof consistent with changes in the first definitions\bigskip + \item it took us appr.~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}(1.5,13)% + \small + \onslide<5->{ + \begin{bubble}[10.3cm]% + RT-Scheduling: You want to avoid that a + high-priority process is starved indefinitely by lower priority + processes. + \end{bubble}} + \end{textblock} + + \end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{frame}[c] + \frametitle{\Large Priority Inheritance Scheduling} + + \begin{itemize} + \item Idea: 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 classic, 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}(1.5,13)% + \small + \begin{bubble}[10.3cm]% + RT-Scheduling: You want to avoid that a + high-priority process is starved indefinitely by lower priority + processes. + \end{bubble} + \end{textblock} + + \end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \begin{frame}[c] + \frametitle{\Large Priority Inheritance Scheduling} + + \begin{itemize} + \item Idea: 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{textblock}{11}(2,1) + \alt<1>{\includegraphics[scale=0.25]{pics/p3.jpg}} + {\includegraphics[scale=0.125]{pics/p3.jpg}} + \alt<2>{\includegraphics[scale=0.25]{pics/p2.jpg}} + {\includegraphics[scale=0.125]{pics/p2.jpg}} + \alt<3>{\includegraphics[scale=0.153]{pics/p1.jpg}} + {\includegraphics[scale=0.076]{pics/p1.jpg}} + \alt<4>{\includegraphics[scale=0.25]{pics/p4.jpg}} + {\includegraphics[scale=0.125]{pics/p4.jpg}} + \alt<5>{\includegraphics[scale=0.088]{pics/p5.jpg}} + {\includegraphics[scale=0.044]{pics/p5.jpg}} + \end{textblock} + + \begin{textblock}{13}(1,9) + \only<1>{ + \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}} + \only<2>{ + \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 uses pretty bogus data structures + \item \small the interesting part is ``{\it left as an exercise}'' + \end{itemize}} + \only<3>{ + \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}} + \only<4>{ + \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}} + \only<5>{ + \begin{itemize} + \item by Stallings (8th edition, 2014) + \item \it ``This priority change takes place as soon as the + higher-priority task blocks on the resource; it should end when + the resource is released by the lower-priority task.'' + \end{itemize}} + \end{textblock} + \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{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{The Derivative of a Rexp} + +\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{The Derivative of a Rexp} + +\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{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 +where \bl{$matches(r, s) \dn nullable(ders(r, s))$} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c] +\frametitle{\bl{$({\tt a}^?)^n \cdot {\tt a}^n$}} + +\begin{center} +\begin{tikzpicture} +\begin{axis}[ + xlabel={strings of \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{\bl{$({\tt a}^?)^n \cdot {\tt a}^n$}} + +\begin{center} +\begin{tikzpicture} +\begin{axis}[ + xlabel={strings of \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{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 + +\begin{tabular}{@{\hspace{4cm}}c@{}} + \includegraphics[scale=0.20]{pics/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 +(for \emph{how} a regular expression matched a string): + +\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} + +\only<10>{ +The original ideas of Sulzmann and Lu are the \bl{\textit{mkeps}} +and \bl{\textit{inj}} functions (ommitted here).} +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[t,squeeze] +\frametitle{Sulzmann \& Lu Paper} + +\begin{itemize} +\item I have no doubt the algorithm is correct --- + the problem is 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]{pics/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(Seq(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\; \exists v.\;POSIX(v, r)$} +\end{center}\bigskip\bigskip\pause + +\item in the sequence case +\bl{$Seq(v_1, v_2)\succ_{r_1\cdot r_2} Seq(v_1', v_2')$}, +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 a direct definition of what a POSIX value is, using +the relation \bl{$s \in r \to v$} (specification):\medskip + +\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}[c] +\frametitle{Properties} + +It is almost trival to prove: + +\begin{itemize} +\item Uniqueness +\begin{center} +If \bl{$s \in r \to v_1$} and \bl{$s \in r \to v_2$} then +\bl{$v_1 = v_2$}. +\end{center}\bigskip + +\item Correctness +\begin{center} +\bl{$lexer(r, s) = v$} if and only if \bl{$s \in r \to v$} +\end{center} +\end{itemize}\bigskip\bigskip\pause + + +You can now start to implement optimisations and derive +correctness proofs for them. But we still do not know whether + +\begin{center} +\bl{$s \in r \to v$} +\end{center} + +is a POSIX value according to Sulzmann \& Lu's definition +(biggest value for \bl{$s$} and \bl{$r$}) +\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]{pics/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]{pics/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]{pics/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 replaced the POSIX definition of Sulzmann \& Lu by a + new definition (ours is inspired by work of Vansummeren, + 2006)\medskip + +\item their proof contained small gaps (acknowledged) but had + also fundamental flaws\medskip + +\item now, its a nice exercise for theorem proving\medskip + +\item some optimisations need to be applied to the algorithm + in order to become fast enough\medskip + +\item can be used for lexing, is a small beautiful 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: + diff -r 5fa8344a5176 -r a35041d5707c progs/scala/tests.scala --- a/progs/scala/tests.scala Sat Jun 11 13:28:45 2016 +0100 +++ b/progs/scala/tests.scala Tue Jun 14 11:58:20 2016 +0100 @@ -200,7 +200,8 @@ } } -println(Parser("a|(bc)*").Regex()) +//test case +//println(Parser("a|(bc)*").Regex()) def process_line(line: String) : String = {