# HG changeset patch # User Christian Urban # Date 1544152546 0 # Node ID 0c752ac51cfa4ba5c7a57ad8933bce5201d8c546 # Parent 046f37a262d0fab1616b5355c52e32d79e20d3e5 updated diff -r 046f37a262d0 -r 0c752ac51cfa pics/compcert.png Binary file pics/compcert.png has changed diff -r 046f37a262d0 -r 0c752ac51cfa pics/drone.jpg Binary file pics/drone.jpg has changed diff -r 046f37a262d0 -r 0c752ac51cfa slides/slides05.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slides/slides05.tex Fri Dec 07 03:15:46 2018 +0000 @@ -0,0 +1,434 @@ +\documentclass[dvipsnames,14pt,t,xelatex]{beamer} +\usepackage{../slides} +\usepackage{../graphics} +\usepackage{../langs} +%%\usepackage{../data} +\usepackage[export]{adjustbox} + +\hfuzz=220pt + +%\setmonofont[Scale=.88]{Consolas} +%\newfontfamily{\consolas}{Consolas} + +\lstset{language=Scala, + style=mystyle, + numbersep=0pt, + numbers=none, + xleftmargin=0mm} + +\newcommand{\bl}[1]{\textcolor{blue}{#1}} + +% beamer stuff +\renewcommand{\slidecaption}{PEP (Scala) 05, King's College London} + +\begin{filecontents}{re3a.data} +1 0.00003 +500001 0.22527 +1000001 0.62752 +1500001 0.88485 +2000001 1.39815 +2500001 1.68619 +3000001 1.94957 +3500001 2.15878 +4000001 2.59918 +4500001 5.90679 +5000001 13.11295 +5500001 19.15376 +6000001 40.16373 +\end{filecontents} +\begin{filecontents}{re-python2.data} +1 0.033 +5 0.036 +10 0.034 +15 0.036 +18 0.059 +19 0.084 +20 0.141 +21 0.248 +22 0.485 +23 0.878 +24 1.71 +25 3.40 +26 7.08 +27 14.12 +28 26.69 +\end{filecontents} + +\begin{filecontents}{re-java.data} +5 0.00298 +10 0.00418 +15 0.00996 +16 0.01710 +17 0.03492 +18 0.03303 +19 0.05084 +20 0.10177 +21 0.19960 +22 0.41159 +23 0.82234 +24 1.70251 +25 3.36112 +26 6.63998 +27 13.35120 +28 29.81185 +\end{filecontents} + +%All O2 technical teams are working closely with one of our third party suppliers who has identified a global software issue in their system which has impacted data services. + + +\begin{document} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[t] +\frametitle{% + \begin{tabular}{@ {}c@ {}} + \\[5mm] + \huge PEP Scala (5) + \end{tabular}} + + \normalsize + \begin{center} + \begin{tabular}{ll} + Email: & christian.urban at kcl.ac.uk\\ + Office: & N\liningnums{7.07} (North Wing, Bush House)\\ + Slides \& Code: & KEATS\medskip\\ + Office Hours: & Mondays 12:00 -- 14:00\\ + \end{tabular} + \end{center} + + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\small + +\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm] +def get_csv_url(url: String) : List[String] = { + val csv = Try(Source.fromURL(url)).getOrElse(null) + if (csv == null){ + List() + } + else { + .... + } +} +\end{lstlisting} + +\pause +\bigskip +\rule{11cm}{0.3mm} +\bigskip + +\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm] +def get_csv_url(url: String) : List[String] = { + Try(Source.fromURL(url)....).getOrElse(Nil) +\end{lstlisting} + + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\small + +\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm] +def get_csv_url(url: String) : List[String] = { + try { + val csvFile = Source.fromURL(url) + .... + } catch { + case unknown : Throwable => List() + } +} +\end{lstlisting} + + +\bigskip +\rule{11cm}{0.3mm} +\bigskip + +\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm] +def get_csv_url(url: String) : List[String] = { + Try(Source.fromURL(url)....).getOrElse(Nil) +\end{lstlisting} + + +\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 + + + \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 2011, verification of a small C-compiler (CompCert) +\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} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c] +\frametitle{seL4 / Isabelle} + +\begin{itemize} +\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip +\item US DoD has competitions to hack into drones; they found that the + isolation guarantees of seL4 hold up\bigskip +\item CompCert and seL4 sell their code +\end{itemize} + +\only<2>{ +\begin{textblock}{5}(5.5,1.9) + \includegraphics[scale=0.25]{../pics/drone.jpg} +\end{textblock}} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c] + \frametitle{CW9 : Regexes} + +\begin{center} + Graphs: $(a^*)^* b$ and strings $\underbrace{\;a\ldots a\;}_{n}$\bigskip + +\begin{tabular}[t]{@{\hspace{-8mm}}c@{\hspace{-4mm}}c@{}} +\raisebox{6mm}{\begin{tikzpicture} +\begin{axis}[ + xlabel={$n$}, + x label style={at={(1.05,0.0)}}, + ylabel={time in secs}, + enlargelimits=false, + xtick={0,5,...,30}, + xmax=33, + ymax=35, + ytick={0,5,...,30}, + scaled ticks=false, + axis lines=left, + width=5.5cm, + height=5cm, + legend entries={Python, Java 8}, + legend pos=north west, + legend cell align=left] +\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data}; +\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data}; +\end{axis} +\end{tikzpicture}} + & +\onslide<1>{\begin{tikzpicture} + \begin{axis}[ + xlabel={$n$}, + x label style={at={(1.05,0.0)}}, + ylabel={time in secs}, + enlargelimits=false, + ymax=35, + ytick={0,5,...,30}, + axis lines=left, + %%scaled ticks=false, + width=5.5cm, + height=5cm] +%%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data}; +\addplot[red,mark=square*,mark options={fill=white}] table {re3a.data}; +\end{axis} +\end{tikzpicture}} +\end{tabular} +\end{center} + + +\small +\hfill Kuklewicz: most POSIX matchers are buggy\\ +\footnotesize +\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix} +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}[c] +\frametitle{Where to go on from here?} + +\begin{itemize} +\item Martin Odersky (EPFL)\ldots he is currently throwing out everything + and starts again with the dotty compiler for Scala\medskip + +\item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip + +\item Haskell, Ocaml, Standard ML, Scheme, \ldots +\end{itemize} +\end{frame} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}[c,fragile] +\frametitle{\alert{Questions?}} + +{\tiny +\begin{verbatim} + * + * * + * * + * * * * + * * + * * * * + * * * * + * * * * * * * * + * * + * * * * + * * * * + * * * * * * * * + * * * * + * * * * * * * * + * * * * * * * * + * * * * * * * * * * * * * * * * + * * + * * * * + * * * * + * * * * * * * * + * * * * + * * * * * * * * + * * * * * * * * + * * * * * * * * * * * * * * * * + * * * * + * * * * * * * * + * * * * * * * * + * * * * * * * * * * * * * * * * + * * * * * * * * + * * * * * * * * * * * * * * * * + * * * * * * * * * * * * * * * * +* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * +\end{verbatim}} + + +\begin{textblock}{6}(8.5,3.5) +\begin{bubble}[5cm] +\footnotesize +\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm] +++++++++[>+>++++<<-]>++>> ++<[-[>>+<<-]+>>]>+[-<<<[- +>[+[-]+>++>>>-<<]<[<]>>++ +++++[<<+++++>>-]+<<++.[-] +<<]>.>+[>>]>+] +\end{lstlisting} +\end{bubble} +\end{textblock} + +\end{frame} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\begin{frame}[c] +\frametitle{Marks for CW6 (Part 1 + 2)} + +Raw marks: + +\begin{itemize} +\item 6\%: 154 students +\item 5\%: 66 +\item 4\%: 18 +\item 3\%: 13 +\item 2\%: 2 +\item 1\%: 1 +\item 0\%: 21 +\end{itemize} +\end{frame} + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\end{document} + + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: +