diff --git a/src/main.tex b/src/main.tex index 525d856..0fb2da3 100644 --- a/src/main.tex +++ b/src/main.tex @@ -1,4 +1,5 @@ \documentclass[12pt]{beamer} +\usepackage[english]{babel} \usetheme[]{metropolis} @@ -6,6 +7,11 @@ \usepackage[notransparent]{svg} % to include svg \usepackage{minted} % source code highlighting \setminted{autogobble=true} % remove unneeded indentation +\setminted{fontsize=\footnotesize} % set font size globally + +\usepackage{xcolor} % color, dvipsnames allows to get more names +\definecolor{mypink}{rgb}{0.858, 0.188, 0.478} +\newcommand{\hl}[1]{\textcolor{mypink}{#1}} \setmainfont{Linux Libertine O} \setsansfont{Linux Biolinum O} @@ -14,7 +20,7 @@ \newcommand{\auth}[3]{#1 {\tiny{\texttt{<#2>}}}\textsuperscript{#3}} \title{Wasocaml: compiling OCaml to WebAssembly} -\author{\auth{Léo Andrès}{l@ndrs.fr}{1, 2}\\ +\author{\auth{\hl{Léo Andrès}}{l@ndrs.fr}{1, 2}\\ \auth{Pierre Chambart}{pierre.chambart@ocamlpro.com}{1}\\ \auth{Jean-Christophe Filliâtre}{jean-christophe.filliatre@cnrs.fr}{2} } diff --git a/src/slides.tex b/src/slides.tex index 3fd9844..ecf168a 100644 --- a/src/slides.tex +++ b/src/slides.tex @@ -1,7 +1,12 @@ \newcommand{\ocaml}[1]{\mintinline{ocaml}{#1}} \newcommand{\wasm}[1]{\mintinline{wast}{#1}} -% TODO: about part (me, ocp, lmf) ? +%- Un peu dommage que les transparents n'aient pas de titre. Par la différence entre 4 et 5 serait plus immédiate si un titre était là. +%- partout : mettre les mots les plus importants en couleur +%- 11 : je ne sais pas quelle est ta transition à l'oral, mais ce n'est pas évident de balancer comme ça l'architecture du compilo ocaml d'un coup sans avoir écrit le mot OCaml nulle part ! + + +% TODO: about part (me, ocp, lmf)? % JavaScript / Wasm @@ -29,7 +34,7 @@ \begin{itemize} \item compact binary format (Wasm) and text format (Wat) \item functions - \item stack machine (stack can not be inspected) + \item stack (can not be inspected) \item static verification and typecheck (few dynamic tests) \item one \wasm{memory} per module \item only scalar types: \wasm{i32}, \wasm{i64}, \wasm{f32}, \wasm{f64} @@ -39,6 +44,7 @@ \end{frame} \begin{frame}[fragile] + Wat with S-expressions: \begin{minted}{wast} (func $fact (param $x i32) (result i32) (if (i32.eq (local.get $x) (i32.const 0)) @@ -54,6 +60,7 @@ \end{frame} \begin{frame}[fragile] + Wat with ASM syntax: \begin{minted}{wast} (func $fact (param $x i32) (result i32) i32.const 0 @@ -74,33 +81,36 @@ % C/C++/Rust to Wasm1 \begin{frame} - Compiling runtime-free languages such as C/C++/Rust to Wasm is straightforward.\\ + Compiling \hl{runtime-free} languages such as C/C++/Rust to Wasm is straightforward.\\ + \\ Some primitives such as \mintinline{c}{malloc} need to be rewritten in Wasm and provided by the compiler. \end{frame} \begin{frame}[fragile] - How does a GC work ? + How does a GC work? \begin{itemize} - \item \emph{Tracing}: we start from \emph{roots} and we find live objects recursively (OCaml, Java) - \item \emph{Reference counting}: we start from dying objects and we kill objects recursively (Python) + \item \emph{Tracing}: we start from \hl{roots} and we find live objects recursively (OCaml, Java) + \item \emph{Reference counting}: we start from dying objects and we kill objects recursively (Python\footnote{plus a tracing one for cycles\ldots}) \end{itemize} - We need to discriminate pointers: +\end{frame} + +\begin{frame}[fragile] + We need to discriminate \hl{pointers}: \begin{itemize} \item \emph{Conservative (Boehm)}: we make a guess and accept memory leaks (Crystal, Guile, Inkscape). \item \emph{Precise}: we have the right information (almost everybody). \end{itemize} - We must have the information somewhere at runtime: quite similar to polymorphism! + Need the information somewhere at \hl{runtime}: similar to polymorphism \end{frame} -% TODO: how do GC work % GC languages to Wasm1 \begin{frame} - Compiling garbage-collected languages to Wasm1 is more involved: + Compiling GC languages to Wasm1 is more involved: \begin{itemize} \item runtime must be rewritten, or compiled from C to Wasm: difficult because of Wasm safety properties - \item GC need to inspect the stack to find roots, not possible in Wasm, requires a shallow stack - \item interactions with the GC of the embedder are difficult (cycles can't be collected) + \item GC need to inspect the stack to find roots, not possible in Wasm, requires a \hl{shallow stack} + \item interactions with the GC of the \hl{embedder} are difficult (cycles can't be collected) \end{itemize} Need for a proper GC in Wasm. @@ -119,13 +129,21 @@ \begin{frame} A type system to represent values from any kind of source language is too complex.\\ + \\ Instead, WasmGC introduces reference types and a subtyping hierarchy: \begin{center} \includegraphics[width=20em]{figure_type_hierarchy.mps} \end{center} The hierarchy tells which casts are allowed.\\ +\end{frame} + +\begin{frame} + \begin{center} + \includegraphics[width=20em]{figure_type_hierarchy.mps} + \end{center} Upcasts are implicit.\\ Downcasts are explicit and lead to runtime errors if incorrect.\\ + \\ Casts are cheap.\\ Possible to dynamically test for compatibility. \end{frame} @@ -155,95 +173,58 @@ \begin{frame}[fragile] \begin{minted}{ocaml} - let f = print_int let rec iter f l = match l with | [] -> () | hd :: tl -> f hd; iter f tl + let () = - let iter_print = iter f in + let iter_print = iter print_int in iter_print [2; 1] \end{minted} \end{frame} \begin{frame}[fragile] -\fontsize{5pt}{5pt}\selectfont -\begin{minted}{ocaml} -let f = - let s = - make_closures - | cl_f { x } env -> print_int x - with vars - end - in - project_closure cl_f from s -in - + \begin{minted}[fontsize={\fontsize{9}{9}\selectfont}]{ocaml} let iter = - let set = - make_closures + let set = make_closures | cl_iter { f } env -> - let otherset = - make_closures + let otherset = make_closures | cl_iter_f { l } envtwo -> switch l - with int - | 0 -> const 0 - with tag - | 0 -> - let x = get_field 0 l in - let f = project_var f from envtwo in - let dummy = f x in - let tl = get_field 1 l in + with int | 0 -> const 0 + with tag | 0 -> + let x = get_field 0 l + let f = project_var f from envtwo + let dummy = f x + let tl = get_field 1 l envtwo tl - end - with vars - | f -> f - end - in + with vars | f -> f end project_closure cl_iter_f from otherset - with vars - end - in project_closure cl_iter from set -in - -let lempty = const 0 in -let one = const 1 in -let lone = make_block 0 one lempty in -let two = const 2 in -let ltwo = make_block 0 two lone in -let iter_print = iter f in + +let lempty = const 0 +let one = const 1 +let lone = make_block 0 one lempty +let two = const 2 +let ltwo = make_block 0 two lone +let iter_print = iter print_int iter_print ltwo \end{minted} \end{frame} \begin{frame} - Value representation strategies: - \begin{itemize} - \item monomorphisation (C++/Rust) - \item boxing everything (Python) - \item boxing only in polymorphic places (Java) - \item pointer-tagging: unboxing small scalars (OCaml) - \item tagged union (Lua) - % TODO: add it back ? - %\item type-passing (TIL, AliceML) - \item runtime monomorphisation (F\#) - \end{itemize} -\end{frame} - -\begin{frame} - uniform representation using a tagged single machine word: + \hl{uniform representation} using a \hl{tagged} single machine word: \begin{center} \includegraphics[width=10em]{figure_ocaml_bit1.mps} \end{center} - if $b_{0} = 0$, the value is a pointer to a heap-allocated block: + if $b_{0} = 0$, the value is a pointer to a \hl{heap-allocated block}: \begin{center} \includegraphics[width=20em]{figure_ocaml_bit2.mps} \end{center} - if $b_{1} = 1$, the $n - 1$ most significant bits are a small scalar: + if $b_{1} = 1$, the $n - 1$ most significant bits are a \hl{small scalar}: \begin{center} \includegraphics[width=20em]{figure_ocaml_bit3.mps} \end{center} @@ -261,13 +242,16 @@ iter_print ltwo Others heap-allocated blocks are \wasm{struct} or \wasm{array}. \end{frame} -% TODO: example with i31 ? +% TODO: example with i31? \begin{frame} - In \ocaml{get_field n x} the type of \ocaml{x} is unknown.\\ + In \ocaml{get_field n x} the \hl{type} of \ocaml{x} is \hl{unknown}.\\ + \\ Could propagate more types but breaks some optimisations.\\ + \\ Not enough because of \ocaml{Obj.field}.\\ - All we know is that \ocaml{x} is a block of size $n + 1$ at least. + \\ + All we know is that \ocaml{x} is a block of \hl{size $n + 1$ at least}. \end{frame} \begin{frame}[fragile] @@ -302,13 +286,18 @@ iter_print ltwo let front_facing_baby_chick = "🐥" \end{minted} \setmonofont{RobotoMono Nerd Font} + \onslide<2-> { Modules represented as blocks: each toplevel value is a field. + } + \onslide<3-> { \begin{center} \emph{too long subtyping chain} ☹ \end{center} - We have two variations to avoid this problem, not implemented yet. - % TODO: explain the two variations quickly ? -% TODO: ^ split on many slides + } + \onslide<4-> { + We have two variants to avoid this problem while still using \wasm{struct}, not implemented yet. + } + % TODO: explain the two variants quickly? \end{frame} \begin{frame}[fragile] @@ -316,7 +305,8 @@ iter_print ltwo \begin{minted}{wast} (type $block (array eqref)) \end{minted} - An array of \wasm{eqref} with the tag stored at position 0. + An array of \wasm{eqref} with the tag stored at position 0.\\ + \\ Tradeoffs: \begin{itemize} \item implicit bounds check at each access @@ -335,70 +325,105 @@ iter_print ltwo (field $v1 eqref) (field $v2 eqref))) \end{minted} - Actual representation is more complex to handle mutually recursives functions and to reduce casts.\\ - Only place where we use Wasm recursives types.\\ + Actual representation is more complex to handle mutually recursive functions and to reduce casts.\\ + Only place where we use Wasm recursive types.\\ To handle currification, functions of arity one need to be supertypes of all others closures. \end{frame} -% TODO: exceptions - \begin{frame} - \begin{description} - \item[monomorphisation] works with Wasm1 - \item[boxing everything] works with WasmGC + our strategies - \item[polymorphic boxing] works with WasmGC + our strategies - \item[pointer-tagging] works with WasmGC + our strategies - \item[tagged union] works with WasmGC + our strategies - % TODO: add it back ? - %\item[type-passing] ? - \item[runtime monomorphisation] doesn't work easily - \end{description} + Exceptions:\\ + \begin{itemize} + \item use the \hl{exception handling proposal} + \item maps quite directly + \item don't have \hl{runtime generated} exceptions + \item a single Wasm exception, handle identifiers on the side + \end{itemize} \end{frame} % Formalized compilation \begin{frame} - We have a proper small-step semantics for a subset of Flambda where functions all have arity one, objects primitives are removed and where exceptions are only static.\\ + A proper \hl{small-step semantics} for a subset of Flambda where functions all have arity one, objects primitives are removed and where exceptions are only static.\\ \\ - This is the first Flambda1 semantics.\\ + \onslide<2-> { + The first Flambda1 semantics.\\ + } \\ - We also have a formalized compilation scheme from Flambda1 to WasmGC.\\ + \onslide<3-> { + A \hl{formalized compilation scheme} from Flambda1 to WasmGC.\\ + } \\ - The proof of correctness is not done yet (would like to use WasmGC semantics which is still ongoing work).\\ + \onslide<4-> { + Proof of correctness is not done yet (would like to use WasmGC semantics which is still ongoing work).\\ + } \\ + \onslide<5-> { The parser, interpreter and compiler targeting WasmGC for mini-Flambda1 fit in 1300 lines of OCaml. + } \end{frame} % Wasocaml + \begin{frame} - The real compiler is called Wasocaml and is available at \href{https://github.com/ocaml-wasm/wasocaml}{github.com/ocaml-wasm/wasocaml}.\\ + The real compiler is called Wasocaml and is available at \hl{\href{https://github.com/ocamlpro/wasocaml}{github.com/ocamlpro/wasocaml}}.\\ \\ + \onslide<2-> { Meant as a way to demonstrate the usefulness of \wasm{i31ref} and convinced the WasmGC working group (along with the Guile implementation that came a few months later).\\ + } \\ + \onslide<3-> { Only a fraction of the stdlib externals are provided and the object fragments of the language has not yet been implemented.\\ + } \\ - The first compiler for a functional language targeting WasmGC. - + \onslide<4-> { + The first compiler for a real-world functional language targeting WasmGC. + } \end{frame} % Benchmarks \begin{frame} - Benchmarks using the experimental branch of V8:\\ \\ + \onslide<2-> { No real sized programs for now.\\ + } \\ + \onslide<3-> { Classical functional microbenchmarks are two times slower than native OCaml..\\ + } \\ - Knuth-Bendix: exceptions are slow (100 times slower than native for a raise) and we need to discuss this with the V8 team (in SpiderMonkey they're fast but other extensions are missing).\\ + \onslide<4-> { + Knuth-Bendix: exceptions are slow (100 times slower than native for a raise) and we need to discuss this with the V8 team (in SpiderMonkey they're fast but other extensions are missing). + } +\end{frame} + +\begin{frame} + Since yesterday:\\ + \begin{itemize} + \onslide<2-> { + \item do not use Wasm exceptions + } + \onslide<3-> { + \item return a pair with a boolean set to true when an exception was raised + } + \onslide<4-> { + \item a hundred times faster than Wasm exceptions + } + \onslide<5-> { + \item KB: 2.7 times slower than native + } + \end{itemize} +\end{frame} + +\begin{frame} + With \hl{casts as no-ops} we have a 10\% gain.\\ \\ - With casts as no-ops we have a 10\% gain.\\ With optimisations and Flambda2 it should be much better.\\ - Jsoo is slower in an unpredictable fashion (up to 40 times) - % TODO: ^ split in many slides ? + \\ + Jsoo is slower in an \hl{unpredictable} fashion (up to 40 times) \end{frame} % FFI @@ -417,18 +442,23 @@ iter_print ltwo \end{minted} \end{frame} -\begin{frame} - With recent additions to Clang, it would be possible to re-use existing bindings and to compile the C code with emscriptem with almost no changes to the bindings.\\ +\begin{frame}[fragile] + With recent additions to Clang, it would be possible to \hl{re-use existing bindings} and to compile the C code with emscriptem with almost no changes to the bindings.\\ \\ - We only need to provide alternative FFI headers files, replacing usual macros by hand-written Wasm functions.\\ + We only need to provide \hl{alternative FFI headers files}, replacing usual macros by hand-written Wasm functions.\\ \\ The only limitation we forsee is that the \mintinline{c}{Field} macro won't be usable as an l-value anymore. We would need a new \mintinline{c}{Set_field} macro instead. + \begin{minted}{c} + Field(v, n) = ...; // not anymore + Set_field(b, v, n); // OK + \end{minted} \end{frame} +% TODO: the Field macro is too technical ? % Effects \begin{frame} - OCaml 5.0 is multicore. We're based on 4.14 so effects handlers are not supported.\\ + OCaml 5.0 is \hl{multicore}. We're based on 4.14 so \hl{effects handlers} are not supported.\\ We could use: \begin{itemize} \item CPS transformation @@ -439,25 +469,27 @@ iter_print ltwo % Related works -% TODO: ? +% TODO:? % Future works -% TODO: ? +% TODO:? % Symbolic execution -% TODO: ? +% TODO:? \begin{frame} Contributions: \begin{itemize} - \item a Wasm backend for OCaml + \item OCaml Wasm backend \hl{github.com/ocamlpro/wasocaml} \item the first compiler for a functional language to WasmGC \item impact on the GC proposal for Wasm \item the first Flambda1 semantics - \item a formalized compilation scheme from Flambda1 to WasmGC - \item compilation strategies usable by others compilers (Guile, Wasm\_of\_ocaml) + \item a formalized compilation scheme + \item compilation strategies usable by others compilers + \item ongoing: proof of the compilation + \item ongoing: symbolic execution of WasmGC program \end{itemize} - Thanks ! + Thanks! \end{frame}