--- a/slides/slides09.tex Tue Nov 20 13:37:40 2018 +0000
+++ b/slides/slides09.tex Tue Nov 27 00:45:26 2018 +0000
@@ -1,16 +1,19 @@
\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
+\usepackage{../data}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}
-\usepackage{mathpartir}
+
-% beamer stuff
+% beamer stuff
\renewcommand{\slidecaption}{CFL 09, King's College London}
-\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
\begin{document}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
@@ -24,53 +27,137 @@
\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}
+ Office: & N\liningnums{7.07} (North Wing, Bush House)\\
+ Slides: & KEATS (also homework is there)\\
\end{tabular}
\end{center}
- \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{While Language}
+
+\begin{center}
+\bl{\begin{tabular}{@{}lcl@{}}
+\\[-12mm]
+\meta{Stmt} & $::=$ & $\texttt{skip}$\\
+ & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\
+ & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\
+ & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\
+ & $|$ & \texttt{read}\;\textit{Id}\\
+ & $|$ & \texttt{write}\;\textit{Id}\\
+ & $|$ & \texttt{write}\;\textit{String}\medskip\\
+\meta{Stmts} & $::=$ & \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$ \meta{Stmt}\medskip\\
+\meta{Block} & $::=$ & \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\
+\meta{AExp} & $::=$ & \ldots\\
+\meta{BExp} & $::=$ & \ldots\\
+\end{tabular}}
+\end{center}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}
+
+\mbox{}\\[-18mm]\mbox{}
+
+{\lstset{language=While}\fontsize{10}{12}\selectfont
+\texttt{\lstinputlisting{../progs/fib.while}}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{BF***}
+
+some big array, say \texttt{a}; 7 (8) instructions:
+
+\begin{itemize}
+\item \texttt{>} move \texttt{ptr++}
+\item \texttt{<} move \texttt{ptr-{}-}
+\item \texttt{+} add \texttt{a[ptr]++}
+\item \texttt{-} subtract \texttt{a[ptr]-{}-}
+\item \texttt{.} print out \texttt{a[ptr]} as ASCII
+\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}
+\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}
+
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Arrays in While}
+\begin{itemize}
+\item \texttt{new arr[15000]}\medskip
+\item \texttt{x := 3 + arr[3 + y]}\medskip
+\item \texttt{arr[42 * n] := ...}
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{New Arrays}
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ new arr[number]
+\end{lstlisting}\bigskip\bigskip
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ ldc number
+ newarray int
+ astore loc_var
+\end{lstlisting}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Array Update}
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ arr[...] :=
+\end{lstlisting}\bigskip\bigskip
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ aload loc_var
+ index_aexp
+ value_aexp
+ iastore
+\end{lstlisting}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Array Lookup in AExp}
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ ...arr[...]...
+\end{lstlisting}\bigskip\bigskip
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+ aload loc_var
+ index_aexp
+ iaload
+\end{lstlisting}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -82,7 +169,11 @@
presence of bugs, but it is hopelessly inadequate for showing
their absence.''
\end{bubble}\bigskip
-
+
+ \small
+ What is good about compilers: the either seem to work,
+ or go horribly wrong (most of the time).
+
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -111,534 +202,22 @@
\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).
+quite general (compiler, 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?
+\frametitle{Can This Be Done?}
\begin{itemize}
-\item in 2008, verification of a C-compiler
+\item in 2008, verification of a small 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
+\item is as good as \texttt{gcc -O1}, but much, much less buggy
\end{itemize}
\end{itemize}
@@ -650,723 +229,31 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% \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)}
+\frametitle{Fuzzy Testing C-Compilers}
\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}
+\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{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)
+\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{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