7 \usepackage{mathpartir}

     8 

     8 

     9 

     9 % beamer stuff 

    10 % beamer stuff

    11 \newcommand{\bl}[1]{\textcolor{blue}{#1}}

    12 \newcommand{\bl}[1]{\textcolor{blue}{#1}}       

    13 

    27   Office: & N7.07 (North Wing, Bush House)\\

    30   Office: & N\liningnums{7.07} (North Wing, Bush House)\\

    28   Slides: & KEATS (also home work is there)\\

    31   Slides: & KEATS (also homework is there)\\

    31 \end{frame}

    34 

    32 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    35 \end{frame}

    33 

    36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    34 

    37 

    35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    38  

    36   \begin{frame}[c]

    39  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    37 

    40 \begin{frame}[t]

    38   \begin{center}

    41 \frametitle{While Language}

    39   \includegraphics[scale=0.6]{../pics/bridge-limits.png}

    42   

    40   \end{center}

    43 \begin{center}

    41 

    44 \bl{\begin{tabular}{@{}lcl@{}}

    42   \end{frame}

    45 \\[-12mm]        

    43 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    46 \meta{Stmt} & $::=$ &  $\texttt{skip}$\\

    44 

    47               & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\

    45 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    48               & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\

    46   \begin{frame}[c]

    49               & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\

    47   \frametitle{Old-Fashioned Eng.~vs.~CS}

    50               & $|$ & \texttt{read}\;\textit{Id}\\

    48   

    51               & $|$ & \texttt{write}\;\textit{Id}\\

    49   \begin{center}

    52               & $|$ & \texttt{write}\;\textit{String}\medskip\\

    50   \begin{tabular}{@{}cc@{}}

    53 \meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\

    51   \begin{tabular}{@{}p{5.2cm}} 

    54 \meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\

    52   \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ 

    55 \meta{AExp} & $::=$ & \ldots\\

    53   {\bf bridges}: \\

    56 \meta{BExp} & $::=$ & \ldots\\

    54   \raggedright\small

    57 \end{tabular}}

    55   engineers can ``look'' at a bridge and have a pretty good

    58 \end{center}

    56   intuition about whether it will hold up or not\\ 

    59 \end{frame}

    57   (redundancy; predictive theory)

    60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

    58   \end{tabular} &

    61 

    59   \begin{tabular}{p{5cm}} 

    62 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    60   \includegraphics[scale=0.265]{../pics/code.jpg}\\

    63 \begin{frame}[c]

    61   \raggedright

    64 \frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}

    62   {\bf code}: \\

    65 

    63   \raggedright\small

    66 \mbox{}\\[-18mm]\mbox{}

    64   programmers have very little intuition about their code; 

    67 

    65   often it is too expensive to have redundancy;

    68 {\lstset{language=While}\fontsize{10}{12}\selectfont

    66   not ``continuous'' 

    69 \texttt{\lstinputlisting{../progs/fib.while}}}

    67   \end{tabular}

    70 

    68   \end{tabular}

    71 \end{frame}

    69   \end{center}

    72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

    70 

    73 

    71   \end{frame}

    74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    75 \begin{frame}[c,fragile]

    73 

    76 \frametitle{BF***}

    77 

    78 some big array, say \texttt{a}; 7 (8) instructions:

    79 

    80 \begin{itemize}

    81 \item \texttt{>} move \texttt{ptr++}

    82 \item \texttt{<} move \texttt{ptr-{}-}

    83 \item \texttt{+} add \texttt{a[ptr]++}

    84 \item \texttt{-} subtract \texttt{a[ptr]-{}-}

    85 \item \texttt{.} print out \texttt{a[ptr]} as ASCII

    86 \item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}

    87 \item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}

    88 

    89 \end{itemize}  

    90 

    91 \end{frame}

    92 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

    93 

    94 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    95 \begin{frame}[c,fragile]

    96 \frametitle{Arrays in While}

    97 

    98 \begin{itemize}

    99 \item \texttt{new arr[15000]}\medskip 

   100 \item \texttt{x := 3 + arr[3 + y]}\medskip 

   101 \item \texttt{arr[42 * n] := ...}

   102 \end{itemize}  

   103 

   104 \end{frame}

   105 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   106 

   107 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   108 \begin{frame}[c,fragile]

   109 \frametitle{New Arrays}

   110 

   111 \begin{lstlisting}[mathescape,numbers=none,language=While]

   112   new arr[number]

   113 \end{lstlisting}\bigskip\bigskip

   114 

   115 \begin{lstlisting}[mathescape,numbers=none,language=While]

   116   ldc number

   117   newarray int

   118   astore loc_var

   119 \end{lstlisting}

   120 

   121 

   122 \end{frame}

   123 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   124 

   125 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   126 \begin{frame}[c,fragile]

   127 \frametitle{Array Update}

   128 

   129 \begin{lstlisting}[mathescape,numbers=none,language=While]

   130   arr[...] := 

   131 \end{lstlisting}\bigskip\bigskip

   132 

   133 \begin{lstlisting}[mathescape,numbers=none,language=While]

   134   aload loc_var

   135   index_aexp

   136   value_aexp

   137   iastore

   138 \end{lstlisting}

   139 

   140 

   141 \end{frame}

   142 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   143 

   144 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   145 \begin{frame}[c,fragile]

   146 \frametitle{Array Lookup in AExp}

   147 

   148 \begin{lstlisting}[mathescape,numbers=none,language=While]

   149   ...arr[...]... 

   150 \end{lstlisting}\bigskip\bigskip

   151 

   152 \begin{lstlisting}[mathescape,numbers=none,language=While]

   153   aload loc_var

   154   index_aexp

   155   iaload

   156 \end{lstlisting}

   157 

   158 

   159 \end{frame}

   160 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

    85 

   172   

   173   \small

   174   What is good about compilers: the either seem to work,

   175   or go horribly wrong (most of the time).

   176   

   114 quite general (protocols, OS, \ldots).

   205 quite general (compiler, OS, \ldots).

   119 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   210 

   120   \begin{frame}[c]

   211 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   121   \frametitle{\Large{}Mars Pathfinder Mission 1997}

   212 

   122 

   213 \begin{frame}[c]

   123   \begin{center}

   214 \frametitle{Can This Be Done?}

   124   \includegraphics[scale=0.15]{../pics/marspath1.png}

   215 

   125   \includegraphics[scale=0.16]{../pics/marspath3.png}

   216 \begin{itemize}

   126   \includegraphics[scale=0.3]{../pics/marsrover.png}

   217 \item in 2008, verification of a small C-compiler

   127   \end{center}

   128   

   129   \begin{itemize}

   130   \item despite NASA's famous testing procedures, the lander crashed frequently on Mars

   131   \item a scheduling algorithm was not used in the OS

   132   \end{itemize}

   133 

   134   \end{frame}

   135 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   136 

   137 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   138   \begin{frame}[c]

   139   

   140 

   141   \begin{textblock}{11}(1,3)

   142   \begin{tabular}{@{\hspace{-10mm}}l}

   143   \begin{tikzpicture}[scale=1.1]

   144   \node at (-2.5,-1.5) {\textcolor{white}{a}};

   145   \node at (8,4) {\textcolor{white}{a}};

   146   

   147     

   148 

   149   \only<1>{

   150    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   151   }

   152   \only<2>{

   153    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   154    \draw[fill, blue!50] (3,0) rectangle (5,0.6);

   155    \draw[fill, blue!100] (2,3) rectangle (3,3.6);

   156   }

   157   \only<3>{

   158    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   159    \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);

   160    \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);

   161    \draw[fill, blue!100] (2,3) rectangle (3,3.6);

   162    \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);

   163   }

   164   \only<4>{

   165    \node at (2.5,0.9) {\small locked a resource};

   166    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   167    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   168    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   169    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   170   }

   171   \only<5>{

   172    \node at (2.5,0.9) {\small locked a resource};

   173    \draw[fill, blue!50] (1,0) rectangle (4,0.6);

   174    \draw[blue!100, fill] (4,3) rectangle (5, 3.6);

   175   }

   176   \only<6>{

   177    \node at (2.5,0.9) {\small locked a resource};

   178    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   179    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   180    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   181    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   182   }

   183   \only<7>{

   184    \node at (2.5,0.9) {\small locked a resource};

   185    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   186    \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);

   187    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   188    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   189   }

   190   \only<8>{

   191    \node at (2.5,0.9) {\small locked a resource}; 

   192    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   193    \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);

   194    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   195    \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);

   196    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   197    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   198   }

   199   \only<9>{

   200    \node at (2.5,0.9) {\small locked a resource}; 

   201    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   202    \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);

   203    \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);

   204    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   205    \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);

   206   }

   207   \only<10>{

   208    \node at (2.5,0.9) {\small locked a resource}; 

   209    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   210    \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);

   211    \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);

   212    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   213    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   214    \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);

   215   }

   216   \only<11>{

   217    \node at (2.5,0.9) {\small locked a resource};

   218    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   219    \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);

   220    \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);

   221    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   222    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   223    \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);

   224   }

   225   \only<12>{

   226    \node at (2.5,0.9) {\small locked a resource}; 

   227    \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);

   228    \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);

   229    \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);

   230    \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);

   231    \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);

   232    \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);

   233    \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);

   234    \node [anchor=base] at (6.3, 1.8) {\Large\ldots};

   235   }

   236   \only<13>{

   237    \node at (2.5,0.9) {\small locked a resource}; 

   238    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   239    \draw[blue!50, very thick] (2,0) rectangle (4,0.6);

   240    \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);

   241    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   242   }

   243   \only<14>{

   244    \node at (2.5,3.9) {\small locked a resource}; 

   245    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   246    \draw[blue!50, fill] (2,3) rectangle (4,3.6);

   247    \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);

   248    \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);

   249    \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);

   250   }

   251   \only<15>{

   252    \node at (2.5,3.9) {\small locked a resource};  

   253    \draw[fill, blue!50] (1,0) rectangle (2,0.6);

   254    \draw[blue!50, fill] (2,3) rectangle (4,3.6);

   255    \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);

   256    \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);

   257    \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 

   258   }

   259 

   260 

   261   \draw[very thick,->](0,0) -- (8,0);

   262   \node [anchor=base] at (8, -0.3) {\scriptsize time};

   263   \node [anchor=base] at (0, -0.3) {\scriptsize 0};

   264   \node [anchor=base] at (-1.2, 0.2) {\small low priority};

   265   \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}

   266   \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

   267 

   268   \end{tikzpicture}

   269   \end{tabular}

   270   \end{textblock}

   271 

   272   \begin{textblock}{0}(2.5,13)%

   273   \small

   274   \onslide<3->{

   275   \begin{bubble}[8cm]%

   276   Scheduling: You want to avoid that a high 

   277   priority process is starved indefinitely.

   278   \end{bubble}}

   279   \end{textblock}

   280 

   281   \end{frame}

   282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   283   

   284 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   285   \begin{frame}[c]

   286   \frametitle{\Large Priority Inheritance Scheduling}

   287 

   288   \begin{itemize}

   289   \item Let a low priority process $L$ temporarily inherit 

   290     the high priority of $H$ until $L$ leaves the critical 

   291     section unlocking the resource.\bigskip

   292   \item Once the resource is unlocked $L$ returns to its original 

   293     priority level.

   294   \end{itemize}

   295 

   296   \end{frame}

   297 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   298   

   299 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   300   \begin{frame}[c]

   301   

   302   \begin{textblock}{11}(1,3)

   303   \begin{tabular}{@{\hspace{-10mm}}l}

   304   \begin{tikzpicture}[scale=1.1]

   305   \node at (-2.5,-1.5) {\textcolor{white}{a}};

   306   \node at (8,4) {\textcolor{white}{a}};

   307   

   308   \only<1>{

   309     \draw[fill, blue!50] (1,0) rectangle (6,0.6);

   310     \node at (1.5,0.9) {\small $A_L$};

   311     \node at (2.0,0.9) {\small $B_L$};

   312     \node at (3.5,0.9) {\small $A_R$};

   313     \node at (5.7,0.9) {\small $B_R$};

   314     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   315     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   316     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   317     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   318   }

   319   \only<2>{

   320     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   321     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   322     \node at (1.5,0.9) {\small $A_L$};

   323     \node at (2.0,0.9) {\small $B_L$};

   324     \node at (3.5,0.9) {\small $A_R$};

   325     \node at (5.7,0.9) {\small $B_R$};

   326     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   327     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   328     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   329     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   330   }

   331   \only<3>{

   332     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   333     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   334     \node at (1.5,0.9) {\small $A_L$};

   335     \node at (2.0,0.9) {\small $B_L$};

   336     \node at (3.5,0.9) {\small $A_R$};

   337     \node at (5.7,0.9) {\small $B_R$};

   338     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   339     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   340     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   341     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   342     \draw[very thick,blue!100] (3,3) rectangle (4,3.6);

   343     \node at (3.5,3.3) {\small $A$};

   344   }

   345   \only<4>{

   346     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   347     \draw[very thick, blue!50] (3,0) rectangle (6,0.6);

   348     \node at (1.5,0.9) {\small $A_L$};

   349     \node at (2.0,0.9) {\small $B_L$};

   350     \node at (3.5,0.9) {\small $A_R$};

   351     \node at (5.7,0.9) {\small $B_R$};

   352     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   353     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   354     \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);

   355     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   356     \draw[very thick,blue!100] (3,3) rectangle (4,3.6);

   357     \node at (3.5,3.3) {\small $A$};

   358     \draw[very thick,blue!100] (4,3) rectangle (5,3.6);

   359     \node at (4.5,3.3) {\small $B$};

   360   }

   361   \only<5>{

   362     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   363     \draw[very thick, blue!50] (3,3) rectangle (6,3.6);

   364     \node at (1.5,0.9) {\small $A_L$};

   365     \node at (2.0,0.9) {\small $B_L$};

   366     \node at (3.5,3.9) {\small $A_R$};

   367     \node at (5.7,3.9) {\small $B_R$};

   368     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   369     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   370     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   371     \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);

   372     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   373     \node at (6.5,3.3) {\small $A$};

   374     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   375     \node at (7.5,3.3) {\small $B$};

   376     \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);

   377   }

   378   \only<6>{

   379     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   380     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   381     \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);

   382     \node at (1.5,0.9) {\small $A_L$};

   383     \node at (2.0,0.9) {\small $B_L$};

   384     \node at (3.5,3.9) {\small $A_R$};

   385     \node at (5.7,3.9) {\small $B_R$};

   386     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   387     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   388     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   389     \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);

   390     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   391     \node at (6.5,3.3) {\small $A$};

   392     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   393     \node at (7.5,3.3) {\small $B$}; 

   394   }

   395   \only<7>{

   396    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   397     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   398     \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);

   399     \node at (1.5,0.9) {\small $A_L$};

   400     \node at (2.0,0.9) {\small $B_L$};

   401     \node at (3.5,3.9) {\small $A_R$};

   402     \node at (5.7,0.9) {\small $B_R$};

   403     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   404     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   405     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   406     \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);

   407     \draw[very thick,blue!100] (6,3) rectangle (7,3.6);

   408     \node at (6.5,3.3) {\small $A$};

   409     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   410     \node at (7.5,3.3) {\small $B$};  

   411     \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);

   412     \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);

   413   }

   414   \only<8>{

   415     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   416     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   417     \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);

   418     \node at (1.5,0.9) {\small $A_L$};

   419     \node at (2.0,0.9) {\small $B_L$};

   420     \node at (3.5,3.9) {\small $A_R$};

   421     \node at (6.7,0.9) {\small $B_R$};

   422     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   423     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   424     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   425     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   426     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   427     \node at (4,3.3) {\small $A$};

   428     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   429     \node at (7.5,3.3) {\small $B$};  

   430   }

   431   \only<9>{

   432     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   433     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   434     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   435     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   436     \node at (1.5,0.9) {\small $A_L$};

   437     \node at (2.0,0.9) {\small $B_L$};

   438     \node at (3.5,3.9) {\small $A_R$};

   439     \node at (6.7,0.9) {\small $B_R$};

   440     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   441     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   442     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   443     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   444     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   445     \node at (4,3.3) {\small $A$};

   446     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   447     \node at (7.5,3.3) {\small $B$};  

   448   }

   449   \only<10>{

   450     \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   451     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   452     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   453     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   454     \node at (1.5,0.9) {\small $A_L$};

   455     \node at (2.0,0.9) {\small $B_L$};

   456     \node at (3.5,3.9) {\small $A_R$};

   457     \node at (6.7,0.9) {\small $B_R$};

   458     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   459     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   460     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   461     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   462     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   463     \node at (4,3.3) {\small $A$};

   464     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   465     \node at (7.5,3.3) {\small $B$};  

   466     \draw[red, fill] (5,1.5) rectangle (6,2.1);

   467     \draw[red, fill] (6.05,1.5) rectangle (7,2.1);

   468   }

   469   \only<11>{

   470    \draw[fill, blue!50] (1,0) rectangle (3,0.6);

   471     \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);

   472     \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);

   473     \draw[very thick, blue!50] (5,0) rectangle (7,0.6);

   474     \node at (1.5,0.9) {\small $A_L$};

   475     \node at (2.0,0.9) {\small $B_L$};

   476     \node at (3.5,3.9) {\small $A_R$};

   477     \node at (6.7,0.9) {\small $B_R$};

   478     \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);

   479     \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);

   480     \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);

   481     \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);

   482     \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);

   483     \node at (4,3.3) {\small $A$};

   484     \draw[very thick,blue!100] (7,3) rectangle (8,3.6);

   485     \node at (7.5,3.3) {\small $B$};  

   486     \draw[red, fill] (5,1.5) rectangle (6,2.1);

   487     \draw[red, fill] (6.05,1.5) rectangle (7,2.1);

   488     \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);

   489     \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);

   490   }

   491 

   492   \draw[very thick,->](0,0) -- (8,0);

   493   \node [anchor=base] at (8, -0.3) {\scriptsize time};

   494   \node [anchor=base] at (0, -0.3) {\scriptsize 0};

   495   \node [anchor=base] at (-1.2, 0.2) {\small low priority};

   496   \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}

   497   \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

   498 

   499   \end{tikzpicture}

   500   \end{tabular}

   501   \end{textblock}

   502   

   503   \begin{textblock}{0}(2.5,13)%

   504   \small

   505   \onslide<11>{

   506   \begin{bubble}[8cm]%

   507   Scheduling: You want to avoid that a high 

   508   priority process is staved indefinitely.

   509   \end{bubble}}

   510   \end{textblock}

   511 

   512 

   513   \end{frame}

   514 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   515   

   516 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   517   \begin{frame}[c]

   518   \frametitle{\Large Priority Inheritance Scheduling}

   519 

   520   \begin{itemize}

   521   \item Let a low priority process $L$ temporarily inherit 

   522     the high priority of $H$ until $L$ leaves the critical 

   523     section unlocking the resource.\bigskip

   524   \item Once the resource is unlocked $L$ returns to its original 

   525     priority level. \alert{\bf BOGUS}\pause\bigskip

   526   \item \ldots $L$ needs to switch to the highest 

   527     \alert{remaining} priority of the threads that it blocks.

   528   \end{itemize}\bigskip

   529 

   530   \small this error is already known since around 1999

   531 

   532   \end{frame}

   533 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   534 

   535 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   536   \begin{frame}[c]

   537 

   538   \begin{center}

   539   \includegraphics[scale=0.25]{../pics/p3.jpg}

   540   \end{center}

   541 

   542    \begin{itemize}

   543   \item by Rajkumar, 1991

   544   \item \it ``it resumes the priority it had at the point of entry into the critical 

   545   section''

   546   \end{itemize}

   547 

   548   \end{frame}

   549 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   550      

   551 

   552 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   553   \begin{frame}[c]

   554 

   555   \begin{center}

   556   \includegraphics[scale=0.25]{../pics/p2.jpg}

   557   \end{center}

   558 

   559    \begin{itemize}

   560   \item by Jane Liu, 2000

   561   \item {\it ``The job $J_l$ executes at its inherited 

   562     priority until it releases $R$; at that time, the 

   563     priority of $J_l$ returns to its priority 

   564     at the time when it acquires the resource $R$.''}\medskip

   565   \item \small gives pseudo code and totally bogus data structures  

   566   \item \small interesting part ``{\it left as an exercise}''

   567   \end{itemize}

   568 

   569   \end{frame}

   570 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   571      

   572 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   573   \begin{frame}[c]

   574 

   575   \begin{center}

   576   \includegraphics[scale=0.15]{../pics/p1.pdf}

   577   \end{center}

   578 

   579   \begin{itemize}

   580   \item by Laplante and Ovaska, 2011 (\$113.76)

   581   \item \it ``when $[$the task$]$ exits the critical section that

   582         caused the block, it reverts to the priority it had

   583         when it entered that section'' 

   584   \end{itemize}

   585 

   586   \end{frame}

   587 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   588   

   589 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   590   \begin{frame}[c]

   591 

   592   \begin{center}

   593   \includegraphics[scale=0.25]{../pics/p4.jpg}

   594   \end{center}

   595 

   596   \begin{itemize}

   597   \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)

   598   \item \it ``Upon releasing the lock, the 

   599   $[$low-priority$]$ thread will revert to 

   600   its original priority.''

   601   \end{itemize}

   602 

   603   \end{frame}

   604 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   605    

   606   

   607 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   608   \begin{frame}[c]

   609   \frametitle{Priority Scheduling}

   610 

   611   \begin{itemize}

   612   \item a scheduling algorithm that is widely used in real-time operating systems

   613   \item has been ``proved'' correct by hand in a paper in 1983

   614   \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause

   615   

   616   \item we used the corrected algorithm and then {\bf really} proved

   617     that it is correct

   618     

   619   \item we implemented this algorithm in a small OS called PINTOS

   620     (used for teaching at Stanford)

   621     

   622   \item our implementation was much more efficient than their

   623     reference implementation

   624 

   625   \end{itemize}

   626 

   627   \end{frame}

   628 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   629    

   630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   631 

   632 \begin{frame}[c]

   633 \frametitle{Big Proofs in CS (1)}

   634 

   635 Formal proofs in CS sound like science fiction?

   636 

   637 \begin{itemize}

   638 \item in 2008, verification of a C-compiler

   641 \item is as good as \texttt{gcc -O1}, but much less buggy 

   220 \item is as good as \texttt{gcc -O1}, but much, much less buggy 

   653 % \begin{frame}[c]

   232 \begin{frame}[c]

   654 % \frametitle{Fuzzy Testing C-Compilers}

   233 \frametitle{Fuzzy Testing C-Compilers}

   655 

   234 

   656 % \begin{itemize}

   235 \begin{itemize}

   657 % \item tested GCC, LLVM and others by randomly generating 

   236 \item tested GCC, LLVM and others by randomly generating 

   658 % C-programs

   237 C-programs

   659 % \item found more than 300 bugs in GCC and also

   238 \item found more than 300 bugs in GCC and also

   660 % many in LLVM (some of them highest-level critical)\bigskip

   239 many in LLVM (some of them highest-level critical)\bigskip

   661 % \item about CompCert:

   240 \item about CompCert:

   662 

   241 

   663 % \begin{bubble}[10cm]\small ``The striking thing about our CompCert

   242 \begin{bubble}[10cm]\small ``The striking thing about our CompCert

   664 % results is that the middle-end bugs we found in all other

   243 results is that the middle-end bugs we found in all other

   665 % compilers are absent. As of early 2011, the under-development

   244 compilers are absent. As of early 2011, the under-development

   666 % version of CompCert is the only compiler we have tested for

   245 version of CompCert is the only compiler we have tested for

   667 % which Csmith cannot find wrong-code errors. This is not for

   246 which Csmith cannot find wrong-code errors. This is not for

   668 % lack of trying: we have devoted about six CPU-years to the

   247 lack of trying: we have devoted about six CPU-years to the

   669 % task.'' 

   248 task.'' 

   670 % \end{bubble} 

   249 \end{bubble} 

   671 % \end{itemize}

   672 

   673 % \end{frame}

   674 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   675 

   676 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   677 \begin{frame}[c]

   678 \frametitle{Big Proofs in CS (2)}

   679 

   680 \begin{itemize}

   681 \item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)

   682   \begin{itemize}

   683   \item used in helicopters and mobile phones

   684   \item 200k loc of proof

   685   \item 25 - 30 person years

   686   \item found 160 bugs in the C code (144 by the proof)

   687   \end{itemize}

   690 \begin{bubble}[10cm]\small

   252 \end{frame}

   691 ``Real-world operating-system kernel with an end-to-end proof

   253 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   692 of implementation correctness and security enforcement''

   693 \end{bubble}\bigskip\pause

   694 

   695 unhackable kernel (New Scientists, September 2015)

   696 \end{frame}

   697 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   698 

   699 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   700 \begin{frame}[c]

   701 \frametitle{Big Proofs in CS (3)}

   702 

   703 \begin{itemize}

   704 \item verified TLS implementation\medskip

   705 \item verified compilers (CompCert, CakeML)\medskip

   706 \item verified distributed systems (Verdi)\medskip

   707 \item verified OSes or OS components\\

   708 (seL4, CertiKOS, \ldots)\bigskip\pause

   709 \item Infer static analyser developed by Facebook  

   710 \end{itemize}

   711 

   712 \end{frame}

   713 

   714 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   715 \begin{frame}[c]

   716 \frametitle{How Did This Happen?}

   717 

   718 Lots of ways!

   719 

   720 \begin{itemize}

   721 \item better programming languages

   722   \begin{itemize}

   723   \item basic safety guarantees built in

   724   \item powerful mechanisms for abstraction and modularity

   725   \end{itemize}

   726 \item better software development methodology

   727 \item stable platforms and frameworks

   728 \item better use of specifications\medskip\\

   729   \small If you want to build software that works or is secure, 

   730     it is helpful to know what you mean by ``works'' and by ``is secure''!

   731 \end{itemize}

   732 

   733 \end{frame}

   734 

   735 

   736 

   737 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   738 \begin{frame}[c]

   739 \frametitle{Goal}

   740 

   741 Remember the Bridges example?

   742 

   743 \begin{itemize}

   744 \item Can we look at our programs and somehow ensure

   745 they are bug free/correct?\pause\bigskip

   746 

   747 \item Very hard: Anything interesting about programs is equivalent

   748 to the Halting Problem, which is undecidable.\pause\bigskip

   749 

   750 \item \alert{Solution:} We avoid this ``minor'' obstacle by

   751       being as close as possible of deciding the halting

   752       problem, without actually deciding the halting problem.

   753       \small$\quad\Rightarrow$ yes, no, don't know (static analysis)

   754 \end{itemize}

   755 

   756 \end{frame}

   757 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   758 

   759 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   760   \begin{frame}[c]

   761   \frametitle{What is Static Analysis?}

   762 

   763   \begin{center}

   764   \includegraphics[scale=0.4]{../pics/state.png}

   765   \end{center}

   766   

   767   \begin{itemize}

   768   \item depending on some initial input, a program 

   769   (behaviour) will ``develop'' over time.

   770   \end{itemize}

   771 

   772   \end{frame}

   773 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   774 

   775 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   776   \begin{frame}[c]

   777   \frametitle{What is Static Analysis?}

   778 

   779   \begin{center}

   780   \includegraphics[scale=0.4]{../pics/state2.png}

   781   \end{center}

   782 

   783   \end{frame}

   784 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   785 

   786 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   787   \begin{frame}[c]

   788   \frametitle{What is Static Analysis?}

   789 

   790   \begin{center}

   791   \includegraphics[scale=0.4]{../pics/state3.jpg}

   792   \end{center}

   793 

   794   \end{frame}

   795 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   796 

   797 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   798   \begin{frame}[c]

   799   \frametitle{What is Static Analysis?}

   800 

   801   \begin{center}

   802   \includegraphics[scale=0.4]{../pics/state4.jpg}

   803   \end{center}

   804 

   805   \begin{itemize}

   806   \item to be avoided

   807   \end{itemize}

   808 

   809   \end{frame}

   810 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   811 

   812 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   813   \begin{frame}[c]

   814   \frametitle{What is Static Analysis?}

   815 

   816   \begin{center}

   817   \includegraphics[scale=0.4]{../pics/state5.png}

   818   \end{center}

   819   

   820   \begin{itemize}

   821   \item this needs more work

   822   \end{itemize}

   823 

   824   \end{frame}

   825 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   826 

   827 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   828   \begin{frame}[c]

   829   \frametitle{What is Static Analysis?}

   830 

   831   \begin{center}

   832   \includegraphics[scale=0.4]{../pics/state6.png}

   833   \end{center}

   834   

   835   \end{frame}

   836 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   837 

   838 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   839   \begin{frame}[c,fragile]

   840     \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   841                   Are Vars Definitely Initialised?\end{tabular}}

   842 

   843 Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip

   844 

   845 Prog.~1:\\

   846 \begin{lstlisting}[numbers=none,

   847                    basicstyle=\ttfamily,

   848                    language=While,xleftmargin=3mm]

   849 if x < 1 then y := x else y := x + 1;

   850 y := y + 1

   851 \end{lstlisting}\medskip     

   852 

   853 Prog.~2:\\

   854 \begin{lstlisting}[numbers=none,

   855                    basicstyle=\ttfamily,

   856                    language=While,xleftmargin=3mm]

   857 if x < x then y := y + 1 else y := x;

   858 y := y + 1

   859 \end{lstlisting}            

   860 

   861   \end{frame}

   862 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   863 

   864 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   865   \begin{frame}[c,fragile]

   866     \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   867                   Are Vars Definitely Initialised?\end{tabular}}

   868 

   869               What should the rules be for deciding when a

   870               variable is initialised?\bigskip\pause

   871 

   872 \begin{itemize}

   873 \item variable \texttt{x} is definitely initialized after

   874   \texttt{skip}\\

   875   iff \texttt{x} is definitely initialized before \texttt{skip}.

   876 \end{itemize}

   877   

   878 \end{frame}

   879 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   880 

   881 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   882   \begin{frame}[c,fragile]

   883 %    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   884 %                  Are Vars Definitely Initialised?\end{tabular}}

   885 

   886 $\bl{A}$ is the set of definitely defined variables:

   887               

   888 \begin{center}

   889 \begin{tabular}{c}

   890   \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad

   891   \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}}

   892   \medskip\\\pause

   893 

   894   \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}}

   895   \medskip\\\pause

   896   

   897   \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2}

   898   {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}}

   899   \medskip\\\pause

   900 

   901   \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'}

   902   {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause

   903 \end{tabular}  

   904 \end{center}

   905 

   906 \hfill we start with $\bl{A = \{\}}$

   907 \end{frame}

   908 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   909 

   910 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   911 \begin{frame}[fragile]

   912 \frametitle{\large Concrete Example: Sign-Analysis}

   913 \mbox{}\\[-20mm]\mbox{}

   914 

   915 \bl{\begin{plstx}[rhs style=,one per line]

   916 : \meta{Exp} ::= \meta{Exp} + \meta{Exp}

   917          | \meta{Exp} * \meta{Exp}

   918          | \meta{Exp} = \meta{Exp} 

   919          | \meta{num}

   920          | \meta{var}\\

   921 : \meta{Stmt} ::= \meta{label} :

   922          | \meta{var} := \meta{Exp}

   923          | \pcode{jmp?} \meta{Exp} \meta{label}

   924          | \pcode{goto} \meta{label}\\

   925 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\

   926 \end{plstx}}

   927 

   928 \begin{textblock}{0}(7.8,2.5)

   929 \small

   930 \begin{bubble}[5.6cm]

   931 \begin{lstlisting}[numbers=none,

   932                    basicstyle=\ttfamily,

   933                    language={},xleftmargin=3mm]

   934       a := 1

   935       n := 5 

   936 top:  jmp? n = 0 done 

   937       a := a * n 

   938       n := n + -1 

   939       goto top 

   940 done:

   941 \end{lstlisting}

   942 \end{bubble}

   943 \end{textblock}

   944 

   945 \end{frame}

   946 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   947 

   948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   949 \begin{frame}[fragile]

   950 \frametitle{\large Concrete Example: Sign-Analysis}

   951 \mbox{}\\[-20mm]\mbox{}

   952 

   953 \bl{\begin{plstx}[rhs style=,one per line]

   954 : \meta{Exp} ::= \meta{Exp} + \meta{Exp}

   955          | \meta{Exp} * \meta{Exp}

   956          | \meta{Exp} = \meta{Exp} 

   957          | \meta{num}

   958          | \meta{var}\\

   959 : \meta{Stmt} ::= \meta{label} :

   960          | \meta{var} := \meta{Exp}

   961          | \pcode{jmp?} \meta{Exp} \meta{label}

   962          | \pcode{goto} \meta{label}\\

   963 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\

   964 \end{plstx}}

   965 

   966 \begin{textblock}{0}(7.8,3.5)

   967 \small

   968 \begin{bubble}[5.6cm]

   969 \begin{lstlisting}[numbers=none,

   970                    basicstyle=\ttfamily,

   971                    language={},xleftmargin=3mm]

   972       n := 6

   973       m1 := 0

   974       m2 := 1

   975 top:  jmp? n = 0 done

   976       tmp := m2

   977       m2 := m1 + m2

   978       m1 := tmp

   979       n := n + -1

   980       goto top

   981 done:

   982 \end{lstlisting}

   983 \end{bubble}

   984 \end{textblock}

   985 

   986 \end{frame}

   987 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   988 

   989 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   990 \begin{frame}[fragile]

   991 \frametitle{\large Concrete Example: Sign-Analysis}

   992 \mbox{}\\[-20mm]\mbox{}

   993 

   994 \bl{\begin{plstx}[rhs style=,one per line]

   995 : \meta{Exp} ::= \meta{Exp} + \meta{Exp}

   996          | \meta{Exp} * \meta{Exp}

   997          | \meta{Exp} = \meta{Exp} 

   998          | \meta{num}

   999          | \meta{var}\\

  1000 : \meta{Stmt} ::= \meta{label} :

  1001          | \meta{var} := \meta{Exp}

  1002          | \pcode{jmp?} \meta{Exp} \meta{label}

  1003          | \pcode{goto} \meta{label}\\

  1004 : \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\

  1005 \end{plstx}}

  1006 

  1007 \end{frame}

  1008 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1009 

  1010 

  1011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1012 \begin{frame}[fragile]

  1013 \frametitle{Eval: An Interpreter}

  1014 \mbox{}\\[-14mm]\mbox{}

  1015 

  1016 \small

  1017 \begin{center}

  1018 \bl{\begin{tabular}{lcl}

  1019 $[n]_{env}$ & $\dn$ & $n$\\

  1020 $[x]_{env}$ & $\dn$ & $env(x)$\\

  1021 $[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\

  1022 $[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\

  1023 $[e_1 = e_2]_{env}$ & $\dn$ & 

  1024 $\begin{cases}

  1025 1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\

  1026 0 & \text{otherwise}

  1027 \end{cases}$\\

  1028 \end{tabular}}

  1029 \end{center}

  1030 

  1031 \footnotesize

  1032 \begin{lstlisting}[numbers=none,xleftmargin=-5mm]

  1033 def eval_exp(e: Exp, env: Env) : Int = e match {

  1034   case Num(n) => n

  1035   case Var(x) => env(x)

  1036   case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env)

  1037   case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env)

  1038   case Equ(e1, e2) => 

  1039     if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0

  1040 }

  1041 \end{lstlisting}

  1042 

  1043 \end{frame}

  1044 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1045 

  1046 

  1047 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1048 \begin{frame}[fragile]

  1049 \small

  1050 A program

  1051 \begin{bubble}[6cm]\footnotesize

  1052 \begin{lstlisting}[numbers=none,

  1053                    language={},

  1054                    basicstyle=\ttfamily,

  1055                    xleftmargin=1mm]

  1056       a := 1

  1057       n := 5 

  1058 top:  jmp? n = 0 done 

  1059       a := a * n 

  1060       n := n + -1 

  1061       goto top 

  1062 done:

  1063 \end{lstlisting}

  1064 \end{bubble}

  1065 

  1066 The \emph{snippets} of the program: