\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}

\makeatletter
\newenvironment<>{btHighlight}[1][]
{\begin{onlyenv}#2\begingroup\tikzset{bt@Highlight@par/.style={#1}}\begin{lrbox}{\@tempboxa}}
{\end{lrbox}\bt@HL@box[bt@Highlight@par]{\@tempboxa}\endgroup\end{onlyenv}}

\newcommand<>\btHL[1][]{%
  \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
}
\def\bt@HL@endenv{%
  \end{btHighlight}%   
  \egroup
}
\newcommand{\bt@HL@box}[2][]{%
  \tikz[#1]{%
    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
    \pgfusepath{use as bounding box}%
    \node[anchor=base west, fill=orange!30,outer sep=0pt,inner xsep=1pt, inner ysep=0pt, rounded corners=3pt, minimum height=\ht\strutbox+1pt,#1]{\raisebox{1pt}{\strut}\strut\usebox{#2}};
  }%
}
\makeatother


% beamer stuff 
\renewcommand{\slidecaption}{APP 09, King's College London}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\
  \LARGE Access Control and \\[-3mm] 
  \LARGE Privacy Policies (9)\\[-6mm] 
  \end{tabular}}\bigskip\bigskip\bigskip

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office: & S1.27 (1st floor Strand Building)\\
  Slides: & KEATS (also homework 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
  
  unfortunately attackers exploit bugs (Satan's computer vs 
  Murphy's)

  \vfill
  \small
  Dijkstra: shortest path algorithm, 
  dining philosophers problem,
  semaphores
  \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 sup+ed 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 (protocol, 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 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.
  \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]
  \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 corrected the algorithm and then {\bf really} proved that it is correct	
  \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)
  \item our implementation was much more efficient than their reference implementation
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
   
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Design of AC-Policies}

  \Large
  \begin{quote}
  ''what you specify is what you get but not necessarily what you want\ldots''
  \end{quote}\bigskip\bigskip\bigskip
  
  \normalsize main work by Chunhan Wu (PhD-student)

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

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

  \begin{center}
  \begin{tikzpicture}[scale=1]
  %\draw[black!10,step=2mm] (-5,-3) grid (5,4);
  %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);
  \draw[white,thick,step=10mm] (-5,-3) grid (5,4);

  \draw [black!20, line width=1mm] (0,0) circle (1cm);
  \draw [line width=1mm] (0,0) circle (3cm);
  \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
  
  \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);
  \node at (-3.5,3.6) {your system};
  \node at (-4.8,0) {\Large policy $+$};

  
  \only<2>{
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
  \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
  \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}

  \only<3>{
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
  \node[white] at (2,1) {\small tainted};}

  \only<4>{
  \begin{scope}
  \draw [clip] (0,0) circle (2.955cm);
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);
  \node[white] at (2,1) {\small tainted};
  \end{scope}}

  \only<5->{
  \begin{scope}
  \draw [clip] (0,0) circle (2.955cm);
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);
  \node[white] at (2,1) {\small tainted};
  \end{scope}}

  \only<6->{
  \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);
  \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);
  \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
  }

  \end{tikzpicture}
  \end{center}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{A Sound and Complete Test}

  \begin{itemize}
  \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip

  \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
  \smallskip
  \begin{itemize}
  \item sup+e a tainted file has type \emph{bin} and
  \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
  \item then we would conclude that this tainted file can spread\medskip\pause
  \item but if there is no process with role \bl{$r$} and it will never been
  created, then the file actually does not spread
  \end{itemize}\bigskip\pause

  \item \alert{our solution:} take a middle ground and record precisely the information
  of the initial state, but be less precise about every newly created object.
  \end{itemize}

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

\begin{frame}[c]
\frametitle{Big Proofs in CS}

Formal proofs in CS sound like science fiction? Completely irrelevant!
Lecturer gone mad?\pause

\begin{itemize}
\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 
\end{itemize}
\medskip 
\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
\begin{itemize}
\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}

\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 secure/bug free/correct?\pause\bigskip

\item Very hard: Anything interesting about programs is equivalent
to halting problem, which is undecidable.\pause\bigskip

\item \alert{Solution:} We avoid this ``minor'' obstacle by
      being as close as +sible of deciding the halting
      problem, without actually deciding the halting problem.
      $\quad\Rightarrow$ 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}[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}
         | jump? \meta{Exp} \meta{label}
         | goto \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots\\
\end{plstx}}

\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}
         | jump? \meta{Exp} \meta{label}
         | goto \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots\\
\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:  jump? 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}
         | jmp? \meta{Exp} \meta{label}
         | goto \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots\\
\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{Eval}
\mbox{}\\[-18mm]\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}[language=Scala,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}

Some snippets

\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{:=}\, e::rest]_{env}$ & $\dn$ & 
$[rest]_{(env[x:= [e]_{env}])}$\medskip\\
$[\texttt{jmp?}\;e\;l::rest]_{env}$ & $\dn$ & 
$\begin{cases}
[sn(l)]_{env} & \text{if}\quad[e]_{env} = 1\\
[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 Jump(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}
\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 are 
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]_{env}$ & $\dn$ & 
$\begin{cases}
\{+\} & \text{if}\; n > 0\\
\{-\} & \text{if}\; n < 0\\
\{0\} & \text{if}\; n = 0
\end{cases}$\\
$[x]_{env}$ & $\dn$ & $env(x)$\\
$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} \oplus [e_2]_{env}$\\
$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} \otimes [e_2]_{env}$\\
$[e_1 = e_2]_{env}$ & $\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}[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 \texttt{if} returns \texttt{+} or \texttt{0}
  \item branch into only one dircection 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).
  \end{itemize}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\end{document}


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