\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}\bigskip+ −
+ − + − similarly\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 have+ −
help from the computer. `Program' is here to be understood to be+ −
quite 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 proof+ −
of implementation correctness and security enforcement''+ −
\end{bubble}\bigskip\pause+ −
+ − unhackable 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 ensure+ −
they are bug free/correct?\pause\bigskip+ −
+ − \item Very hard: Anything interesting about programs is equivalent+ −
to 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}?\bigskip+ −
+ − Prog.~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 := 1+ −
top: jmp? n = 0 done+ −
tmp := m2+ −
m2 := m1 + m2+ −
m1 := tmp+ −
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}}+ −
+ − \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]+ −
\small+ −
A 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}\bigskip+ −
+ − Start 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\bigskip+ −
+ − Replace all constants and variables by either + −
\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out+ −
is 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}\bigskip+ −
+ − Start 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: + −
+ −