--- a/slides/slides09.tex Wed Nov 22 18:27:59 2017 +0000
+++ b/slides/slides09.tex Wed Nov 29 08:47:22 2017 +0000
@@ -1,52 +1,23 @@
\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
-\usepackage{../data}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}
-
-\tikzset{onslide/.code args={<#1>#2}{%
- \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
-}}
-
-\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}}
+\usepackage{mathpartir}
-\newcommand<>\btHL[1][]{%
- \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
-}
-\def\bt@HL@endenv{%b jm
- \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
-
-\lstset{morekeywords={def,if,then,else,write,read},keywordstyle=\color{codepurple}\bfseries}
-
-% 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{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
\LARGE Compilers and \\[-2mm]
- \LARGE Formal Languages (8)\\[3mm]
+ \LARGE Formal Languages (9)\\[3mm]
\end{tabular}}
\normalsize
@@ -57,613 +28,50 @@
Slides: & KEATS (also home work is there)\\
\end{tabular}
\end{center}
-
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t,fragile]
-\frametitle{Compiling AExps}
-For example \bl{$1 + ((2 * 3) + (4 - 3))$}:\medskip
-
-\begin{columns}[T]
-\begin{column}{.3\textwidth}
-\begin{center}
-\bl{\begin{tikzpicture}
-\tikzset{level distance=12mm,sibling distance=4mm}
-\tikzset{edge from parent/.style={draw,very thick}}
\Tree [.$+$ [.$1$ ] [.$+$ [.$*$ $2$ $3$ ] [.$-$ $4$ $3$ ]]]
\end{tikzpicture}}
-\end{center}
-\end{column}
-\begin{column}{.3\textwidth}
-\begin{lstlisting}[language=JVMIS,numbers=none]
-ldc 1
-ldc 2
-ldc 3
-imul
-ldc 4
-ldc 3
-isub
-iadd
-iadd
-\end{lstlisting}
-\end{column}
-\end{columns}\bigskip
-
-\small
-Traverse tree in post-order \bl{$\Rightarrow$} code for
-stack-machine
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Compiling AExps}
-
-\bl{
-\begin{center}
-\begin{tabular}{lcl}
-$\textit{compile}(n, E)$ & $\dn$ & $\pcode{ldc}\;n$\smallskip\\
-$\textit{compile}(a_1 + a_2, E)$ & $\dn$ \\
-\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\;\textit{compile}(a_2, E)\;@\; \pcode{iadd}$}\smallskip\\
-$\textit{compile}(a_1 - a_2, E)$ & $\dn$ \\
-\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{isub}$}\smallskip\\
-$\textit{compile}(a_1 * a_2, E)$ & $\dn$ \\
-\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{imul}$}\smallskip\\
-$\textit{compile}(a_1 \backslash a_2, E)$ & $\dn$\\
-\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{idiv}$}\smallskip\\
-$\textit{compile}(x, E)$ & $\dn$ & $\pcode{iload}\;E(x)$\\
-\end{tabular}
-\end{center}}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Compiling Ifs}
-
-For example
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-if 1 = 1 then x := 2 else y := 3
-\end{lstlisting}
-
-
-\begin{center}
-\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
- ldc 1
- ldc 1
- if_icmpne L_ifelse $\quad\tikz[remember picture] \node (C) {\mbox{}};$
- ldc 2
- istore 0
- goto L_ifend $\quad\tikz[remember picture] \node (A) {\mbox{}};$
-L_ifelse: $\quad\tikz[remember picture] \node[] (D) {\mbox{}};$
- ldc 3
- istore 1
-L_ifend: $\quad\tikz[remember picture] \node[] (B) {\mbox{}};$
-\end{lstlisting}
-\end{center}
-
-\begin{tikzpicture}[remember picture,overlay]
\draw[->,very thick] (A) edge [->,to path={-- ++(10mm,0mm)
- -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (B.east);
- \draw[->,very thick] (C) edge [->,to path={-- ++(10mm,0mm)
- -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (D.east);
\end{tikzpicture}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Compiling Whiles}
+ \begin{center}
+ \includegraphics[scale=0.6]{../pics/bridge-limits.png}
+ \end{center}
-For example
-
-\begin{lstlisting}[mathescape,numbers=none,language=While]
-while x <= 10 do x := x + 1
-\end{lstlisting}
-
-
-\begin{center}
-\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
-L_wbegin: $\quad\tikz[remember picture] \node[] (LB) {\mbox{}};$
- iload 0
- ldc 10
- if_icmpgt L_wend $\quad\tikz[remember picture] \node (LC) {\mbox{}};$
- iload 0
- ldc 1
- iadd
- istore 0
- goto L_wbegin $\quad\tikz[remember picture] \node (LA) {\mbox{}};$
-L_wend: $\quad\tikz[remember picture] \node[] (LD) {\mbox{}};$
-\end{lstlisting}
-\end{center}
-
-\begin{tikzpicture}[remember picture,overlay]
- \draw[->,very thick] (LA) edge [->,to path={-- ++(12mm,0mm)
- -- ++(0mm,17.3mm) |- (\tikztotarget)},line width=1mm] (LB.east);
- \draw[->,very thick] (LC) edge [->,to path={-- ++(12mm,0mm)
- -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (LD.east);
\end{tikzpicture}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Compiling Writes}
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\small
-\begin{lstlisting}[language=JVMIS,mathescape,
- numbers=none,xleftmargin=-6mm]
-.method public static write(I)V
- .limit locals 1
- .limit stack 2
- getstatic java/lang/System/out
- Ljava/io/PrintStream;
- iload 0
- invokevirtual java/io/PrintStream/println(I)V
- return
-.end method
-
-
-
-iload $E(x)$
-invokestatic XXX/XXX/write(I)V
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Compiling Main}
-
-\footnotesize
-\begin{lstlisting}[language=JVMIS,mathescape,
- numbers=none,xleftmargin=-6mm]
-.class public XXX.XXX
-.super java/lang/Object
-
-.method public <init>()V
- aload_0
- invokenonvirtual java/lang/Object/<init>()V
- return
-.end method
-
-.method public static main([Ljava/lang/String;)V
- .limit locals 200
- .limit stack 200
-
- $\textit{\ldots{}here comes the compiled code\ldots}$
-
- return
-.end method
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Functional Programming}
-
-\footnotesize
-\begin{textblock}{13}(0.9,3)
-\begin{lstlisting}[]numbers=none]
-def fib(n) = if n == 0 then 0
- else if n == 1 then 1
- else fib(n - 1) + fib(n - 2);
-
-def fact(n) = if n == 0 then 1 else n * fact(n - 1);
-
-def ack(m, n) = if m == 0 then n + 1
- else if n == 0 then ack(m - 1, 1)
- else ack(m - 1, ack(m, n - 1));
-
-def gcd(a, b) = if b == 0 then a else gcd(b, a % b);
-\end{lstlisting}
-\end{textblock}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \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{Fun Grammar}
-\bl{
-\begin{plstx}[rhs style=]
-: \meta{Exp} ::= \meta{Var} | \meta{Num}{\hspace{3cm}}
- | \meta{Exp} + \meta{Exp} | ... | (\meta{Exp})
- | \code{if} \meta{BExp} \code{then} \meta{Exp} \code{else} \meta{Exp}
- | \code{write} \meta{Exp} {\hspace{3cm}}
- | \meta{Exp} ; \meta{Exp}
- | \textit{FunName} (\meta{Exp}, ... , \meta{Exp})\\
-: \meta{BExp} ::= ...\\
-: \meta{Decl} ::= \meta{Def} ; \meta{Decl}
- | \meta{Exp}\\
-: \meta{Def} ::= \code{def} \textit{FunName} ($\hspace{0.4mm}x_1$, ... , $x_n$) = \meta{Exp}\\
-\end{plstx}}
-
-
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Abstract Syntax Trees}
-
-\footnotesize
-\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]
-abstract class Exp
-abstract class BExp
-abstract class Decl
-
-case class Var(s: String) extends Exp
-case class Num(i: Int) extends Exp
-case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
-case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
-case class Write(e: Exp) extends Exp
-case class Sequ(e1: Exp, e2: Exp) extends Exp
-case class Call(name: String, args: List[Exp]) extends Exp
-
-case class Bop(o: String, a1: Exp, a2: Exp) extends BExp
-
-case class Def(name: String,
- args: List[String],
- body: Exp) extends Decl
-case class Main(e: Exp) extends Decl
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Sequences}
-
-Compiling \texttt{exp1 ; exp2}:\bigskip
-
-
-\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
-$\textit{compile}$(exp1)
-pop
-$\textit{compile}$(exp2)
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Write}
-
-Compiling call to \texttt{write(1+2)}:\bigskip
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
-$\textit{compile}$(1+2)
-dup
-invokestatic XXX/XXX/write(I)V
-\end{lstlisting}\bigskip
-
-\small
-needs the helper method
-
-\footnotesize
-\begin{lstlisting}[language=JVMIS,
- xleftmargin=2mm,
- numbers=none]
-.method public static write(I)V
- .limit locals 1
- .limit stack 2
- getstatic java/lang/System/out Ljava/io/PrintStream;
- iload 0
- invokevirtual java/io/PrintStream/println(I)V
- return
-.end method
-\end{lstlisting}
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t, fragile]
-\frametitle{Function Definitions}
-
-\footnotesize
-\begin{lstlisting}[language=JVMIS,
- xleftmargin=2mm,
- numbers=none]
-.method public static write(I)V
- .limit locals 1
- .limit stack 2
- getstatic java/lang/System/out Ljava/io/PrintStream;
- iload 0
- invokevirtual java/io/PrintStream/println(I)V
- return
-.end method
-\end{lstlisting}\bigskip
-
-\small We will need for definitions, like\footnotesize\medskip
-
-\begin{lstlisting}[language=JVMIS,
- xleftmargin=2mm,
- numbers=none]
-def fname (x1, ... , xn) = ...
-
-.method public static fname (I...I)I
- .limit locals ??
- .limit stack ??
- ??
-.end method
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Stack Estimation}
-\small
-\mbox{}\\[-15mm]
-
-\bl{\begin{center}
-\begin{tabular}{@{\hspace{-4mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
-$\textit{estimate}(n)$ & $\dn$ & $1$\\
-$\textit{estimate}(x)$ & $\dn$ & $1$\\
-$\textit{estimate}(a_1\;aop\;a_2)$ & $\dn$ &
-$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
-$\textit{estimate}(\pcode{if}\;b\;\pcode{then}\;e_1\;\pcode{else}\;e_2)$ & $\dn$ &
-$\textit{estimate}(b) +$\\
-& & $\quad max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
-$\textit{estimate}(\pcode{write}(e))$ & $\dn$ &
-$\textit{estimate}(e) + 1$\\
-$\textit{estimate}(e_1 ; e_2)$ & $\dn$ &
-$max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
-$\textit{estimate}(f(e_1, ..., e_n))$ & $\dn$ &
-$\sum_{i = 1..n}\;estimate(e_i)$\medskip\\
-$\textit{estimate}(a_1\;bop\;a_2)$ & $\dn$ &
-$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
-\end{tabular}
-\end{center}}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile]
-\frametitle{Successor Function}
-
-\begin{textblock}{7}(1,2.5)\footnotesize
-\begin{minipage}{6cm}
-\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
-.method public static suc(I)I
-.limit locals 1
-.limit stack 2
- iload 0
- ldc 1
- iadd
- ireturn
-.end method
-\end{lstlisting}
-\end{minipage}
-\end{textblock}
-
-\begin{textblock}{7}(6,8)
-\begin{bubble}[5cm]\small
-\begin{lstlisting}[language=Lisp,
- basicstyle=\ttfamily,
- numbers=none,
- xleftmargin=1mm]
-def suc(x) = x + 1;
-\end{lstlisting}
-\end{bubble}
-\end{textblock}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile]
-\frametitle{Addition Function}
-
-\begin{textblock}{7}(1,1.9)\footnotesize
-\begin{minipage}{6cm}
-\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
-.method public static add(II)I
-.limit locals 2
-.limit stack 5
- iload 0
- ldc 0
- if_icmpne If_else
- iload 1
- goto If_end
-If_else:
- iload 0
- ldc 1
- isub
- iload 1
- invokestatic XXX/XXX/add(II)I
- invokestatic XXX/XXX/suc(I)I
-If_end:
- ireturn
-.end method
-\end{lstlisting}
-\end{minipage}
-\end{textblock}
-
-\begin{textblock}{7}(6,6.6)
-\begin{bubble}[7cm]\small
-\begin{lstlisting}[language=Lisp,
- basicstyle=\ttfamily,
- numbers=none,
- xleftmargin=1mm]
-def add(x, y) =
- if x == 0 then y
- else suc(add(x - 1, y));
-\end{lstlisting}
-\end{bubble}
-\end{textblock}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile]
-\frametitle{Factorial}
-
-\begin{textblock}{7}(1,1.5)\footnotesize
-\begin{minipage}{6cm}
-\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
-.method public static facT(II)I
-.limit locals 2
-.limit stack 6
- iload 0
- ldc 0
- if_icmpne If_else_2
- iload 1
- goto If_end_3
-If_else_2:
- iload 0
- ldc 1
- isub
- iload 0
- iload 1
- imul
- invokestatic fact/fact/facT(II)I
-If_end_3:
- ireturn
-.end method
-\end{lstlisting}
-\end{minipage}
-\end{textblock}
-
-\begin{textblock}{7}(6,7)
-\begin{bubble}[7cm]\small
-\begin{lstlisting}[language=Lisp,
- basicstyle=\ttfamily,
- numbers=none,
- xleftmargin=1mm]
-def facT(n, acc) =
- if n == 0 then acc
- else facT(n - 1, n * acc);
-\end{lstlisting}
-\end{bubble}
-\end{textblock}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[fragile]
-
-\begin{textblock}{7}(1,-0.2)\footnotesize
-\begin{minipage}{6cm}
-\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
-.method public static facT(II)I
-.limit locals 2
-.limit stack 6
-(*@\hl{facT\_Start:} @*)
- iload 0
- ldc 0
- if_icmpne If_else_2
- iload 1
- goto If_end_3
-If_else_2:
- iload 0
- ldc 1
- isub
- iload 0
- iload 1
- imul
- (*@\hl{istore 1} @*)
- (*@\hl{istore 0} @*)
- (*@\hl{goto facT\_Start} @*)
-If_end_3:
- ireturn
-.end method
-\end{lstlisting}
-\end{minipage}
-\end{textblock}
-
-\begin{textblock}{7}(6,7)
-\begin{bubble}[7cm]\small
-\begin{lstlisting}[language=Lisp,
- basicstyle=\ttfamily,
- numbers=none,
- xleftmargin=1mm]
-def facT(n, acc) =
- if n == 0 then acc
- else facT(n - 1, n * acc);
-\end{lstlisting}
-\end{bubble}
-\end{textblock}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Tail Recursion}
-
-A call to \texttt{f(args)} is usually compiled as\medskip
-
-{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
- args onto stack
- invokestatic .../f
-\end{lstlisting}}\pause
-
-
-A call is in tail position provided:\medskip
-
-{\small\begin{itemize}
-\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
-\item \texttt{Exp ; \hl{Exp}}
-\item \texttt{Exp op Exp}
-\end{itemize}}\medskip
-
-then a call \texttt{f(args)} can be compiled as\medskip\small
-
-\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
- prepare environment
- jump to start of function
-\end{lstlisting}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
-\frametitle{Tail Recursive Call}
-\footnotesize
-
-\begin{textblock}{13}(-0.3,2)
-\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
-def compile_expT(a: Exp, env: Mem, name: String): Instrs =
- ...
- case Call(n, args) => if (name == n)
- {
- val stores = args.zipWithIndex.map
- { case (x, y) => "istore " + y.toString + "\n" }
- args.flatMap(a => compile_expT(a, env, "")) ++
- stores.reverse ++
- List ("goto " + n + "_Start\n")
- }
- else
- {
- val is = "I" * args.length
- args.flatMap(a => compile_expT(a, env, "")) ++
- List ("invokestatic XXX/XXX/" + n + "(" + is + ")I\n")
- }
-\end{lstlisting}
-\end{textblock}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
@@ -674,11 +82,7 @@
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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -707,22 +111,534 @@
\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 (compiler, OS, \ldots).
+quite general (protocols, OS, \ldots).
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{\Large{}Mars Pathfinder Mission 1997}
+ \begin{center}
+ \includegraphics[scale=0.15]{../pics/marspath1.png}
+ \includegraphics[scale=0.16]{../pics/marspath3.png}
+ \includegraphics[scale=0.3]{../pics/marsrover.png}
+ \end{center}
+
+ \begin{itemize}
+ \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
+ \item a scheduling algorithm was not used in the OS
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+
+ \begin{textblock}{11}(1,3)
+ \begin{tabular}{@{\hspace{-10mm}}l}
+ \begin{tikzpicture}[scale=1.1]
+ \node at (-2.5,-1.5) {\textcolor{white}{a}};
+ \node at (8,4) {\textcolor{white}{a}};
+
+
+
+ \only<1>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ }
+ \only<2>{
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[fill, blue!50] (3,0) rectangle (5,0.6);
+ \draw[fill, blue!100] (2,3) rectangle (3,3.6);
+ }
+ \only<3>{
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
+ \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
+ \draw[fill, blue!100] (2,3) rectangle (3,3.6);
+ \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
+ }
+ \only<4>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
+ \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
+ \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
+ }
+ \only<5>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (4,0.6);
+ \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
+ }
+ \only<6>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
+ \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
+ \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
+ }
+ \only<7>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
+ \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
+ \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
+ }
+ \only<8>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
+ \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
+ \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
+ \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
+ \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
+ }
+ \only<9>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
+ \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
+ \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
+ \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
+ }
+ \only<10>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
+ \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
+ \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
+ \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
+ \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
+ }
+ \only<11>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
+ \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
+ \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
+ \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
+ \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
+ }
+ \only<12>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
+ \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
+ \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
+ \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
+ \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
+ \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
+ \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
+ \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
+ }
+ \only<13>{
+ \node at (2.5,0.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
+ \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
+ \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
+ }
+ \only<14>{
+ \node at (2.5,3.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[blue!50, fill] (2,3) rectangle (4,3.6);
+ \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
+ \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
+ \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
+ }
+ \only<15>{
+ \node at (2.5,3.9) {\small locked a resource};
+ \draw[fill, blue!50] (1,0) rectangle (2,0.6);
+ \draw[blue!50, fill] (2,3) rectangle (4,3.6);
+ \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
+ \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
+ \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1);
+ }
+
+
+ \draw[very thick,->](0,0) -- (8,0);
+ \node [anchor=base] at (8, -0.3) {\scriptsize time};
+ \node [anchor=base] at (0, -0.3) {\scriptsize 0};
+ \node [anchor=base] at (-1.2, 0.2) {\small low priority};
+ \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
+ \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
+
+ \end{tikzpicture}
+ \end{tabular}
+ \end{textblock}
+
+ \begin{textblock}{0}(2.5,13)%
+ \small
+ \onslide<3->{
+ \begin{bubble}[8cm]%
+ Scheduling: You want to avoid that a high
+ priority process is starved indefinitely.
+ \end{bubble}}
+ \end{textblock}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{\Large Priority Inheritance Scheduling}
+
+ \begin{itemize}
+ \item Let a low priority process $L$ temporarily inherit
+ the high priority of $H$ until $L$ leaves the critical
+ section unlocking the resource.\bigskip
+ \item Once the resource is unlocked $L$ returns to its original
+ priority level.
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+ \begin{textblock}{11}(1,3)
+ \begin{tabular}{@{\hspace{-10mm}}l}
+ \begin{tikzpicture}[scale=1.1]
+ \node at (-2.5,-1.5) {\textcolor{white}{a}};
+ \node at (8,4) {\textcolor{white}{a}};
+
+ \only<1>{
+ \draw[fill, blue!50] (1,0) rectangle (6,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,0.9) {\small $A_R$};
+ \node at (5.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
+ \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
+ }
+ \only<2>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,0.9) {\small $A_R$};
+ \node at (5.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
+ \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
+ }
+ \only<3>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,0.9) {\small $A_R$};
+ \node at (5.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
+ \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
+ \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
+ \node at (3.5,3.3) {\small $A$};
+ }
+ \only<4>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,0.9) {\small $A_R$};
+ \node at (5.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
+ \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
+ \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
+ \node at (3.5,3.3) {\small $A$};
+ \draw[very thick,blue!100] (4,3) rectangle (5,3.6);
+ \node at (4.5,3.3) {\small $B$};
+ }
+ \only<5>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[very thick, blue!50] (3,3) rectangle (6,3.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (5.7,3.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
+ \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
+ \node at (6.5,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
+ }
+ \only<6>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (5.7,3.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
+ \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
+ \node at (6.5,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ }
+ \only<7>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (5.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
+ \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
+ \node at (6.5,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
+ \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
+ }
+ \only<8>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (6.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
+ \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
+ \node at (4,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ }
+ \only<9>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
+ \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (6.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
+ \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
+ \node at (4,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ }
+ \only<10>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
+ \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (6.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
+ \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
+ \node at (4,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ \draw[red, fill] (5,1.5) rectangle (6,2.1);
+ \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
+ }
+ \only<11>{
+ \draw[fill, blue!50] (1,0) rectangle (3,0.6);
+ \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
+ \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
+ \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
+ \node at (1.5,0.9) {\small $A_L$};
+ \node at (2.0,0.9) {\small $B_L$};
+ \node at (3.5,3.9) {\small $A_R$};
+ \node at (6.7,0.9) {\small $B_R$};
+ \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
+ \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
+ \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
+ \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
+ \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
+ \node at (4,3.3) {\small $A$};
+ \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
+ \node at (7.5,3.3) {\small $B$};
+ \draw[red, fill] (5,1.5) rectangle (6,2.1);
+ \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
+ \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
+ \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
+ }
+
+ \draw[very thick,->](0,0) -- (8,0);
+ \node [anchor=base] at (8, -0.3) {\scriptsize time};
+ \node [anchor=base] at (0, -0.3) {\scriptsize 0};
+ \node [anchor=base] at (-1.2, 0.2) {\small low priority};
+ \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
+ \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}
+
+ \end{tikzpicture}
+ \end{tabular}
+ \end{textblock}
+
+ \begin{textblock}{0}(2.5,13)%
+ \small
+ \onslide<11>{
+ \begin{bubble}[8cm]%
+ Scheduling: You want to avoid that a high
+ priority process is staved indefinitely.
+ \end{bubble}}
+ \end{textblock}
+
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{\Large Priority Inheritance Scheduling}
+
+ \begin{itemize}
+ \item Let a low priority process $L$ temporarily inherit
+ the high priority of $H$ until $L$ leaves the critical
+ section unlocking the resource.\bigskip
+ \item Once the resource is unlocked $L$ returns to its original
+ priority level. \alert{\bf BOGUS}\pause\bigskip
+ \item \ldots $L$ needs to switch to the highest
+ \alert{remaining} priority of the threads that it blocks.
+ \end{itemize}\bigskip
+
+ \small this error is already known since around 1999
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+ \begin{center}
+ \includegraphics[scale=0.25]{../pics/p3.jpg}
+ \end{center}
+
+ \begin{itemize}
+ \item by Rajkumar, 1991
+ \item \it ``it resumes the priority it had at the point of entry into the critical
+ section''
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+ \begin{center}
+ \includegraphics[scale=0.25]{../pics/p2.jpg}
+ \end{center}
+
+ \begin{itemize}
+ \item by Jane Liu, 2000
+ \item {\it ``The job $J_l$ executes at its inherited
+ priority until it releases $R$; at that time, the
+ priority of $J_l$ returns to its priority
+ at the time when it acquires the resource $R$.''}\medskip
+ \item \small gives pseudo code and totally bogus data structures
+ \item \small interesting part ``{\it left as an exercise}''
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+ \begin{center}
+ \includegraphics[scale=0.15]{../pics/p1.pdf}
+ \end{center}
+
+ \begin{itemize}
+ \item by Laplante and Ovaska, 2011 (\$113.76)
+ \item \it ``when $[$the task$]$ exits the critical section that
+ caused the block, it reverts to the priority it had
+ when it entered that section''
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+
+ \begin{center}
+ \includegraphics[scale=0.25]{../pics/p4.jpg}
+ \end{center}
+
+ \begin{itemize}
+ \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)
+ \item \it ``Upon releasing the lock, the
+ $[$low-priority$]$ thread will revert to
+ its original priority.''
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{Priority Scheduling}
+
+ \begin{itemize}
+ \item a scheduling algorithm that is widely used in real-time operating systems
+ \item has been ``proved'' correct by hand in a paper in 1983
+ \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
+
+ \item we used the corrected algorithm and then {\bf really} proved
+ that it is correct
+
+ \item we implemented this algorithm in a small OS called PINTOS
+ (used for teaching at Stanford)
+
+ \item our implementation was much more efficient than their
+ reference implementation
+
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
-\frametitle{Can This Be Done?}
+\frametitle{Big Proofs in CS (1)}
+
+Formal proofs in CS sound like science fiction?
\begin{itemize}
-\item in 2008, verification of a small C-compiler
+\item in 2008, verification of a C-compiler
\begin{itemize}
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
-\item is as good as \texttt{gcc -O1}, but much, much less buggy
+\item is as good as \texttt{gcc -O1}, but much less buggy
\end{itemize}
\end{itemize}
@@ -734,31 +650,723 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \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{Fuzzy Testing C-Compilers}
+\frametitle{Big Proofs in CS (2)}
\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:
+\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
+ \begin{itemize}
+ \item used in helicopters and mobile phones
+ \item 200k loc of proof
+ \item 25 - 30 person years
+ \item found 160 bugs in the C code (144 by the proof)
+ \end{itemize}
+\end{itemize}
+
+\begin{bubble}[10cm]\small
+``Real-world operating-system kernel with an end-to-end proof
+of implementation correctness and security enforcement''
+\end{bubble}\bigskip\pause
+
+unhackable kernel (New Scientists, September 2015)
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Big Proofs in CS (3)}
+
+\begin{itemize}
+\item verified TLS implementation\medskip
+\item verified compilers (CompCert, CakeML)\medskip
+\item verified distributed systems (Verdi)\medskip
+\item verified OSes or OS components\\
+(seL4, CertiKOS, \ldots)\bigskip\pause
+\item Infer static analyser developed by Facebook
+\end{itemize}
+
+\end{frame}
-\begin{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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{How Did This Happen?}
+
+Lots of ways!
+
+\begin{itemize}
+\item better programming languages
+ \begin{itemize}
+ \item basic safety guarantees built in
\item powerful mechanisms for abstraction and modularity
+ \end{itemize}
+\item better software development methodology
+\item stable platforms and frameworks
+\item better use of specifications\medskip\\
+ \small If you want to build software that works or is secure,
+ it is helpful to know what you mean by ``works'' and by ``is secure''!
+\end{itemize}
+
+\end{frame}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Goal}
+
+Remember the Bridges example?
+
+\begin{itemize}
+\item Can we look at our programs and somehow ensure
+they are bug free/correct?\pause\bigskip
+
+\item Very hard: Anything interesting about programs is equivalent
+to the Halting Problem, which is undecidable.\pause\bigskip
+
+\item \alert{Solution:} We avoid this ``minor'' obstacle by
+ being as close as possible of deciding the halting
+ problem, without actually deciding the halting problem.
+ \small$\quad\Rightarrow$ yes, no, don't know (static analysis)
\end{itemize}
\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state.png}
+ \end{center}
+
+ \begin{itemize}
+ \item depending on some initial input, a program
+ (behaviour) will ``develop'' over time.
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state2.png}
+ \end{center}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state3.jpg}
+ \end{center}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state4.jpg}
+ \end{center}
+
+ \begin{itemize}
+ \item to be avoided
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state5.png}
+ \end{center}
+
+ \begin{itemize}
+ \item this needs more work
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{What is Static Analysis?}
+
+ \begin{center}
+ \includegraphics[scale=0.4]{../pics/state6.png}
+ \end{center}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c,fragile]
+ \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
+ Are Vars Definitely Initialised?\end{tabular}}
+
+Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip
+
+Prog.~1:\\
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language=While,xleftmargin=3mm]
+if x < 1 then y := x else y := x + 1;
+y := y + 1
+\end{lstlisting}\medskip
+
+Prog.~2:\\
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language=While,xleftmargin=3mm]
+if x < x then y := y + 1 else y := x;
+y := y + 1
+\end{lstlisting}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c,fragile]
+ \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
+ Are Vars Definitely Initialised?\end{tabular}}
+
+ What should the rules be for deciding when a
+ variable is initialised?\bigskip\pause
+
+\begin{itemize}
+\item variable \texttt{x} is definitely initialized after
+ \texttt{skip}\\
+ iff \texttt{x} is definitely initialized before \texttt{skip}.
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c,fragile]
+% \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
+% Are Vars Definitely Initialised?\end{tabular}}
+
+$\bl{A}$ is the set of definitely defined variables:
+
+\begin{center}
+\begin{tabular}{c}
+ \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad
+ \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}}
+ \medskip\\\pause
+
+ \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}}
+ \medskip\\\pause
+
+ \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2}
+ {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}}
+ \medskip\\\pause
+
+ \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'}
+ {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause
+\end{tabular}
+\end{center}
+
+\hfill we start with $\bl{A = \{\}}$
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{\large Concrete Example: Sign-Analysis}
+\mbox{}\\[-20mm]\mbox{}
+
+\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
+ | \meta{Exp} * \meta{Exp}
+ | \meta{Exp} = \meta{Exp}
+ | \meta{num}
+ | \meta{var}\\
+: \meta{Stmt} ::= \meta{label} :
+ | \meta{var} := \meta{Exp}
+ | \pcode{jmp?} \meta{Exp} \meta{label}
+ | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
+\end{plstx}}
+
+\begin{textblock}{0}(7.8,2.5)
+\small
+\begin{bubble}[5.6cm]
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language={},xleftmargin=3mm]
+ a := 1
+ n := 5
+top: jmp? n = 0 done
+ a := a * n
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{\large Concrete Example: Sign-Analysis}
+\mbox{}\\[-20mm]\mbox{}
+
+\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
+ | \meta{Exp} * \meta{Exp}
+ | \meta{Exp} = \meta{Exp}
+ | \meta{num}
+ | \meta{var}\\
+: \meta{Stmt} ::= \meta{label} :
+ | \meta{var} := \meta{Exp}
+ | \pcode{jmp?} \meta{Exp} \meta{label}
+ | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
+\end{plstx}}
+
+\begin{textblock}{0}(7.8,3.5)
+\small
+\begin{bubble}[5.6cm]
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language={},xleftmargin=3mm]
+ n := 6
+ m1 := 0
+ m2 := 1
+top: jmp? n = 0 done
+ tmp := m2
+ m2 := m1 + m2
+ m1 := tmp
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{\large Concrete Example: Sign-Analysis}
+\mbox{}\\[-20mm]\mbox{}
+
+\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
+ | \meta{Exp} * \meta{Exp}
+ | \meta{Exp} = \meta{Exp}
+ | \meta{num}
+ | \meta{var}\\
+: \meta{Stmt} ::= \meta{label} :
+ | \meta{var} := \meta{Exp}
+ | \pcode{jmp?} \meta{Exp} \meta{label}
+ | \pcode{goto} \meta{label}\\
+: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
+\end{plstx}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval: An Interpreter}
+\mbox{}\\[-14mm]\mbox{}
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[n]_{env}$ & $\dn$ & $n$\\
+$[x]_{env}$ & $\dn$ & $env(x)$\\
+$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\
+$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\
+$[e_1 = e_2]_{env}$ & $\dn$ &
+$\begin{cases}
+1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\
+0 & \text{otherwise}
+\end{cases}$\\
+\end{tabular}}
+\end{center}
+
+\footnotesize
+\begin{lstlisting}[numbers=none,xleftmargin=-5mm]
+def eval_exp(e: Exp, env: Env) : Int = e match {
+ case Num(n) => n
+ case Var(x) => env(x)
+ case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env)
+ case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env)
+ case Equ(e1, e2) =>
+ if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0
+}
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\small
+A program
+\begin{bubble}[6cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+ language={},
+ basicstyle=\ttfamily,
+ xleftmargin=1mm]
+ a := 1
+ n := 5
+top: jmp? n = 0 done
+ a := a * n
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+
+The \emph{snippets} of the program:
+
+\footnotesize
+\begin{columns}
+\begin{column}[t]{5cm}
+\begin{bubble}[4.5cm]
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language={},xleftmargin=1mm]
+"" a := 1
+ n := 5
+top: jmp? n = 0 done
+ a := a * n
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\begin{column}[t]{5cm}
+\begin{bubble}[4.5cm]
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language={},xleftmargin=1mm]
+top: jmp? n = 0 done
+ a := a * n
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\begin{column}[t]{2cm}
+\begin{bubble}[1.1cm]
+\begin{lstlisting}[numbers=none,
+ basicstyle=\ttfamily,
+ language={},xleftmargin=1mm]
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\end{columns}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval for Stmts}
+\mbox{}\\[-12mm]\mbox{}
+
+Let \bl{$sn$} be the snippets of a program
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\
+$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\
+$[x \,\texttt{:=}\, a::rest]_{env}$ & $\dn$ &
+$[rest]_{(env[x:= [a]_{env}])}$\medskip\\
+$[\texttt{jmp?}\;b\;l::rest]_{env}$ & $\dn$ &
+$\begin{cases}
+[sn(l)]_{env} & \text{if}\quad[b]_{env} = true\\
+[rest]_{env} & \text{otherwise}
+\end{cases}$\medskip\\
+$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\
+\end{tabular}}
+\end{center}\bigskip
+
+Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval in Code}
+
+\footnotesize
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
+def eval(sn: Snips) : Env = {
+ def eval_stmts(sts: Stmts, env: Env) : Env = sts match {
+ case Nil => env
+
+ case Label(l)::rest => eval_stmts(rest, env)
+
+ case Assign(x, e)::rest =>
+ eval_stmts(rest, env + (x -> eval_exp(e, env)))
+
+ case Jmp(b, l)::rest =>
+ if (eval_exp(b, env) == 1) eval_stmts(sn(l), env)
+ else eval_stmts(rest, env)
+
+ case Goto(l)::rest => eval_stmts(sn(l), env)
+ }
+
+ eval_stmts(sn(""), Map())
+}
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{The Idea of Static Analysis}
+\small
+\mbox{}\bigskip\\
+
+\begin{columns}
+\begin{column}{5cm}
+\begin{bubble}[4.5cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+ language={},
+ basicstyle=\ttfamily,
+ xleftmargin=1mm]
+ a := 1
+ n := 5
+top: jmp? n = 0 done
+ a := a * n
+ n := n + -1
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+
+\begin{column}{1cm}
+\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}
+\end{column}
+\begin{column}{6cm}
+\begin{bubble}[4.7cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+ language={},
+ basicstyle=\ttfamily,
+ xleftmargin=1mm,
+ escapeinside={(*}{*)}]
+ a := (*\hl{'+'}*)
+ n := (*\hl{'+'}*)
+top: jmp? n = (*\hl{'0'}*) done
+ a := a * n
+ n := n + (*\hl{'-'}*)
+ goto top
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\end{columns}\bigskip\bigskip
+
+Replace all constants and variables by either
+\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out
+is what the sign of \texttt{a} and \texttt{n} is (they should
+always positive).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{Sign Analysis?}
+
+
+ \begin{columns}
+ \begin{column}{3cm}
+ \begin{tabular}{cc|l}
+ $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{}
+ - & - & -\\
+ - & 0 & -\\
+ - & + & -, 0, +\\
+ 0 & $x$ & $x$\\
+ + & - & -, 0, +\\
+ + & 0 & +\\
+ + & + & +\\
+ \end{tabular}
+ \end{column}
+
+ \begin{column}{3cm}
+ \begin{tabular}{cc|l}
+ $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{}
+ - & - & +\\
+ - & 0 & 0\\
+ - & + & -\\
+ 0 & $x$ & 0\\
+ + & - & -\\
+ + & 0 & 0\\
+ + & + & +\\
+ \end{tabular}
+ \end{column}
+ \end{columns}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\mbox{}\\[-13mm]\mbox{}
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[n]_{aenv}$ & $\dn$ &
+$\begin{cases}
+\{+\} & \text{if}\; n > 0\\
+\{-\} & \text{if}\; n < 0\\
+\{0\} & \text{if}\; n = 0
+\end{cases}$\\
+$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\
+$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\
+$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\
+$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\
+\end{tabular}}
+\end{center}
+
+\scriptsize
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
+def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match {
+ case Num(0) => Set(Zero)
+ case Num(n) if (n < 0) => Set(Neg)
+ case Num(n) if (n > 0) => Set(Pos)
+ case Var(x) => aenv(x)
+ case Plus(e1, e2) =>
+ aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
+ case Times(e1, e2) =>
+ atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
+ case Equ(e1, e2) => Set(Zero, Pos)
+}
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{AEval for Stmts}
+\mbox{}\\[-12mm]\mbox{}
+
+Let \bl{$sn$} be the snippets of a program
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\
+$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\
+$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ &
+$(rest, aenv[x:= [e]_{aenv}])$\medskip\\
+$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ &
+$(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\
+$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\
+\end{tabular}}
+\end{center}\bigskip
+
+Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to
+reach all \emph{states} you can find (until a fix point is reached).
+
+Check whether there are only $aenv$ in the final states that have
+your property.
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{Sign Analysis}
+
+ \begin{itemize}
+ \item We want to find out whether \texttt{a} and \texttt{n}
+ are always positive?\medskip
+ \item After a few optimisations, we can indeed find this out.
+ \begin{itemize}
+ \item equal signs return only \texttt{+} or \texttt{0}
+ \item branch into only one direction if you know
+ \item if $x$ is \texttt{+}, then $x + \texttt{-1}$
+ cannot be negative
+ \end{itemize}\bigskip
+
+ \item What is this good for? Well, you do not need
+ underflow checks (in order to prevent buffer-overflow
+ attacks). In general this technique is used to make sure
+ keys stay secret.
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{Take Home Points}
+
+ \begin{itemize}
+ \item While testing is important, it does not show the
+ absence of bugs/vulnerabilities.\medskip
+ \item More and more we need (formal) proofs that show
+ a program is bug free.\medskip
+
+ \item Static analysis is more and more employed nowadays
+ in order to automatically hunt for bugs.
+ \end{itemize}
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
\end{document}
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides09.tex-bak Wed Nov 29 08:47:22 2017 +0000
@@ -0,0 +1,766 @@
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{../slides}
+\usepackage{../langs}
+\usepackage{../data}
+\usepackage{../graphics}
+\usepackage{../grammar}
+\usepackage{soul}
+
+\tikzset{onslide/.code args={<#1>#2}{%
+ \only<#1>{\pgfkeysalso{#2}} % \pgfkeysalso doesn't change the path
+}}
+
+\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{%b jm
+ \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
+
+\lstset{morekeywords={def,if,then,else,write,read},keywordstyle=\color{codepurple}\bfseries}
+
+% beamer stuff
+\renewcommand{\slidecaption}{CFL 09, King's College London}
+\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{%
+ \begin{tabular}{@ {}c@ {}}
+ \\[-3mm]
+ \LARGE Compilers and \\[-2mm]
+ \LARGE Formal Languages (8)\\[3mm]
+ \end{tabular}}
+
+ \normalsize
+ \begin{center}
+ \begin{tabular}{ll}
+ Email: & christian.urban at kcl.ac.uk\\
+ Office: & N7.07 (North Wing, Bush House)\\
+ Slides: & KEATS (also home work is there)\\
+ \end{tabular}
+ \end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,fragile]
+\frametitle{Compiling AExps}
+
+For example \bl{$1 + ((2 * 3) + (4 - 3))$}:\medskip
+
+\begin{columns}[T]
+\begin{column}{.3\textwidth}
+\begin{center}
+\bl{\begin{tikzpicture}
+\tikzset{level distance=12mm,sibling distance=4mm}
+\tikzset{edge from parent/.style={draw,very thick}}
\Tree [.$+$ [.$1$ ] [.$+$ [.$*$ $2$ $3$ ] [.$-$ $4$ $3$ ]]]
\end{tikzpicture}}
+\end{center}
+\end{column}
+\begin{column}{.3\textwidth}
+\begin{lstlisting}[language=JVMIS,numbers=none]
+ldc 1
+ldc 2
+ldc 3
+imul
+ldc 4
+ldc 3
+isub
+iadd
+iadd
+\end{lstlisting}
+\end{column}
+\end{columns}\bigskip
+
+\small
+Traverse tree in post-order \bl{$\Rightarrow$} code for
+stack-machine
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling AExps}
+
+\bl{
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{compile}(n, E)$ & $\dn$ & $\pcode{ldc}\;n$\smallskip\\
+$\textit{compile}(a_1 + a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\;\textit{compile}(a_2, E)\;@\; \pcode{iadd}$}\smallskip\\
+$\textit{compile}(a_1 - a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{isub}$}\smallskip\\
+$\textit{compile}(a_1 * a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{imul}$}\smallskip\\
+$\textit{compile}(a_1 \backslash a_2, E)$ & $\dn$\\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{idiv}$}\smallskip\\
+$\textit{compile}(x, E)$ & $\dn$ & $\pcode{iload}\;E(x)$\\
+\end{tabular}
+\end{center}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Ifs}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+if 1 = 1 then x := 2 else y := 3
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+ ldc 1
+ ldc 1
+ if_icmpne L_ifelse $\quad\tikz[remember picture] \node (C) {\mbox{}};$
+ ldc 2
+ istore 0
+ goto L_ifend $\quad\tikz[remember picture] \node (A) {\mbox{}};$
+L_ifelse: $\quad\tikz[remember picture] \node[] (D) {\mbox{}};$
+ ldc 3
+ istore 1
+L_ifend: $\quad\tikz[remember picture] \node[] (B) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
\draw[->,very thick] (A) edge [->,to path={-- ++(10mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (B.east);
+ \draw[->,very thick] (C) edge [->,to path={-- ++(10mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (D.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Whiles}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language=While]
+while x <= 10 do x := x + 1
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+L_wbegin: $\quad\tikz[remember picture] \node[] (LB) {\mbox{}};$
+ iload 0
+ ldc 10
+ if_icmpgt L_wend $\quad\tikz[remember picture] \node (LC) {\mbox{}};$
+ iload 0
+ ldc 1
+ iadd
+ istore 0
+ goto L_wbegin $\quad\tikz[remember picture] \node (LA) {\mbox{}};$
+L_wend: $\quad\tikz[remember picture] \node[] (LD) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
+ \draw[->,very thick] (LA) edge [->,to path={-- ++(12mm,0mm)
+ -- ++(0mm,17.3mm) |- (\tikztotarget)},line width=1mm] (LB.east);
+ \draw[->,very thick] (LC) edge [->,to path={-- ++(12mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (LD.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Writes}
+
+\small
+\begin{lstlisting}[language=JVMIS,mathescape,
+ numbers=none,xleftmargin=-6mm]
+.method public static write(I)V
+ .limit locals 1
+ .limit stack 2
+ getstatic java/lang/System/out
+ Ljava/io/PrintStream;
+ iload 0
+ invokevirtual java/io/PrintStream/println(I)V
+ return
+.end method
+
+
+
+iload $E(x)$
+invokestatic XXX/XXX/write(I)V
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Main}
+
+\footnotesize
+\begin{lstlisting}[language=JVMIS,mathescape,
+ numbers=none,xleftmargin=-6mm]
+.class public XXX.XXX
+.super java/lang/Object
+
+.method public <init>()V
+ aload_0
+ invokenonvirtual java/lang/Object/<init>()V
+ return
+.end method
+
+.method public static main([Ljava/lang/String;)V
+ .limit locals 200
+ .limit stack 200
+
+ $\textit{\ldots{}here comes the compiled code\ldots}$
+
+ return
+.end method
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Functional Programming}
+
+\footnotesize
+\begin{textblock}{13}(0.9,3)
+\begin{lstlisting}[]numbers=none]
+def fib(n) = if n == 0 then 0
+ else if n == 1 then 1
+ else fib(n - 1) + fib(n - 2);
+
+def fact(n) = if n == 0 then 1 else n * fact(n - 1);
+
+def ack(m, n) = if m == 0 then n + 1
+ else if n == 0 then ack(m - 1, 1)
+ else ack(m - 1, ack(m, n - 1));
+
+def gcd(a, b) = if b == 0 then a else gcd(b, a % b);
+\end{lstlisting}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Fun Grammar}
+\bl{
+\begin{plstx}[rhs style=]
+: \meta{Exp} ::= \meta{Var} | \meta{Num}{\hspace{3cm}}
+ | \meta{Exp} + \meta{Exp} | ... | (\meta{Exp})
+ | \code{if} \meta{BExp} \code{then} \meta{Exp} \code{else} \meta{Exp}
+ | \code{write} \meta{Exp} {\hspace{3cm}}
+ | \meta{Exp} ; \meta{Exp}
+ | \textit{FunName} (\meta{Exp}, ... , \meta{Exp})\\
+: \meta{BExp} ::= ...\\
+: \meta{Decl} ::= \meta{Def} ; \meta{Decl}
+ | \meta{Exp}\\
+: \meta{Def} ::= \code{def} \textit{FunName} ($\hspace{0.4mm}x_1$, ... , $x_n$) = \meta{Exp}\\
+\end{plstx}}
+
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Abstract Syntax Trees}
+
+\footnotesize
+\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]
+abstract class Exp
+abstract class BExp
+abstract class Decl
+
+case class Var(s: String) extends Exp
+case class Num(i: Int) extends Exp
+case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
+case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
+case class Write(e: Exp) extends Exp
+case class Sequ(e1: Exp, e2: Exp) extends Exp
+case class Call(name: String, args: List[Exp]) extends Exp
+
+case class Bop(o: String, a1: Exp, a2: Exp) extends BExp
+
+case class Def(name: String,
+ args: List[String],
+ body: Exp) extends Decl
+case class Main(e: Exp) extends Decl
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Sequences}
+
+Compiling \texttt{exp1 ; exp2}:\bigskip
+
+
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(exp1)
+pop
+$\textit{compile}$(exp2)
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Write}
+
+Compiling call to \texttt{write(1+2)}:\bigskip
+
+
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(1+2)
+dup
+invokestatic XXX/XXX/write(I)V
+\end{lstlisting}\bigskip
+
+\small
+needs the helper method
+
+\footnotesize
+\begin{lstlisting}[language=JVMIS,
+ xleftmargin=2mm,
+ numbers=none]
+.method public static write(I)V
+ .limit locals 1
+ .limit stack 2
+ getstatic java/lang/System/out Ljava/io/PrintStream;
+ iload 0
+ invokevirtual java/io/PrintStream/println(I)V
+ return
+.end method
+\end{lstlisting}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t, fragile]
+\frametitle{Function Definitions}
+
+\footnotesize
+\begin{lstlisting}[language=JVMIS,
+ xleftmargin=2mm,
+ numbers=none]
+.method public static write(I)V
+ .limit locals 1
+ .limit stack 2
+ getstatic java/lang/System/out Ljava/io/PrintStream;
+ iload 0
+ invokevirtual java/io/PrintStream/println(I)V
+ return
+.end method
+\end{lstlisting}\bigskip
+
+\small We will need for definitions, like\footnotesize\medskip
+
+\begin{lstlisting}[language=JVMIS,
+ xleftmargin=2mm,
+ numbers=none]
+def fname (x1, ... , xn) = ...
+
+.method public static fname (I...I)I
+ .limit locals ??
+ .limit stack ??
+ ??
+.end method
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Stack Estimation}
+\small
+\mbox{}\\[-15mm]
+
+\bl{\begin{center}
+\begin{tabular}{@{\hspace{-4mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
+$\textit{estimate}(n)$ & $\dn$ & $1$\\
+$\textit{estimate}(x)$ & $\dn$ & $1$\\
+$\textit{estimate}(a_1\;aop\;a_2)$ & $\dn$ &
+$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
+$\textit{estimate}(\pcode{if}\;b\;\pcode{then}\;e_1\;\pcode{else}\;e_2)$ & $\dn$ &
+$\textit{estimate}(b) +$\\
+& & $\quad max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
+$\textit{estimate}(\pcode{write}(e))$ & $\dn$ &
+$\textit{estimate}(e) + 1$\\
+$\textit{estimate}(e_1 ; e_2)$ & $\dn$ &
+$max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
+$\textit{estimate}(f(e_1, ..., e_n))$ & $\dn$ &
+$\sum_{i = 1..n}\;estimate(e_i)$\medskip\\
+$\textit{estimate}(a_1\;bop\;a_2)$ & $\dn$ &
+$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
+\end{tabular}
+\end{center}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Successor Function}
+
+\begin{textblock}{7}(1,2.5)\footnotesize
+\begin{minipage}{6cm}
+\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
+.method public static suc(I)I
+.limit locals 1
+.limit stack 2
+ iload 0
+ ldc 1
+ iadd
+ ireturn
+.end method
+\end{lstlisting}
+\end{minipage}
+\end{textblock}
+
+\begin{textblock}{7}(6,8)
+\begin{bubble}[5cm]\small
+\begin{lstlisting}[language=Lisp,
+ basicstyle=\ttfamily,
+ numbers=none,
+ xleftmargin=1mm]
+def suc(x) = x + 1;
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Addition Function}
+
+\begin{textblock}{7}(1,1.9)\footnotesize
+\begin{minipage}{6cm}
+\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
+.method public static add(II)I
+.limit locals 2
+.limit stack 5
+ iload 0
+ ldc 0
+ if_icmpne If_else
+ iload 1
+ goto If_end
+If_else:
+ iload 0
+ ldc 1
+ isub
+ iload 1
+ invokestatic XXX/XXX/add(II)I
+ invokestatic XXX/XXX/suc(I)I
+If_end:
+ ireturn
+.end method
+\end{lstlisting}
+\end{minipage}
+\end{textblock}
+
+\begin{textblock}{7}(6,6.6)
+\begin{bubble}[7cm]\small
+\begin{lstlisting}[language=Lisp,
+ basicstyle=\ttfamily,
+ numbers=none,
+ xleftmargin=1mm]
+def add(x, y) =
+ if x == 0 then y
+ else suc(add(x - 1, y));
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Factorial}
+
+\begin{textblock}{7}(1,1.5)\footnotesize
+\begin{minipage}{6cm}
+\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
+.method public static facT(II)I
+.limit locals 2
+.limit stack 6
+ iload 0
+ ldc 0
+ if_icmpne If_else_2
+ iload 1
+ goto If_end_3
+If_else_2:
+ iload 0
+ ldc 1
+ isub
+ iload 0
+ iload 1
+ imul
+ invokestatic fact/fact/facT(II)I
+If_end_3:
+ ireturn
+.end method
+\end{lstlisting}
+\end{minipage}
+\end{textblock}
+
+\begin{textblock}{7}(6,7)
+\begin{bubble}[7cm]\small
+\begin{lstlisting}[language=Lisp,
+ basicstyle=\ttfamily,
+ numbers=none,
+ xleftmargin=1mm]
+def facT(n, acc) =
+ if n == 0 then acc
+ else facT(n - 1, n * acc);
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+
+\begin{textblock}{7}(1,-0.2)\footnotesize
+\begin{minipage}{6cm}
+\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
+.method public static facT(II)I
+.limit locals 2
+.limit stack 6
+(*@\hl{facT\_Start:} @*)
+ iload 0
+ ldc 0
+ if_icmpne If_else_2
+ iload 1
+ goto If_end_3
+If_else_2:
+ iload 0
+ ldc 1
+ isub
+ iload 0
+ iload 1
+ imul
+ (*@\hl{istore 1} @*)
+ (*@\hl{istore 0} @*)
+ (*@\hl{goto facT\_Start} @*)
+If_end_3:
+ ireturn
+.end method
+\end{lstlisting}
+\end{minipage}
+\end{textblock}
+
+\begin{textblock}{7}(6,7)
+\begin{bubble}[7cm]\small
+\begin{lstlisting}[language=Lisp,
+ basicstyle=\ttfamily,
+ numbers=none,
+ xleftmargin=1mm]
+def facT(n, acc) =
+ if n == 0 then acc
+ else facT(n - 1, n * acc);
+\end{lstlisting}
+\end{bubble}
+\end{textblock}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Tail Recursion}
+
+A call to \texttt{f(args)} is usually compiled as\medskip
+
+{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
+ args onto stack
+ invokestatic .../f
+\end{lstlisting}}\pause
+
+
+A call is in tail position provided:\medskip
+
+{\small\begin{itemize}
+\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
+\item \texttt{Exp ; \hl{Exp}}
+\item \texttt{Exp op Exp}
+\end{itemize}}\medskip
+
+then a call \texttt{f(args)} can be compiled as\medskip\small
+
+\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
+ prepare environment
+ jump to start of function
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c, fragile]
+\frametitle{Tail Recursive Call}
+\footnotesize
+
+\begin{textblock}{13}(-0.3,2)
+\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
+def compile_expT(a: Exp, env: Mem, name: String): Instrs =
+ ...
+ case Call(n, args) => if (name == n)
+ {
+ val stores = args.zipWithIndex.map
+ { case (x, y) => "istore " + y.toString + "\n" }
+ args.flatMap(a => compile_expT(a, env, "")) ++
+ stores.reverse ++
+ List ("goto " + n + "_Start\n")
+ }
+ else
+ {
+ val is = "I" * args.length
+ args.flatMap(a => compile_expT(a, env, "")) ++
+ List ("invokestatic XXX/XXX/" + n + "(" + is + ")I\n")
+ }
+\end{lstlisting}
+\end{textblock}
+
+\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
+
+ \small
+ What is good about compilers: the either seem to work,
+ or go horribly wrong (most of the time).
+
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{\Large Proving Programs to be Correct}
+
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} There are infinitely many prime
+numbers.\medskip\\
+
+{\bf Proof} \ldots\\
+\end{bubble}\bigskip
+
+
+similarly\bigskip
+
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} The program is doing what
+it is supposed to be doing.\medskip
+
+{\bf Long, long proof} \ldots\\
+\end{bubble}\bigskip\medskip
+
+\small This can be a gigantic proof. The only hope is to have
+help from the computer. `Program' is here to be understood to be
+quite general (compiler, OS, \ldots).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{frame}[c]
+\frametitle{Can This Be Done?}
+
+\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, much less buggy
+\end{itemize}
+\end{itemize}
+
+\begin{center}
+ \includegraphics[scale=0.12]{../pics/compcert.png}
+\end{center}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Fuzzy Testing C-Compilers}
+
+\begin{itemize}
+\item tested GCC, LLVM and others by randomly generating
+C-programs
+\item found more than 300 bugs in GCC and also
+many in LLVM (some of them highest-level critical)\bigskip
+\item about CompCert:
+
+\begin{bubble}[10cm]\small ``The striking thing about our CompCert
+results is that the middle-end bugs we found in all other
+compilers are absent. As of early 2011, the under-development
+version of CompCert is the only compiler we have tested for
+which Csmith cannot find wrong-code errors. This is not for
+lack of trying: we have devoted about six CPU-years to the
+task.''
+\end{bubble}
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+