diff -r 29fc780ca130 -r fa7f7144f2bb slides/slides05.tex --- a/slides/slides05.tex Tue Dec 07 01:35:00 2021 +0000 +++ b/slides/slides05.tex Tue Dec 07 23:17:51 2021 +0000 @@ -8,6 +8,129 @@ \usetikzlibrary{shapes,arrows,shadows} +% Swift, example (a*)*b +\begin{filecontents}{re-swift.data} +5 0.001 +10 0.001 +15 0.009 +20 0.178 +23 1.399 +24 2.893 +25 5.671 +26 11.357 +27 22.430 +\end{filecontents} + +% Dart, example (a*)*b +\begin{filecontents}{re-dart.data} +20 0.042 +21 0.084 +22 0.190 +23 0.340 +24 0.678 +25 1.369 +26 2.700 +27 5.462 +28 10.908 +29 21.725 +30 43.492 +\end{filecontents} + + +\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-js.data} +5 0.061 +10 0.061 +15 0.061 +20 0.070 +23 0.131 +25 0.308 +26 0.564 +28 1.994 +30 7.648 +31 15.881 +32 32.190 +\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} + +\begin{filecontents}{re-java9.data} +1000 0.01410 +2000 0.04882 +3000 0.10609 +4000 0.17456 +5000 0.27530 +6000 0.41116 +7000 0.53741 +8000 0.70261 +9000 0.93981 +10000 0.97419 +11000 1.28697 +12000 1.51387 +14000 2.07079 +16000 2.69846 +20000 4.41823 +24000 6.46077 +26000 7.64373 +30000 9.99446 +34000 12.966885 +38000 16.281621 +42000 19.180228 +46000 21.984721 +50000 26.950203 +60000 43.0327746 +\end{filecontents} + + \hfuzz=220pt %\setmonofont[Scale=.88]{Consolas} @@ -38,16 +161,100 @@ \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ %Office: & N\liningnums{7.07} (North Wing, Bush House)\bigskip\\ - Slides \& Code: & KEATS\\ + Slides \& Code: & KEATS\bigskip\\ % & \onslide<2>{\alert{PDF: A Crash-Course in Scala}}\bigskip\\ %Office Hours: & Thursdays 12:00 -- 14:00\\ - %Additionally: & (for Scala) Tuesdays 10:45 -- 11:45\\ + %Additionally: & (for Scala) Tuesdays 10:45 -- 11:45\\ + \multicolumn{2}{c}{\Large\textbf{https://pollev.com/cfltutoratki576}}\\[2cm] \end{tabular} \end{center} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\begin{frame}<1>[c] + \frametitle{Main 3: Regexes} + +\begin{center} + \mbox{Graphs: regex \alert{\texttt{(a*)*b}} and strings $\underbrace{\;\texttt{a}\ldots \texttt{a}\;}_{n}$}\bigskip + + + \small +\begin{tabular}[t]{@{\hspace{-8mm}}c@{\hspace{-0mm}}c@{}} +\only<1>{\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={Java 8,Python,JavaScript,Swift,Dart}, + %legend entries={\small{}Python, \small{}Java 8, \small{}JavaScript}, + 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}; +\addplot[red,mark=*, mark options={fill=white}] table {re-js.data}; +\addplot[magenta,mark=*, mark options={fill=white}] table {re-swift.data}; +\addplot[brown,mark=*, mark options={fill=white}] table {re-dart.data}; +\end{axis} +\end{tikzpicture}}}% +\only<2>{\raisebox{0mm}{\begin{tikzpicture} +\begin{axis}[ + xlabel={$n$}, + x label style={at={(1.05,0.0)}}, + ylabel={time in secs}, + %y label style={at={(0.06,0.5)}}, + enlargelimits=false, + %xtick={0,30000,...,60000}, + xmax=65000, + ymax=35, + ytick={0,5,...,30}, + scaled ticks=true, + axis lines=left, + width=5.5cm, + height=5cm, + legend entries={\small{}Java 9}, + legend pos=north west] +\addplot[cyan,mark=*, mark options={fill=white}] table {re-java9.data}; +\end{axis} +\end{tikzpicture}}} + & +\onslide<1-2>{\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, + legend entries={You in M3}, + %%scaled ticks=false, + width=5.5cm, + height=5cm] +%%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data}; +\addplot[magenta,mark=square*,mark options={fill=white}] table {re3a.data}; +\end{axis} +\end{tikzpicture}} +\end{tabular} +\end{center} + +\hfill\small\url{https://vimeo.com/112065252} +\end{frame} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\begin{frame}[c] @@ -241,151 +448,6 @@ \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm, - text centered, minimum height=2em,drop shadow] -\tikzstyle{ann} = [above, text width=4em, text centered] -\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, - minimum height=6em, rounded corners, drop shadow,line width=1mm] - -\begin{frame}[fragile,c] -\frametitle{Compilers 6CCS3CFL} - -\begin{tikzpicture} - % Validation Layer is the same except that there are a set of nodes and links which are added - - \path (0,0) node (IR) [sc] {\textbf{WHILE Language}\\ compiler}; - \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {Fact}; - \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {Fib}; - \path (IR.west)+(-2.2,-0.7) node (sou4)[sensor] {Primes}; - \only<2>{\path (IR.west)+(-2.2,-1.9) node (sou3)[sensor] {BrainF**k};} - - \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160); - \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180); - \only<2>{\path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);} - \path [draw,->,line width=1mm] (sou4.east) -- node [above] {} (IR.190); - - \path (IR.east)+(2.2, 0.8) node (tar2)[sensor] {JVM}; - \path (IR.east)+(2.2,-0.8) node (tar3)[sensor] {LLVM{\small(x86)}}; - - \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5); - \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.-5); - - -\end{tikzpicture} -\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} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%% ~2,237,800 lines of proof in 474 - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\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} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -393,8 +455,7 @@ \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 3.0\medskip +\item Martin Odersky (EPFL) developed Scala 3.0\medskip \item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip @@ -463,26 +524,6 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -\begin{frame}[t] - - \begin{center} - \includegraphics[scale=0.4]{../pics/mind2.jpg} - \end{center} - - \begin{textblock}{14}(2,11.4) - \large\bf{}Mind-Blowing Programming Languages:\\ - \centering Scala\;\;? - \end{textblock} -\end{frame} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - - -\end{document} - \end{document}