\documentclass[dvipsnames,14pt,t]{beamer}\usepackage{../slides}\usepackage{../langs}\usepackage{../graphics}\usepackage{../grammar}\usepackage{soul}\usepackage{mathpartir}% beamer stuff \renewcommand{\slidecaption}{CFL 09, King's College London}\newcommand{\bl}[1]{\textcolor{blue}{#1}}\begin{document}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[t]\frametitle{% \begin{tabular}{@ {}c@ {}} \\[-3mm] \LARGE Compilers and \\[-2mm] \LARGE Formal Languages (9)\\[3mm] \end{tabular}} \normalsize \begin{center} \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ Office: & N7.07 (North Wing, Bush House)\\ Slides: & KEATS (also home work is there)\\ \end{tabular} \end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.6]{../pics/bridge-limits.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Old-Fashioned Eng.~vs.~CS} \begin{center} \begin{tabular}{@{}cc@{}} \begin{tabular}{@{}p{5.2cm}} \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ {\bf bridges}: \\ \raggedright\small engineers can ``look'' at a bridge and have a pretty good intuition about whether it will hold up or not\\ (redundancy; predictive theory) \end{tabular} & \begin{tabular}{p{5cm}} \includegraphics[scale=0.265]{../pics/code.jpg}\\ \raggedright {\bf code}: \\ \raggedright\small programmers have very little intuition about their code; often it is too expensive to have redundancy; not ``continuous'' \end{tabular} \end{tabular} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Dijkstra on Testing} \begin{bubble}[10cm] ``Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence.'' \end{bubble}\bigskip \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{\Large Proving Programs to be Correct}\begin{bubble}[10cm]\small{\bf Theorem:} There are infinitely many prime numbers.\medskip\\{\bf Proof} \ldots\\\end{bubble}\bigskipsimilarly\bigskip\begin{bubble}[10cm]\small{\bf Theorem:} The program is doing what it is supposed to be doing.\medskip{\bf Long, long proof} \ldots\\\end{bubble}\bigskip\medskip\small This can be a gigantic proof. The only hope is to havehelp from the computer. `Program' is here to be understood to bequite general (protocols, OS, \ldots).\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{\Large{}Mars Pathfinder Mission 1997} \begin{center} \includegraphics[scale=0.15]{../pics/marspath1.png} \includegraphics[scale=0.16]{../pics/marspath3.png} \includegraphics[scale=0.3]{../pics/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 \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 (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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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 locked 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]% 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 $L$ temporarily inherit the high priority of $H$ until $L$ leaves the critical section unlocking the resource.\bigskip \item Once the resource is unlocked $L$ returns to its original priority level. \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 staved indefinitely. \end{bubble}} \end{textblock} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{\Large Priority Inheritance Scheduling} \begin{itemize} \item Let a low priority process $L$ temporarily inherit the high priority of $H$ until $L$ leaves the critical section unlocking the resource.\bigskip \item Once the resource is unlocked $L$ returns to its original priority level. \alert{\bf BOGUS}\pause\bigskip \item \ldots $L$ needs to switch to the highest \alert{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]{../pics/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]{../pics/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 ``{\it left as an exercise}'' \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.15]{../pics/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.25]{../pics/p4.jpg} \end{center} \begin{itemize} \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible) \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 1983 \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause \item we used the corrected 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 much more efficient than their reference implementation \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{Big Proofs in CS (1)}Formal proofs in CS sound like science fiction?\begin{itemize}\item in 2008, verification of a C-compiler\begin{itemize}\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''\item is as good as \texttt{gcc -O1}, but much less buggy \end{itemize}\end{itemize}\begin{center} \includegraphics[scale=0.12]{../pics/compcert.png}\end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \begin{frame}[c]% \frametitle{Fuzzy Testing C-Compilers}% \begin{itemize}% \item tested GCC, LLVM and others by randomly generating % C-programs% \item found more than 300 bugs in GCC and also% many in LLVM (some of them highest-level critical)\bigskip% \item about CompCert:% \begin{bubble}[10cm]\small ``The striking thing about our CompCert% results is that the middle-end bugs we found in all other% compilers are absent. As of early 2011, the under-development% version of CompCert is the only compiler we have tested for% which Csmith cannot find wrong-code errors. This is not for% lack of trying: we have devoted about six CPU-years to the% task.'' % \end{bubble} % \end{itemize}% \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{Big Proofs in CS (2)}\begin{itemize}\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) \begin{itemize} \item used in helicopters and mobile phones \item 200k loc of proof \item 25 - 30 person years \item found 160 bugs in the C code (144 by the proof) \end{itemize}\end{itemize}\begin{bubble}[10cm]\small``Real-world operating-system kernel with an end-to-end proofof implementation correctness and security enforcement''\end{bubble}\bigskip\pauseunhackable kernel (New Scientists, September 2015)\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{Big Proofs in CS (3)}\begin{itemize}\item verified TLS implementation\medskip\item verified compilers (CompCert, CakeML)\medskip\item verified distributed systems (Verdi)\medskip\item verified OSes or OS components\\(seL4, CertiKOS, \ldots)\bigskip\pause\item Infer static analyser developed by Facebook \end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{How Did This Happen?}Lots of ways!\begin{itemize}\item better programming languages \begin{itemize} \item basic safety guarantees built in \item powerful mechanisms for abstraction and modularity \end{itemize}\item better software development methodology\item stable platforms and frameworks\item better use of specifications\medskip\\ \small If you want to build software that works or is secure, it is helpful to know what you mean by ``works'' and by ``is secure''!\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{Goal}Remember the Bridges example?\begin{itemize}\item Can we look at our programs and somehow ensurethey are bug free/correct?\pause\bigskip\item Very hard: Anything interesting about programs is equivalentto the Halting Problem, which is undecidable.\pause\bigskip\item \alert{Solution:} We avoid this ``minor'' obstacle by being as close as possible of deciding the halting problem, without actually deciding the halting problem. \small$\quad\Rightarrow$ yes, no, don't know (static analysis)\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state.png} \end{center} \begin{itemize} \item depending on some initial input, a program (behaviour) will ``develop'' over time. \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state2.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state3.jpg} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state4.jpg} \end{center} \begin{itemize} \item to be avoided \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state5.png} \end{center} \begin{itemize} \item this needs more work \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state6.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile] \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] Are Vars Definitely Initialised?\end{tabular}}Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskipProg.~1:\\\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language=While,xleftmargin=3mm]if x < 1 then y := x else y := x + 1;y := y + 1\end{lstlisting}\medskip Prog.~2:\\\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language=While,xleftmargin=3mm]if x < x then y := y + 1 else y := x;y := y + 1\end{lstlisting} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile] \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] Are Vars Definitely Initialised?\end{tabular}} What should the rules be for deciding when a variable is initialised?\bigskip\pause\begin{itemize}\item variable \texttt{x} is definitely initialized after \texttt{skip}\\ iff \texttt{x} is definitely initialized before \texttt{skip}.\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile]% \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]% Are Vars Definitely Initialised?\end{tabular}}$\bl{A}$ is the set of definitely defined variables:\begin{center}\begin{tabular}{c} \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}} \medskip\\\pause \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}} \medskip\\\pause \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2} {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}} \medskip\\\pause \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'} {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause\end{tabular} \end{center}\hfill we start with $\bl{A = \{\}}$\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{\large Concrete Example: Sign-Analysis}\mbox{}\\[-20mm]\mbox{}\bl{\begin{plstx}[rhs style=,one per line]: \meta{Exp} ::= \meta{Exp} + \meta{Exp} | \meta{Exp} * \meta{Exp} | \meta{Exp} = \meta{Exp} | \meta{num} | \meta{var}\\: \meta{Stmt} ::= \meta{label} : | \meta{var} := \meta{Exp} | \pcode{jmp?} \meta{Exp} \meta{label} | \pcode{goto} \meta{label}\\: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\\end{plstx}}\begin{textblock}{0}(7.8,2.5)\small\begin{bubble}[5.6cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=3mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{textblock}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{\large Concrete Example: Sign-Analysis}\mbox{}\\[-20mm]\mbox{}\bl{\begin{plstx}[rhs style=,one per line]: \meta{Exp} ::= \meta{Exp} + \meta{Exp} | \meta{Exp} * \meta{Exp} | \meta{Exp} = \meta{Exp} | \meta{num} | \meta{var}\\: \meta{Stmt} ::= \meta{label} : | \meta{var} := \meta{Exp} | \pcode{jmp?} \meta{Exp} \meta{label} | \pcode{goto} \meta{label}\\: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\\end{plstx}}\begin{textblock}{0}(7.8,3.5)\small\begin{bubble}[5.6cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=3mm] n := 6 m1 := 0 m2 := 1top: jmp? n = 0 done tmp := m2 m2 := m1 + m2 m1 := tmp n := n + -1 goto topdone:\end{lstlisting}\end{bubble}\end{textblock}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{\large Concrete Example: Sign-Analysis}\mbox{}\\[-20mm]\mbox{}\bl{\begin{plstx}[rhs style=,one per line]: \meta{Exp} ::= \meta{Exp} + \meta{Exp} | \meta{Exp} * \meta{Exp} | \meta{Exp} = \meta{Exp} | \meta{num} | \meta{var}\\: \meta{Stmt} ::= \meta{label} : | \meta{var} := \meta{Exp} | \pcode{jmp?} \meta{Exp} \meta{label} | \pcode{goto} \meta{label}\\: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\\end{plstx}}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval: An Interpreter}\mbox{}\\[-14mm]\mbox{}\small\begin{center}\bl{\begin{tabular}{lcl}$[n]_{env}$ & $\dn$ & $n$\\$[x]_{env}$ & $\dn$ & $env(x)$\\$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\$[e_1 = e_2]_{env}$ & $\dn$ & $\begin{cases}1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\0 & \text{otherwise}\end{cases}$\\\end{tabular}}\end{center}\footnotesize\begin{lstlisting}[numbers=none,xleftmargin=-5mm]def eval_exp(e: Exp, env: Env) : Int = e match { case Num(n) => n case Var(x) => env(x) case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env) case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env) case Equ(e1, e2) => if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0}\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\smallA program\begin{bubble}[6cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}The \emph{snippets} of the program:\footnotesize\begin{columns}\begin{column}[t]{5cm}\begin{bubble}[4.5cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]"" a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}[t]{5cm}\begin{bubble}[4.5cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}[t]{2cm}\begin{bubble}[1.1cm]\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language={},xleftmargin=1mm]done:\end{lstlisting}\end{bubble}\end{column}\end{columns}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval for Stmts}\mbox{}\\[-12mm]\mbox{}Let \bl{$sn$} be the snippets of a program\small\begin{center}\bl{\begin{tabular}{lcl}$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\$[x \,\texttt{:=}\, a::rest]_{env}$ & $\dn$ & $[rest]_{(env[x:= [a]_{env}])}$\medskip\\$[\texttt{jmp?}\;b\;l::rest]_{env}$ & $\dn$ & $\begin{cases}[sn(l)]_{env} & \text{if}\quad[b]_{env} = true\\[rest]_{env} & \text{otherwise}\end{cases}$\medskip\\$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\\end{tabular}}\end{center}\bigskipStart with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{Eval in Code}\footnotesize\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]def eval(sn: Snips) : Env = { def eval_stmts(sts: Stmts, env: Env) : Env = sts match { case Nil => env case Label(l)::rest => eval_stmts(rest, env) case Assign(x, e)::rest => eval_stmts(rest, env + (x -> eval_exp(e, env))) case Jmp(b, l)::rest => if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) else eval_stmts(rest, env) case Goto(l)::rest => eval_stmts(sn(l), env) } eval_stmts(sn(""), Map())}\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{The Idea of Static Analysis}\small\mbox{}\bigskip\\\begin{columns}\begin{column}{5cm}\begin{bubble}[4.5cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm] a := 1 n := 5 top: jmp? n = 0 done a := a * n n := n + -1 goto top done:\end{lstlisting}\end{bubble}\end{column}\begin{column}{1cm}\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}\end{column}\begin{column}{6cm}\begin{bubble}[4.7cm]\footnotesize\begin{lstlisting}[numbers=none, language={}, basicstyle=\ttfamily, xleftmargin=1mm, escapeinside={(*}{*)}] a := (*\hl{'+'}*) n := (*\hl{'+'}*) top: jmp? n = (*\hl{'0'}*) done a := a * n n := n + (*\hl{'-'}*) goto top done:\end{lstlisting}\end{bubble}\end{column}\end{columns}\bigskip\bigskipReplace all constants and variables by either \pcode{+}, \pcode{-} or \pcode{0}. What we want to find outis what the sign of \texttt{a} and \texttt{n} is (they should always positive).\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Sign Analysis?} \begin{columns} \begin{column}{3cm} \begin{tabular}{cc|l} $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{} - & - & -\\ - & 0 & -\\ - & + & -, 0, +\\ 0 & $x$ & $x$\\ + & - & -, 0, +\\ + & 0 & +\\ + & + & +\\ \end{tabular} \end{column} \begin{column}{3cm} \begin{tabular}{cc|l} $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{} - & - & +\\ - & 0 & 0\\ - & + & -\\ 0 & $x$ & 0\\ + & - & -\\ + & 0 & 0\\ + & + & +\\ \end{tabular} \end{column} \end{columns} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\mbox{}\\[-13mm]\mbox{}\small\begin{center}\bl{\begin{tabular}{lcl}$[n]_{aenv}$ & $\dn$ & $\begin{cases}\{+\} & \text{if}\; n > 0\\\{-\} & \text{if}\; n < 0\\\{0\} & \text{if}\; n = 0\end{cases}$\\$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\\end{tabular}}\end{center}\scriptsize\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match { case Num(0) => Set(Zero) case Num(n) if (n < 0) => Set(Neg) case Num(n) if (n > 0) => Set(Pos) case Var(x) => aenv(x) case Plus(e1, e2) => aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) case Times(e1, e2) => atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) case Equ(e1, e2) => Set(Zero, Pos)}\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile]\frametitle{AEval for Stmts}\mbox{}\\[-12mm]\mbox{}Let \bl{$sn$} be the snippets of a program\small\begin{center}\bl{\begin{tabular}{lcl}$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & $(rest, aenv[x:= [e]_{aenv}])$\medskip\\$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & $(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\\end{tabular}}\end{center}\bigskipStart with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to reach all \emph{states} you can find (until a fix point is reached).Check whether there are only $aenv$ in the final states that have your property.\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Sign Analysis} \begin{itemize} \item We want to find out whether \texttt{a} and \texttt{n} are always positive?\medskip \item After a few optimisations, we can indeed find this out. \begin{itemize} \item equal signs return only \texttt{+} or \texttt{0} \item branch into only one direction if you know \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ cannot be negative \end{itemize}\bigskip \item What is this good for? Well, you do not need underflow checks (in order to prevent buffer-overflow attacks). In general this technique is used to make sure keys stay secret. \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Take Home Points} \begin{itemize} \item While testing is important, it does not show the absence of bugs/vulnerabilities.\medskip \item More and more we need (formal) proofs that show a program is bug free.\medskip \item Static analysis is more and more employed nowadays in order to automatically hunt for bugs. \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: