# HG changeset patch # User Christian Urban # Date 1511945242 0 # Node ID 17acdd516ccdb89aa0191823432779aa188f4a2d # Parent feb8a2a426253e8cee61b1284f5c42c7e039a50d updated diff -r feb8a2a42625 -r 17acdd516ccd progs/catastrophic2.py --- a/progs/catastrophic2.py Wed Nov 22 18:27:59 2017 +0000 +++ b/progs/catastrophic2.py Wed Nov 29 08:47:22 2017 +0000 @@ -15,6 +15,7 @@ cn = sys.argv[1] # calling the matching function -m = re.match('(a*)*b' , "a" * int(cn)) +s = ("a" * int(cn)) +m = re.match('(a*)*b' , s) -print m.group(0) +print s diff -r feb8a2a42625 -r 17acdd516ccd slides/slides09.pdf Binary file slides/slides09.pdf has changed diff -r feb8a2a42625 -r 17acdd516ccd slides/slides09.tex --- 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 ()V - aload_0 - invokenonvirtual java/lang/Object/()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 diff -r feb8a2a42625 -r 17acdd516ccd slides/slides09.tex-bak --- /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 ()V + aload_0 + invokenonvirtual java/lang/Object/()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: +