# HG changeset patch # User Christian Urban # Date 1543279526 0 # Node ID e33545bb2eba08c84e90599d1b7ac6e1405e2b8c # Parent 3db4970ad0aa87b2d5c859d0d1dbec9cb8c07e74 updated diff -r 3db4970ad0aa -r e33545bb2eba coursework/cw03.pdf Binary file coursework/cw03.pdf has changed diff -r 3db4970ad0aa -r e33545bb2eba progs/compile.scala --- a/progs/compile.scala Tue Nov 20 13:37:40 2018 +0000 +++ b/progs/compile.scala Tue Nov 27 00:45:26 2018 +0000 @@ -196,25 +196,9 @@ } -// Fibonacci numbers as a test-case -val fib_test = - List(Read("n"), // read n; - Assign("minus1",Num(0)), // minus1 := 0; - Assign("minus2",Num(1)), // minus2 := 1; - Assign("temp",Num(0)), // temp := 0; - While(Bop("<",Num(0),Var("n")), // while n > 0 do { - List(Assign("temp",Var("minus2")), // temp := minus2; - Assign("minus2",Aop("+",Var("minus1"),Var("minus2"))), - // minus2 := minus1 + minus2; - Assign("minus1",Var("temp")), // minus1 := temp; - Assign("n",Aop("-",Var("n"),Num(1))))), // n := n - 1 }; - Write("minus1")) // write minus1 - -// prints out the JVM-assembly program - -println(compile(fib_test, "fib")) - -// can be assembled with +// compiling and running files +// +// JVM files can be assembled with // // java -jar jvm/jasmin-2.4/jasmin.jar fib.j // @@ -222,6 +206,8 @@ // // java fib/fib + + import scala.util._ import scala.sys.process._ import scala.io @@ -240,6 +226,36 @@ println("assembled ") } +def time_needed[T](i: Int, code: => T) = { + val start = System.nanoTime() + for (j <- 1 to i) code + val end = System.nanoTime() + (end - start)/(i * 1.0e9) +} -compile_all(fib_test, "fib") + +def compile_run(bl: Block, class_name: String) : Unit = { + println("Start compilation") + compile_all(bl, class_name) + println("Time: " + time_needed(1, ("java " + class_name + "/" + class_name).!)) +} + +// Fibonacci numbers as a test-case +val fib_test = + List(Assign("n", Num(10)), // n := 10; + Assign("minus1",Num(0)), // minus1 := 0; + Assign("minus2",Num(1)), // minus2 := 1; + Assign("temp",Num(0)), // temp := 0; + While(Bop("<",Num(0),Var("n")), // while n > 0 do { + List(Assign("temp",Var("minus2")), // temp := minus2; + Assign("minus2",Aop("+",Var("minus1"),Var("minus2"))), + // minus2 := minus1 + minus2; + Assign("minus1",Var("temp")), // minus1 := temp; + Assign("n",Aop("-",Var("n"),Num(1))))), // n := n - 1 }; + Write("minus1")) // write minus1 + + +compile_run(fib_test, "fib") + + diff -r 3db4970ad0aa -r e33545bb2eba progs/compile_arr.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/progs/compile_arr.scala Tue Nov 27 00:45:26 2018 +0000 @@ -0,0 +1,261 @@ +// A Small Compiler for the WHILE Language +// (it does not use a parser and lexer) + +// the abstract syntax trees +abstract class Stmt +abstract class AExp +abstract class BExp +type Block = List[Stmt] + +// statements +case object Skip extends Stmt +case class If(a: BExp, bl1: Block, bl2: Block) extends Stmt +case class While(b: BExp, bl: Block) extends Stmt +case class Assign(s: String, a: AExp) extends Stmt +case class Write(s: String) extends Stmt +case class Read(s: String) extends Stmt + +// arithmetic expressions +case class Var(s: String) extends AExp +case class Num(i: Int) extends AExp +case class Aop(o: String, a1: AExp, a2: AExp) extends AExp + +// boolean expressions +case object True extends BExp +case object False extends BExp +case class Bop(o: String, a1: AExp, a2: AExp) extends BExp + + +// compiler headers needed for the JVM +// (contains an init method, as well as methods for read and write) +val beginning = """ +.class public XXX.XXX +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.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 + +.method public static read()I + .limit locals 10 + .limit stack 10 + + ldc 0 + istore 1 ; this will hold our final integer +Label1: + getstatic java/lang/System/in Ljava/io/InputStream; + invokevirtual java/io/InputStream/read()I + istore 2 + iload 2 + ldc 10 ; the newline delimiter + isub + ifeq Label2 + iload 2 + ldc 32 ; the space delimiter + isub + ifeq Label2 + + iload 2 + ldc 48 ; we have our digit in ASCII, have to subtract it from 48 + isub + ldc 10 + iload 1 + imul + iadd + istore 1 + goto Label1 +Label2: + ;when we come here we have our integer computed in local variable 1 + iload 1 + ireturn +.end method + +.method public static main([Ljava/lang/String;)V + .limit locals 200 + .limit stack 200 + +""" + +val ending = """ + + return + +.end method +""" + +println("Start compilation") + + +// for generating new labels +var counter = -1 + +def Fresh(x: String) = { + counter += 1 + x ++ "_" ++ counter.toString() +} + +// environments and instructions +type Env = Map[String, String] +type Instrs = List[String] + +// arithmetic expression compilation +def compile_aexp(a: AExp, env : Env) : Instrs = a match { + case Num(i) => List("ldc " + i.toString + "\n") + case Var(s) => List("iload " + env(s) + "\n") + case Aop("+", a1, a2) => + compile_aexp(a1, env) ++ + compile_aexp(a2, env) ++ List("iadd\n") + case Aop("-", a1, a2) => + compile_aexp(a1, env) ++ compile_aexp(a2, env) ++ List("isub\n") + case Aop("*", a1, a2) => + compile_aexp(a1, env) ++ compile_aexp(a2, env) ++ List("imul\n") +} + +// boolean expression compilation +def compile_bexp(b: BExp, env : Env, jmp: String) : Instrs = b match { + case True => Nil + case False => List("goto " + jmp + "\n") + case Bop("=", a1, a2) => + compile_aexp(a1, env) ++ compile_aexp(a2, env) ++ + List("if_icmpne " + jmp + "\n") + case Bop("!=", a1, a2) => + compile_aexp(a1, env) ++ compile_aexp(a2, env) ++ + List("if_icmpeq " + jmp + "\n") + case Bop("<", a1, a2) => + compile_aexp(a1, env) ++ compile_aexp(a2, env) ++ + List("if_icmpge " + jmp + "\n") +} + +// statement compilation +def compile_stmt(s: Stmt, env: Env) : (Instrs, Env) = s match { + case Skip => (Nil, env) + case Assign(x, a) => { + val index = if (env.isDefinedAt(x)) env(x) else + env.keys.size.toString + (compile_aexp(a, env) ++ + List("istore " + index + "\n"), env + (x -> index)) + } + case If(b, bl1, bl2) => { + val if_else = Fresh("If_else") + val if_end = Fresh("If_end") + val (instrs1, env1) = compile_block(bl1, env) + val (instrs2, env2) = compile_block(bl2, env1) + (compile_bexp(b, env, if_else) ++ + instrs1 ++ + List("goto " + if_end + "\n") ++ + List("\n" + if_else + ":\n\n") ++ + instrs2 ++ + List("\n" + if_end + ":\n\n"), env2) + } + case While(b, bl) => { + val loop_begin = Fresh("Loop_begin") + val loop_end = Fresh("Loop_end") + val (instrs1, env1) = compile_block(bl, env) + (List("\n" + loop_begin + ":\n\n") ++ + compile_bexp(b, env, loop_end) ++ + instrs1 ++ + List("goto " + loop_begin + "\n") ++ + List("\n" + loop_end + ":\n\n"), env1) + } + case Write(x) => + (List("iload " + env(x) + "\n" + + "invokestatic XXX/XXX/write(I)V\n"), env) + case Read(x) => { + val index = if (env.isDefinedAt(x)) env(x) else + env.keys.size.toString + (List("invokestatic XXX/XXX/read()I\n" + + "istore " + index + "\n"), env + (x -> index)) + } +} + +// compilation of a block (i.e. list of instructions) +def compile_block(bl: Block, env: Env) : (Instrs, Env) = bl match { + case Nil => (Nil, env) + case s::bl => { + val (instrs1, env1) = compile_stmt(s, env) + val (instrs2, env2) = compile_block(bl, env1) + (instrs1 ++ instrs2, env2) + } +} + +// main compilation function for blocks +def compile(bl: Block, class_name: String) : String = { + val instructions = compile_block(bl, Map.empty)._1 + (beginning ++ instructions.mkString ++ ending).replaceAllLiterally("XXX", class_name) +} + + +// compiling and running files +// +// JVM files can be assembled with +// +// java -jar jvm/jasmin-2.4/jasmin.jar fib.j +// +// and started with +// +// java fib/fib + + + +import scala.util._ +import scala.sys.process._ +import scala.io + +def compile_tofile(bl: Block, class_name: String) = { + val output = compile(bl, class_name) + val fw = new java.io.FileWriter(class_name + ".j") + fw.write(output) + fw.close() +} + +def compile_all(bl: Block, class_name: String) : Unit = { + compile_tofile(bl, class_name) + println("compiled ") + val test = ("java -jar jvm/jasmin-2.4/jasmin.jar " + class_name + ".j").!! + println("assembled ") +} + +def time_needed[T](i: Int, code: => T) = { + val start = System.nanoTime() + for (j <- 1 to i) code + val end = System.nanoTime() + (end - start)/(i * 1.0e9) +} + + +def compile_run(bl: Block, class_name: String) : Unit = { + println("Start compilation") + compile_all(bl, class_name) + println("Time: " + time_needed(1, ("java " + class_name + "/" + class_name).!)) +} + + +// Fibonacci numbers as a test-case +val fib_test = + List(Assign("n", Num(10)), // n := 10; + Assign("minus1",Num(0)), // minus1 := 0; + Assign("minus2",Num(1)), // minus2 := 1; + Assign("temp",Num(0)), // temp := 0; + While(Bop("<",Num(0),Var("n")), // while n > 0 do { + List(Assign("temp",Var("minus2")), // temp := minus2; + Assign("minus2",Aop("+",Var("minus1"),Var("minus2"))), + // minus2 := minus1 + minus2; + Assign("minus1",Var("temp")), // minus1 := temp; + Assign("n",Aop("-",Var("n"),Num(1))))), // n := n - 1 }; + Write("minus1")) // write minus1 + + +compile_run(fib_test, "fib") + + diff -r 3db4970ad0aa -r e33545bb2eba progs/fib.j --- a/progs/fib.j Tue Nov 20 13:37:40 2018 +0000 +++ b/progs/fib.j Tue Nov 27 00:45:26 2018 +0000 @@ -55,7 +55,7 @@ .limit locals 200 .limit stack 200 -invokestatic fib/fib/read()I +ldc 10 istore 0 ldc 0 istore 1 @@ -64,11 +64,11 @@ ldc 0 istore 3 -Loop_begin_2: +Loop_begin_0: ldc 0 iload 0 -if_icmpge Loop_end_3 +if_icmpge Loop_end_1 iload 2 istore 3 iload 1 @@ -81,9 +81,9 @@ ldc 1 isub istore 0 -goto Loop_begin_2 +goto Loop_begin_0 -Loop_end_3: +Loop_end_1: iload 1 invokestatic fib/fib/write(I)V diff -r 3db4970ad0aa -r e33545bb2eba progs/funt.scala --- a/progs/funt.scala Tue Nov 20 13:37:40 2018 +0000 +++ b/progs/funt.scala Tue Nov 27 00:45:26 2018 +0000 @@ -492,6 +492,7 @@ // a problem with the parser +/* val text = "(((((1)))))" val tokens = tokenizer(text) println(tokens) @@ -506,3 +507,4 @@ val tokens = tokenizer(text) println(tokens) Exp.parse(tokens) +*/ diff -r 3db4970ad0aa -r e33545bb2eba slides/slides07.pdf Binary file slides/slides07.pdf has changed diff -r 3db4970ad0aa -r e33545bb2eba slides/slides08.pdf Binary file slides/slides08.pdf has changed diff -r 3db4970ad0aa -r e33545bb2eba slides/slides09.pdf Binary file slides/slides09.pdf has changed diff -r 3db4970ad0aa -r e33545bb2eba slides/slides09.tex --- a/slides/slides09.tex Tue Nov 20 13:37:40 2018 +0000 +++ b/slides/slides09.tex Tue Nov 27 00:45:26 2018 +0000 @@ -1,16 +1,19 @@ \documentclass[dvipsnames,14pt,t]{beamer} \usepackage{../slides} \usepackage{../langs} +\usepackage{../data} \usepackage{../graphics} \usepackage{../grammar} \usepackage{soul} -\usepackage{mathpartir} + -% beamer stuff +% beamer stuff \renewcommand{\slidecaption}{CFL 09, King's College London} -\newcommand{\bl}[1]{\textcolor{blue}{#1}} +\newcommand{\bl}[1]{\textcolor{blue}{#1}} + \begin{document} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[t] \frametitle{% @@ -24,53 +27,137 @@ \begin{center} \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ - Office: & N7.07 (North Wing, Bush House)\\ - Slides: & KEATS (also home work is there)\\ - \end{tabular} - \end{center} -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{center} - \includegraphics[scale=0.6]{../pics/bridge-limits.png} - \end{center} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{Old-Fashioned Eng.~vs.~CS} - - \begin{center} - \begin{tabular}{@{}cc@{}} - \begin{tabular}{@{}p{5.2cm}} - \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ - {\bf bridges}: \\ - \raggedright\small - engineers can ``look'' at a bridge and have a pretty good - intuition about whether it will hold up or not\\ - (redundancy; predictive theory) - \end{tabular} & - \begin{tabular}{p{5cm}} - \includegraphics[scale=0.265]{../pics/code.jpg}\\ - \raggedright - {\bf code}: \\ - \raggedright\small - programmers have very little intuition about their code; - often it is too expensive to have redundancy; - not ``continuous'' - \end{tabular} + Office: & N\liningnums{7.07} (North Wing, Bush House)\\ + Slides: & KEATS (also homework is there)\\ \end{tabular} \end{center} - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[t] +\frametitle{While Language} + +\begin{center} +\bl{\begin{tabular}{@{}lcl@{}} +\\[-12mm] +\meta{Stmt} & $::=$ & $\texttt{skip}$\\ + & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\ + & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\ + & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\ + & $|$ & \texttt{read}\;\textit{Id}\\ + & $|$ & \texttt{write}\;\textit{Id}\\ + & $|$ & \texttt{write}\;\textit{String}\medskip\\ +\meta{Stmts} & $::=$ & \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$ \meta{Stmt}\medskip\\ +\meta{Block} & $::=$ & \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\ +\meta{AExp} & $::=$ & \ldots\\ +\meta{BExp} & $::=$ & \ldots\\ +\end{tabular}} +\end{center} +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c] +\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}} + +\mbox{}\\[-18mm]\mbox{} + +{\lstset{language=While}\fontsize{10}{12}\selectfont +\texttt{\lstinputlisting{../progs/fib.while}}} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{BF***} + +some big array, say \texttt{a}; 7 (8) instructions: + +\begin{itemize} +\item \texttt{>} move \texttt{ptr++} +\item \texttt{<} move \texttt{ptr-{}-} +\item \texttt{+} add \texttt{a[ptr]++} +\item \texttt{-} subtract \texttt{a[ptr]-{}-} +\item \texttt{.} print out \texttt{a[ptr]} as ASCII +\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++} +\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++} + +\end{itemize} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{Arrays in While} +\begin{itemize} +\item \texttt{new arr[15000]}\medskip +\item \texttt{x := 3 + arr[3 + y]}\medskip +\item \texttt{arr[42 * n] := ...} +\end{itemize} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{New Arrays} + +\begin{lstlisting}[mathescape,numbers=none,language=While] + new arr[number] +\end{lstlisting}\bigskip\bigskip + +\begin{lstlisting}[mathescape,numbers=none,language=While] + ldc number + newarray int + astore loc_var +\end{lstlisting} + + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{Array Update} + +\begin{lstlisting}[mathescape,numbers=none,language=While] + arr[...] := +\end{lstlisting}\bigskip\bigskip + +\begin{lstlisting}[mathescape,numbers=none,language=While] + aload loc_var + index_aexp + value_aexp + iastore +\end{lstlisting} + + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{Array Lookup in AExp} + +\begin{lstlisting}[mathescape,numbers=none,language=While] + ...arr[...]... +\end{lstlisting}\bigskip\bigskip + +\begin{lstlisting}[mathescape,numbers=none,language=While] + aload loc_var + index_aexp + iaload +\end{lstlisting} + + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -82,7 +169,11 @@ presence of bugs, but it is hopelessly inadequate for showing their absence.'' \end{bubble}\bigskip - + + \small + What is good about compilers: the either seem to work, + or go horribly wrong (most of the time). + \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -111,534 +202,22 @@ \small This can be a gigantic proof. The only hope is to have help from the computer. `Program' is here to be understood to be -quite general (protocols, OS, \ldots). +quite general (compiler, OS, \ldots). \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{\Large{}Mars Pathfinder Mission 1997} - \begin{center} - \includegraphics[scale=0.15]{../pics/marspath1.png} - \includegraphics[scale=0.16]{../pics/marspath3.png} - \includegraphics[scale=0.3]{../pics/marsrover.png} - \end{center} - - \begin{itemize} - \item despite NASA's famous testing procedures, the lander crashed frequently on Mars - \item a scheduling algorithm was not used in the OS - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - - \begin{textblock}{11}(1,3) - \begin{tabular}{@{\hspace{-10mm}}l} - \begin{tikzpicture}[scale=1.1] - \node at (-2.5,-1.5) {\textcolor{white}{a}}; - \node at (8,4) {\textcolor{white}{a}}; - - - - \only<1>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - } - \only<2>{ - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[fill, blue!50] (3,0) rectangle (5,0.6); - \draw[fill, blue!100] (2,3) rectangle (3,3.6); - } - \only<3>{ - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[fill, blue!50] (3,0) rectangle (4.5,0.6); - \draw[fill, blue!50] (5.5,0) rectangle (6,0.6); - \draw[fill, blue!100] (2,3) rectangle (3,3.6); - \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6); - } - \only<4>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[blue!50, very thick] (2,0) rectangle (4,0.6); - \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); - \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); - } - \only<5>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (4,0.6); - \draw[blue!100, fill] (4,3) rectangle (5, 3.6); - } - \only<6>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[blue!50, very thick] (2,0) rectangle (4,0.6); - \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); - \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); - } - \only<7>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); - \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); - \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); - } - \only<8>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6); - \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); - \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6); - \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); - \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); - } - \only<9>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); - \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); - \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); - \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); - } - \only<10>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6); - \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6); - \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); - \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); - \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1); - } - \only<11>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6); - \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6); - \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); - \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); - \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1); - } - \only<12>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2.5,0.6); - \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6); - \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6); - \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1); - \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1); - \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1); - \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1); - \node [anchor=base] at (6.3, 1.8) {\Large\ldots}; - } - \only<13>{ - \node at (2.5,0.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[blue!50, very thick] (2,0) rectangle (4,0.6); - \draw[blue!100, very thick] (2,3) rectangle (3, 3.6); - \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); - } - \only<14>{ - \node at (2.5,3.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[blue!50, fill] (2,3) rectangle (4,3.6); - \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); - \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5); - \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1); - } - \only<15>{ - \node at (2.5,3.9) {\small locked a resource}; - \draw[fill, blue!50] (1,0) rectangle (2,0.6); - \draw[blue!50, fill] (2,3) rectangle (4,3.6); - \draw[blue!100, very thick] (4,3) rectangle (5, 3.6); - \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1); - \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); - } - - - \draw[very thick,->](0,0) -- (8,0); - \node [anchor=base] at (8, -0.3) {\scriptsize time}; - \node [anchor=base] at (0, -0.3) {\scriptsize 0}; - \node [anchor=base] at (-1.2, 0.2) {\small low priority}; - \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} - \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} - - \end{tikzpicture} - \end{tabular} - \end{textblock} - - \begin{textblock}{0}(2.5,13)% - \small - \onslide<3->{ - \begin{bubble}[8cm]% - Scheduling: You want to avoid that a high - priority process is starved indefinitely. - \end{bubble}} - \end{textblock} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{\Large Priority Inheritance Scheduling} - - \begin{itemize} - \item Let a low priority process $L$ temporarily inherit - the high priority of $H$ until $L$ leaves the critical - section unlocking the resource.\bigskip - \item Once the resource is unlocked $L$ returns to its original - priority level. - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{textblock}{11}(1,3) - \begin{tabular}{@{\hspace{-10mm}}l} - \begin{tikzpicture}[scale=1.1] - \node at (-2.5,-1.5) {\textcolor{white}{a}}; - \node at (8,4) {\textcolor{white}{a}}; - - \only<1>{ - \draw[fill, blue!50] (1,0) rectangle (6,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,0.9) {\small $A_R$}; - \node at (5.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); - \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); - } - \only<2>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[very thick, blue!50] (3,0) rectangle (6,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,0.9) {\small $A_R$}; - \node at (5.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); - \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); - } - \only<3>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[very thick, blue!50] (3,0) rectangle (6,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,0.9) {\small $A_R$}; - \node at (5.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); - \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); - \draw[very thick,blue!100] (3,3) rectangle (4,3.6); - \node at (3.5,3.3) {\small $A$}; - } - \only<4>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[very thick, blue!50] (3,0) rectangle (6,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,0.9) {\small $A_R$}; - \node at (5.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6); - \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); - \draw[very thick,blue!100] (3,3) rectangle (4,3.6); - \node at (3.5,3.3) {\small $A$}; - \draw[very thick,blue!100] (4,3) rectangle (5,3.6); - \node at (4.5,3.3) {\small $B$}; - } - \only<5>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[very thick, blue!50] (3,3) rectangle (6,3.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (5.7,3.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); - \draw[very thick,blue!100] (6,3) rectangle (7,3.6); - \node at (6.5,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5); - } - \only<6>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (5.7,3.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6); - \draw[very thick,blue!100] (6,3) rectangle (7,3.6); - \node at (6.5,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - } - \only<7>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (5.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6); - \draw[very thick,blue!100] (6,3) rectangle (7,3.6); - \node at (6.5,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5); - \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3); - } - \only<8>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (6.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); - \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); - \node at (4,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - } - \only<9>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); - \draw[very thick, blue!50] (5,0) rectangle (7,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (6.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); - \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); - \node at (4,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - } - \only<10>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); - \draw[very thick, blue!50] (5,0) rectangle (7,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (6.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); - \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); - \node at (4,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - \draw[red, fill] (5,1.5) rectangle (6,2.1); - \draw[red, fill] (6.05,1.5) rectangle (7,2.1); - } - \only<11>{ - \draw[fill, blue!50] (1,0) rectangle (3,0.6); - \draw[fill, blue!50] (3,3) rectangle (3.5,3.6); - \draw[fill, blue!50] (4.5,0) rectangle (5,0.6); - \draw[very thick, blue!50] (5,0) rectangle (7,0.6); - \node at (1.5,0.9) {\small $A_L$}; - \node at (2.0,0.9) {\small $B_L$}; - \node at (3.5,3.9) {\small $A_R$}; - \node at (6.7,0.9) {\small $B_R$}; - \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6); - \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6); - \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6); - \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6); - \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6); - \node at (4,3.3) {\small $A$}; - \draw[very thick,blue!100] (7,3) rectangle (8,3.6); - \node at (7.5,3.3) {\small $B$}; - \draw[red, fill] (5,1.5) rectangle (6,2.1); - \draw[red, fill] (6.05,1.5) rectangle (7,2.1); - \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4); - \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4); - } - - \draw[very thick,->](0,0) -- (8,0); - \node [anchor=base] at (8, -0.3) {\scriptsize time}; - \node [anchor=base] at (0, -0.3) {\scriptsize 0}; - \node [anchor=base] at (-1.2, 0.2) {\small low priority}; - \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};} - \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};} - - \end{tikzpicture} - \end{tabular} - \end{textblock} - - \begin{textblock}{0}(2.5,13)% - \small - \onslide<11>{ - \begin{bubble}[8cm]% - Scheduling: You want to avoid that a high - priority process is staved indefinitely. - \end{bubble}} - \end{textblock} - - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{\Large Priority Inheritance Scheduling} - - \begin{itemize} - \item Let a low priority process $L$ temporarily inherit - the high priority of $H$ until $L$ leaves the critical - section unlocking the resource.\bigskip - \item Once the resource is unlocked $L$ returns to its original - priority level. \alert{\bf BOGUS}\pause\bigskip - \item \ldots $L$ needs to switch to the highest - \alert{remaining} priority of the threads that it blocks. - \end{itemize}\bigskip - - \small this error is already known since around 1999 - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{center} - \includegraphics[scale=0.25]{../pics/p3.jpg} - \end{center} - - \begin{itemize} - \item by Rajkumar, 1991 - \item \it ``it resumes the priority it had at the point of entry into the critical - section'' - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{center} - \includegraphics[scale=0.25]{../pics/p2.jpg} - \end{center} - - \begin{itemize} - \item by Jane Liu, 2000 - \item {\it ``The job $J_l$ executes at its inherited - priority until it releases $R$; at that time, the - priority of $J_l$ returns to its priority - at the time when it acquires the resource $R$.''}\medskip - \item \small gives pseudo code and totally bogus data structures - \item \small interesting part ``{\it left as an exercise}'' - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{center} - \includegraphics[scale=0.15]{../pics/p1.pdf} - \end{center} - - \begin{itemize} - \item by Laplante and Ovaska, 2011 (\$113.76) - \item \it ``when $[$the task$]$ exits the critical section that - caused the block, it reverts to the priority it had - when it entered that section'' - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - - \begin{center} - \includegraphics[scale=0.25]{../pics/p4.jpg} - \end{center} - - \begin{itemize} - \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible) - \item \it ``Upon releasing the lock, the - $[$low-priority$]$ thread will revert to - its original priority.'' - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{Priority Scheduling} - - \begin{itemize} - \item a scheduling algorithm that is widely used in real-time operating systems - \item has been ``proved'' correct by hand in a paper in 1983 - \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause - - \item we used the corrected algorithm and then {\bf really} proved - that it is correct - - \item we implemented this algorithm in a small OS called PINTOS - (used for teaching at Stanford) - - \item our implementation was much more efficient than their - reference implementation - - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] -\frametitle{Big Proofs in CS (1)} - -Formal proofs in CS sound like science fiction? +\frametitle{Can This Be Done?} \begin{itemize} -\item in 2008, verification of a C-compiler +\item in 2008, verification of a small C-compiler \begin{itemize} \item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour'' -\item is as good as \texttt{gcc -O1}, but much less buggy +\item is as good as \texttt{gcc -O1}, but much, much less buggy \end{itemize} \end{itemize} @@ -650,723 +229,31 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% \begin{frame}[c] -% \frametitle{Fuzzy Testing C-Compilers} - -% \begin{itemize} -% \item tested GCC, LLVM and others by randomly generating -% C-programs -% \item found more than 300 bugs in GCC and also -% many in LLVM (some of them highest-level critical)\bigskip -% \item about CompCert: - -% \begin{bubble}[10cm]\small ``The striking thing about our CompCert -% results is that the middle-end bugs we found in all other -% compilers are absent. As of early 2011, the under-development -% version of CompCert is the only compiler we have tested for -% which Csmith cannot find wrong-code errors. This is not for -% lack of trying: we have devoted about six CPU-years to the -% task.'' -% \end{bubble} -% \end{itemize} - -% \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] -\frametitle{Big Proofs in CS (2)} +\frametitle{Fuzzy Testing C-Compilers} \begin{itemize} -\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc) - \begin{itemize} - \item used in helicopters and mobile phones - \item 200k loc of proof - \item 25 - 30 person years - \item found 160 bugs in the C code (144 by the proof) - \end{itemize} -\end{itemize} - -\begin{bubble}[10cm]\small -``Real-world operating-system kernel with an end-to-end proof -of implementation correctness and security enforcement'' -\end{bubble}\bigskip\pause - -unhackable kernel (New Scientists, September 2015) -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[c] -\frametitle{Big Proofs in CS (3)} - -\begin{itemize} -\item verified TLS implementation\medskip -\item verified compilers (CompCert, CakeML)\medskip -\item verified distributed systems (Verdi)\medskip -\item verified OSes or OS components\\ -(seL4, CertiKOS, \ldots)\bigskip\pause -\item Infer static analyser developed by Facebook -\end{itemize} - -\end{frame} +\item tested GCC, LLVM and others by randomly generating +C-programs +\item found more than 300 bugs in GCC and also +many in LLVM (some of them highest-level critical)\bigskip +\item about CompCert: -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[c] -\frametitle{How Did This Happen?} - -Lots of ways! - -\begin{itemize} -\item better programming languages - \begin{itemize} - \item basic safety guarantees built in \item powerful mechanisms for abstraction and modularity - \end{itemize} -\item better software development methodology -\item stable platforms and frameworks -\item better use of specifications\medskip\\ - \small If you want to build software that works or is secure, - it is helpful to know what you mean by ``works'' and by ``is secure''! -\end{itemize} - -\end{frame} - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[c] -\frametitle{Goal} - -Remember the Bridges example? - -\begin{itemize} -\item Can we look at our programs and somehow ensure -they are bug free/correct?\pause\bigskip - -\item Very hard: Anything interesting about programs is equivalent -to the Halting Problem, which is undecidable.\pause\bigskip - -\item \alert{Solution:} We avoid this ``minor'' obstacle by - being as close as possible of deciding the halting - problem, without actually deciding the halting problem. - \small$\quad\Rightarrow$ yes, no, don't know (static analysis) +\begin{bubble}[10cm]\small ``The striking thing about our CompCert +results is that the middle-end bugs we found in all other +compilers are absent. As of early 2011, the under-development +version of CompCert is the only compiler we have tested for +which Csmith cannot find wrong-code errors. This is not for +lack of trying: we have devoted about six CPU-years to the +task.'' +\end{bubble} \end{itemize} \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state.png} - \end{center} - - \begin{itemize} - \item depending on some initial input, a program - (behaviour) will ``develop'' over time. - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state2.png} - \end{center} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state3.jpg} - \end{center} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state4.jpg} - \end{center} - - \begin{itemize} - \item to be avoided - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state5.png} - \end{center} - - \begin{itemize} - \item this needs more work - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{What is Static Analysis?} - - \begin{center} - \includegraphics[scale=0.4]{../pics/state6.png} - \end{center} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c,fragile] - \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] - Are Vars Definitely Initialised?\end{tabular}} - -Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip - -Prog.~1:\\ -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language=While,xleftmargin=3mm] -if x < 1 then y := x else y := x + 1; -y := y + 1 -\end{lstlisting}\medskip - -Prog.~2:\\ -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language=While,xleftmargin=3mm] -if x < x then y := y + 1 else y := x; -y := y + 1 -\end{lstlisting} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c,fragile] - \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] - Are Vars Definitely Initialised?\end{tabular}} - - What should the rules be for deciding when a - variable is initialised?\bigskip\pause - -\begin{itemize} -\item variable \texttt{x} is definitely initialized after - \texttt{skip}\\ - iff \texttt{x} is definitely initialized before \texttt{skip}. -\end{itemize} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c,fragile] -% \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] -% Are Vars Definitely Initialised?\end{tabular}} - -$\bl{A}$ is the set of definitely defined variables: - -\begin{center} -\begin{tabular}{c} - \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad - \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}} - \medskip\\\pause - - \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}} - \medskip\\\pause - - \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2} - {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}} - \medskip\\\pause - - \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'} - {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause -\end{tabular} -\end{center} - -\hfill we start with $\bl{A = \{\}}$ -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{\large Concrete Example: Sign-Analysis} -\mbox{}\\[-20mm]\mbox{} - -\bl{\begin{plstx}[rhs style=,one per line] : \meta{Exp} ::= \meta{Exp} + \meta{Exp} - | \meta{Exp} * \meta{Exp} - | \meta{Exp} = \meta{Exp} - | \meta{num} - | \meta{var}\\ -: \meta{Stmt} ::= \meta{label} : - | \meta{var} := \meta{Exp} - | \pcode{jmp?} \meta{Exp} \meta{label} - | \pcode{goto} \meta{label}\\ -: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ -\end{plstx}} - -\begin{textblock}{0}(7.8,2.5) -\small -\begin{bubble}[5.6cm] -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language={},xleftmargin=3mm] - a := 1 - n := 5 -top: jmp? n = 0 done - a := a * n - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} -\end{textblock} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{\large Concrete Example: Sign-Analysis} -\mbox{}\\[-20mm]\mbox{} - -\bl{\begin{plstx}[rhs style=,one per line] : \meta{Exp} ::= \meta{Exp} + \meta{Exp} - | \meta{Exp} * \meta{Exp} - | \meta{Exp} = \meta{Exp} - | \meta{num} - | \meta{var}\\ -: \meta{Stmt} ::= \meta{label} : - | \meta{var} := \meta{Exp} - | \pcode{jmp?} \meta{Exp} \meta{label} - | \pcode{goto} \meta{label}\\ -: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ -\end{plstx}} - -\begin{textblock}{0}(7.8,3.5) -\small -\begin{bubble}[5.6cm] -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language={},xleftmargin=3mm] - n := 6 - m1 := 0 - m2 := 1 -top: jmp? n = 0 done - tmp := m2 - m2 := m1 + m2 - m1 := tmp - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} -\end{textblock} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{\large Concrete Example: Sign-Analysis} -\mbox{}\\[-20mm]\mbox{} - -\bl{\begin{plstx}[rhs style=,one per line] : \meta{Exp} ::= \meta{Exp} + \meta{Exp} - | \meta{Exp} * \meta{Exp} - | \meta{Exp} = \meta{Exp} - | \meta{num} - | \meta{var}\\ -: \meta{Stmt} ::= \meta{label} : - | \meta{var} := \meta{Exp} - | \pcode{jmp?} \meta{Exp} \meta{label} - | \pcode{goto} \meta{label}\\ -: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\ -\end{plstx}} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{Eval: An Interpreter} -\mbox{}\\[-14mm]\mbox{} - -\small -\begin{center} -\bl{\begin{tabular}{lcl} -$[n]_{env}$ & $\dn$ & $n$\\ -$[x]_{env}$ & $\dn$ & $env(x)$\\ -$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\ -$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\ -$[e_1 = e_2]_{env}$ & $\dn$ & -$\begin{cases} -1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\ -0 & \text{otherwise} -\end{cases}$\\ -\end{tabular}} -\end{center} - -\footnotesize -\begin{lstlisting}[numbers=none,xleftmargin=-5mm] -def eval_exp(e: Exp, env: Env) : Int = e match { - case Num(n) => n - case Var(x) => env(x) - case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env) - case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env) - case Equ(e1, e2) => - if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0 -} -\end{lstlisting} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\small -A program -\begin{bubble}[6cm]\footnotesize -\begin{lstlisting}[numbers=none, - language={}, - basicstyle=\ttfamily, - xleftmargin=1mm] - a := 1 - n := 5 -top: jmp? n = 0 done - a := a * n - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} - -The \emph{snippets} of the program: - -\footnotesize -\begin{columns} -\begin{column}[t]{5cm} -\begin{bubble}[4.5cm] -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language={},xleftmargin=1mm] -"" a := 1 - n := 5 -top: jmp? n = 0 done - a := a * n - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} -\end{column} -\begin{column}[t]{5cm} -\begin{bubble}[4.5cm] -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language={},xleftmargin=1mm] -top: jmp? n = 0 done - a := a * n - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} -\end{column} -\begin{column}[t]{2cm} -\begin{bubble}[1.1cm] -\begin{lstlisting}[numbers=none, - basicstyle=\ttfamily, - language={},xleftmargin=1mm] -done: -\end{lstlisting} -\end{bubble} -\end{column} -\end{columns} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{Eval for Stmts} -\mbox{}\\[-12mm]\mbox{} - -Let \bl{$sn$} be the snippets of a program - -\small -\begin{center} -\bl{\begin{tabular}{lcl} -$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\ -$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\ -$[x \,\texttt{:=}\, a::rest]_{env}$ & $\dn$ & -$[rest]_{(env[x:= [a]_{env}])}$\medskip\\ -$[\texttt{jmp?}\;b\;l::rest]_{env}$ & $\dn$ & -$\begin{cases} -[sn(l)]_{env} & \text{if}\quad[b]_{env} = true\\ -[rest]_{env} & \text{otherwise} -\end{cases}$\medskip\\ -$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\ -\end{tabular}} -\end{center}\bigskip - -Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{Eval in Code} - -\footnotesize -\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm] -def eval(sn: Snips) : Env = { - def eval_stmts(sts: Stmts, env: Env) : Env = sts match { - case Nil => env - - case Label(l)::rest => eval_stmts(rest, env) - - case Assign(x, e)::rest => - eval_stmts(rest, env + (x -> eval_exp(e, env))) - - case Jmp(b, l)::rest => - if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) - else eval_stmts(rest, env) - - case Goto(l)::rest => eval_stmts(sn(l), env) - } - - eval_stmts(sn(""), Map()) -} -\end{lstlisting} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{The Idea of Static Analysis} -\small -\mbox{}\bigskip\\ - -\begin{columns} -\begin{column}{5cm} -\begin{bubble}[4.5cm]\footnotesize -\begin{lstlisting}[numbers=none, - language={}, - basicstyle=\ttfamily, - xleftmargin=1mm] - a := 1 - n := 5 -top: jmp? n = 0 done - a := a * n - n := n + -1 - goto top -done: -\end{lstlisting} -\end{bubble} -\end{column} - -\begin{column}{1cm} -\raisebox{-20mm}{\LARGE\bf$\Rightarrow$} -\end{column} -\begin{column}{6cm} -\begin{bubble}[4.7cm]\footnotesize -\begin{lstlisting}[numbers=none, - language={}, - basicstyle=\ttfamily, - xleftmargin=1mm, - escapeinside={(*}{*)}] - a := (*\hl{'+'}*) - n := (*\hl{'+'}*) -top: jmp? n = (*\hl{'0'}*) done - a := a * n - n := n + (*\hl{'-'}*) - goto top -done: -\end{lstlisting} -\end{bubble} -\end{column} -\end{columns}\bigskip\bigskip - -Replace all constants and variables by either -\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out -is what the sign of \texttt{a} and \texttt{n} is (they should -always positive). - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{Sign Analysis?} - - - \begin{columns} - \begin{column}{3cm} - \begin{tabular}{cc|l} - $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{} - - & - & -\\ - - & 0 & -\\ - - & + & -, 0, +\\ - 0 & $x$ & $x$\\ - + & - & -, 0, +\\ - + & 0 & +\\ - + & + & +\\ - \end{tabular} - \end{column} - - \begin{column}{3cm} - \begin{tabular}{cc|l} - $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{} - - & - & +\\ - - & 0 & 0\\ - - & + & -\\ - 0 & $x$ & 0\\ - + & - & -\\ - + & 0 & 0\\ - + & + & +\\ - \end{tabular} - \end{column} - \end{columns} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\mbox{}\\[-13mm]\mbox{} - -\small -\begin{center} -\bl{\begin{tabular}{lcl} -$[n]_{aenv}$ & $\dn$ & -$\begin{cases} -\{+\} & \text{if}\; n > 0\\ -\{-\} & \text{if}\; n < 0\\ -\{0\} & \text{if}\; n = 0 -\end{cases}$\\ -$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\ -$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\ -$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\ -$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\ -\end{tabular}} -\end{center} - -\scriptsize -\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm] -def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match { - case Num(0) => Set(Zero) - case Num(n) if (n < 0) => Set(Neg) - case Num(n) if (n > 0) => Set(Pos) - case Var(x) => aenv(x) - case Plus(e1, e2) => - aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) - case Times(e1, e2) => - atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv)) - case Equ(e1, e2) => Set(Zero, Pos) -} -\end{lstlisting} - -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\begin{frame}[fragile] -\frametitle{AEval for Stmts} -\mbox{}\\[-12mm]\mbox{} - -Let \bl{$sn$} be the snippets of a program - -\small -\begin{center} -\bl{\begin{tabular}{lcl} -$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\ -$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\ -$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & -$(rest, aenv[x:= [e]_{aenv}])$\medskip\\ -$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & -$(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\ -$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\ -\end{tabular}} -\end{center}\bigskip - -Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to -reach all \emph{states} you can find (until a fix point is reached). - -Check whether there are only $aenv$ in the final states that have -your property. -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{Sign Analysis} - - \begin{itemize} - \item We want to find out whether \texttt{a} and \texttt{n} - are always positive?\medskip - \item After a few optimisations, we can indeed find this out. - \begin{itemize} - \item equal signs return only \texttt{+} or \texttt{0} - \item branch into only one direction if you know - \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ - cannot be negative - \end{itemize}\bigskip - - \item What is this good for? Well, you do not need - underflow checks (in order to prevent buffer-overflow - attacks). In general this technique is used to make sure - keys stay secret. - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \begin{frame}[c] - \frametitle{Take Home Points} - - \begin{itemize} - \item While testing is important, it does not show the - absence of bugs/vulnerabilities.\medskip - \item More and more we need (formal) proofs that show - a program is bug free.\medskip - - \item Static analysis is more and more employed nowadays - in order to automatically hunt for bugs. - \end{itemize} - - \end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \end{document} - %%% Local Variables: %%% mode: latex %%% TeX-master: t