zapashcanon 11 months ago
parent
commit
3e7cd923b9
Signed by: zapashcanon GPG Key ID: 8981C3C62D1D28F1
  1. 8
      src/main.tex
  2. 262
      src/slides.tex

8
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}
}

262
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}

Loading…
Cancel
Save