gray!40 gray!40

# Continuing WebAssembly with Effect Handlers

Luna Phipps-Costin  0009-0001-4398-6987 Northeastern UniversityUSA phipps-
<EMAIL_ADDRESS>,  Andreas Rossberg  0000-0003-3137-3160
UnaffiliatedGermany<EMAIL_ADDRESS>,  Arjun Guha  0000-0002-7493-3271
Northeastern UniversityUSA<EMAIL_ADDRESS>,  Daan Leijen
0000-0003-1027-5430 Microsoft ResearchUSA<EMAIL_ADDRESS>,  Daniel
Hillerström  0000-0003-4730-9315 Huawei Zurich Research CenterSwitzerland
<EMAIL_ADDRESS>,  KC Sivaramakrishnan  0000-0002-3491-1780
Tarides and IIT MadrasIndia<EMAIL_ADDRESS>,  Matija Pretnar
0000-0001-7755-2303 Ljubljana UniversitySlovenia<EMAIL_ADDRESS>and  Sam Lindley  0000-0002-1360-4714 The University of EdinburghUnited
Kingdom<EMAIL_ADDRESS>
###### Abstract.

WebAssembly (Wasm) is a low-level portable code format offering near native
performance. It is intended as a compilation target for a wide variety of
source languages. However, Wasm provides no direct support for non-local
control flow features such as async/await, generators/iterators, lightweight
threads, first-class continuations, etc. This means that compilers for source
languages with such features must ceremoniously transform whole source
programs in order to target Wasm.

We present _WasmFX_ , an extension to Wasm which provides a universal target
for non-local control features via _effect handlers_ , enabling compilers to
translate such features directly into Wasm. Our extension is minimal and only
adds three main instructions for creating, suspending, and resuming
continuations. Moreover, our primitive instructions are type-safe providing
typed continuations which are well-aligned with the design principles of Wasm
whose stacks are typed. We present a formal specification of WasmFX and show
that the extension is sound. We have implemented WasmFX as an extension to the
Wasm reference interpreter and also built a prototype WasmFX extension for
Wasmtime, a production-grade Wasm engine, piggybacking on Wasmtime’s existing
fibers API. The preliminary performance results for our prototype are
encouraging, and we outline future plans to realise a native implementation.

WebAssembly, effect handlers, stack switching

##  1\. Introduction

WebAssembly (also known as Wasm) (Haas et al., 2017; Rossberg, 2019, 2023) is
a low-level virtual machine designed to be safe and fast, while being both
language- and platform-independent. A primary motivating use case is efficient
code execution on the Web, but Wasm is employed in many other environments,
such as edge and cloud computing, mobile, embedded systems, and blockchains.
Due to its universal nature and its mostly direct mapping to modern CPUs, Wasm
is now being targeted by a multitude of different languages.

However, Wasm currently lacks direct support for implementing non-local
control flow features appearing in many relevant languages, such as
generators/iterators, coroutines, futures/promises, async/await, effect
handlers, call/cc, and so forth. For some languages, such features are central
to their identity or essential for performance, e.g., to support massively
scalable concurrency. Of course, it would be possible to extend Wasm with
special support for each individual feature, but that would be at odds with
Wasm’s low-level spirit and does not scale to the next 700 non-local control
flow features. But without native Wasm support, the only option often left to
users is a global transformation of source programs, which is at odds with
modularity and often inefficient.

We propose WasmFX, a unified structured mechanism that is sufficiently general
to cover present use-cases as well as being forwards compatible with future
use-cases, while also admitting efficient implementations. WasmFX mechanism is
based on _delimited continuations_ extended with multiple _named control tags_
inspired by Plotkin and Pretnar’s effect handlers (Plotkin and Pretnar, 2009,
2013). From an operational perspective, we may view delimited continuations as
the rest of a computation from a particular point in its execution up to a
_delimiter_. From an implementation perspective, we can view them as
additional _stacks_ that execution can switch to. Tags, then, are an interface
for the possible kinds of non-local transfers of control that a computation
may perform. In addition to versatility, effect handlers are supported by a
decade’s worth of literature (Yallop, 2023), have a straightforward typing
discipline that aligns well with Wasm, and are proven to admit efficient
implementation strategies (Sivaramakrishnan et al., 2021; Xie and Leijen,
2021).

Following an overview of Wasm and WasmFX (Section 2), we make the following
contributions:

  * •

a formal specification of a minimal extension of Wasm with typed continuations
(Section 3),

  * •

a number of applications displaying the versatility of the extended language
(Section 4),

  * •

a prototype implementation based on the optimising Wasmtime compiler and a
preliminary performance evaluation comparing it to the current current state
of the art implementations of non-local control in Wasm (Section 5),

  * •

a discussion of interesting deviations from the usual implementations of typed
continuations, implementation concerns that influenced the current design, and
potential alternative designs and extensions (Section 6).

We conclude by discussing related and future work.

##  2\. Overview

###  2.1. A short Wasm primer

Wasm defines a _virtual instruction set architecture_ that closely mirrors the
instruction sets common to modern CPUs. Unlike real hardware, however, Wasm is
structured as a _stack machine_ , i.e., instead of named registers,
instructions operate on a virtual operand stack, a design that typically
achieves a more compact code representation. For example, a sequence of
instructions

⬇

(i32.const 30) (i32.const 12) (i32.add)

pushes two integers to the stack and then adds them, pushing the result. To
keep sequences of instructions more readable, the Wasm text format allows
syntactic sugar in which operands are “folded” into an instruction. For
example, the above sequence can be written as an expression:

⬇

(i32.add (i32.const 30) (i32.const 12))

_Local variables._ In addition, Wasm also provides _locals_ , which are
virtual registers accessed via dedicated instructions local.get and local.set.
For example, the of local $i can be incremented:

⬇

(local.set $i (i32.add (local.get $i) (i32.const 1)))

_Blocks._ In contrast to most other low-level code formats, control flow in
Wasm is _structured_ : it does not have arbitrary goto, but merely outward
branches to the end of a surrounding block (like break in C) or to the
beginning of a loop (like continue in C). In order to jump out of a loop, we
nest the loop immediately inside a block, for example

⬇

(block $b

(loop $l

(br_if $b (i32.ge_u (local.get $i) (i32.const 42)))

(local.set $i (i32.add (local.get $i) (i32.const 1)))

(br $l) ) )

increments the local $i in a loop. For each iteration, it checks if $i has
exceeded 42, in which case it branches to the end of the block $b. Otherwise,
it proceeds with incrementing $i and repeats by branching to the beginning of
loop $l.

_Functions._ Wasm code is organised into functions. Besides parameter and
result types, functions may declare locals. For example, the function $range
processes a given range of sequential integers:

⬇

(func $range (param $from i32) (param $to i32) (local $i i32)

(local.set $i (local.get $from))

(block $b

(loop $l

(br_if $b (i32.gt_u (local.get $i) (local.get $to)))

(call $process (local.get $i))

(local.set $i (i32.add (local.get $i) (i32.const 1)))

(br $l) ) ) )

It declares a local variable $i, initialising it to the parameter $from and
iterating up to $to, processing each value using a previously defined function
$process which just prints its argument,

⬇

(func $process (param $x i32)

(call $print (local.get $x))

such that the following call prints “10 11 12 13”:

⬇

(call $range (i32.const 10) (i32.const 13))

_Function references._ Wasm 2.0 adds simple _reference types_ , which
represent first-class pointers to functions or host resources (Rossberg,
2023). References are opaque values, such that their actual representation
cannot be inspected and their use cannot compromise memory or type safety. The
instruction ref.func $f produces a reference to a previously defined function
$f, whilst call_ref calls a function through such a reference operand. If we
define $task to be the type of functions that takes a single i32 parameter, we
can write a function $run that calls two such functions sequentially:

⬇

(type $task (func (param i32)))

(func $run (param $task1 (ref $task)) (param $task2 (ref $task))

(call_ref $task (i32.const 10) (local.get $task1))

(call_ref $task (i32.const 20) (local.get $task2)) )

We can define two functions that print given ranges of numbers and pass their
references to $run:

⬇

(func $task1 (param $x i32) (call $range (local.get $x) (i32.const 13)))

(func $task2 (param $x i32) (call $range (local.get $x) (i32.const 23)))

(func $main (call $run (ref.func $task1) (ref.func $task2)))

Executing $main prints “10 11 12 13 20 21 22 23”.

###  2.2. Continuations

Let us now turn from plain Wasm to WasmFX. A _continuation_ is a first-class
program object representing the remaining computation from a certain point in
the execution of a program. WasmFX is based on a structured notion of a
_delimited continuation_ , which is a continuation whose extent is delimited
by some _control delimiter_ , meaning it represents the remaining computation
from a certain point up to (and possibly including) its delimiter.
Intuitively, a continuation represents the current stack, whereas a delimited
continuation represents a segment of the stack. In implementations, stack
segments are often realised by allocating _multiple_ stacks in a dynamic
parent-child hierarchy.

WasmFX introduces three core instructions for manipulating delimited
continuations. First, cont.new creates a new continuation from a given
function. At the implementation level, this can be thought of as _creating a
new stack_. Next, suspend suspends the currently running computation and
reifies it into a continuation. In terms of implementation, this can be viewed
as _switching_ from the current stack to its parent. Finally, resume invokes a
given continuation in a delimited scope and declares how to handle any
suspensions that happen inside it. In an implementation, that means switching
from a parent stack to a selected child. For example, the code

⬇

(type $cont (cont $task))

(cont.new $cont (ref.func $task1))

declares the type $cont to be continuations of the function type $task, and
creates a continuation that represents a suspended computation to print a
sequence of integers.

###  2.3. Tags

A running computation suspends itself by invoking a declared _control tag_ ,
which transfers control to the nearest _handler_ for that tag (Section 2.4).
This way, control tags are similar to exceptions, with the key difference
being that execution may subsequently be resumed by the handling context.
Tags, however, are not only resumable exceptions (Steele Jr., 1990), as
handlers not only return a result to the suspended computation, but can
control when and how it is resumed.

For example, let us declare a tag $yield that allows a current computation to
signal (e.g. to a scheduler) that it is ready to relinquish control of
execution. We can then extend the function $process to yield after printing
out the given number:

⬇

(tag $yield)

(func $process (param $x i32)

(call $print (local.get $x))

(suspend $yield) )

However, suspend only creates a continuation at the invocation site of the
control tag, it does not determine how to handle it (in contrast to delimited
continuations, which do both). Thus, executing

⬇

(call $run (ref.func $task2) (ref.func $task1))

prints 0 and then traps, as there is no handler associated with $yield.

###  2.4. Handlers

How to react to $yield is specified by installing a suitable _handler_ , which
may be done each time a continuation is resumed. A handler both delimits the
scope of continuations and determines the behaviour of subsequent control
suspensions inside them. The resume instruction defines a handler in terms of
a jump table pairing control tags with labels pointing to corresponding
handler code.

Consider the following example, which treats $yield as a non-resumable
exception. We begin by setting a local variable $k to store a reference to the
continuation.

⬇

(local $k (ref $cont))

(cont.new $cont (ref.func $task1))

(local.set $k)

Next, we start an encompassing block $h, whose label serves as a join point.
Immediately inside $h, we define another block with label $on_yield, which
will serve as a label for the handling code. Recall that in Wasm, branching to
a block continues execution _after_ the block, thus the code used to handle
$yield is that immediately after the $on_yield block. Handler code receives
the suspended continuation on the stack, thus the block is annotated with a
ref $cont result type.

⬇

(block $h

(block $on_yield (result (ref $cont))

(resume $cont (on $yield $on_yield) (local.get $k))

(call $print (i32.const -2))

(br $h) )

;; $on_yield lands here

(call $print (i32.const -1))

(br $h) )

Having set both blocks up, we may resume the continuation using resume, which
points to the handling code for $yield and invokes the continuation referenced
by $k. The code that follows the resumption describes printing -2, but will
never execute since the continuation will suspend with $yield. Thus the
program prints -1 and exits. The ultimate output is the number 10, printed by
$task1, followed by -1, printed by the handling code.

The resume instruction pushes the continuation created by (suspend $yield) to
the stack before branching to a handler. For example, we may store it back
into $k and repeat the process by introducing a loop $l.

⬇

(block $h

(loop $l

(block $on_yield (result (ref $cont))

(resume $cont (on $yield $on_yield) (local.get $k))

(call $print (i32.const -2))

(br $h) )

;; $on_yield lands here, with the continuation on the stack

(local.set $k) ;; grab continuation and save it

(call $print (i32.const -1))

(br $l) ) )

This then alternates between printing numbers from $task1 and printing -1,
ultimately printing -2 once the continuation runs to its end. In terms of
implementation, this can be thought of as switching back and forth between the
main stack and the stack for $task1.

The resume instruction consumes its continuation operand, meaning a
continuation may be resumed only once — i.e., we only support _single-shot_
continuations. An attempt to resume the same continuation again will result in
a trap (an extension to support multi-shot continuations would be interesting,
but difficult to support efficiently or robustly in existing Wasm engines).
When a continuation runs to completion, i.e., when control is transferred back
to resume via a return rather than a suspension, then no further continuation
is created. The underlying child stack can be considered dead and be reclaimed
by the system.

###  2.5. Using continuations for scheduling

Handlers give us fine control over how to resume continuations. For example,
we can use them to implement lightweight threads (a primary use-case for
handlers). Let us assume a suitable interface for a queue implementation in
which we keep inactive threads. While the queue is non-empty, the scheduler
repeatedly resumes the thread at the head of the queue, by way of a loop $l
containing a block $on_yield in which the continuation is resumed. On any
$yield suspension, we branch to the instructions following the block, which
enqueue the current continuation and repeat the process:

⬇

(block $scheduler

(loop $l

(br_if $scheduler (call $queue_empty)) ;; exit if the queue is empty

(block $on_yield (result (ref $cont))

(resume $cont (on $yield $on_yield) (call $dequeue))

;; we land here when a thread finishes without suspensions

(br $l) ) ;; repeat the loop and proceed with a smaller queue

;; we land here when a thread suspends with $yield, with continuation on stack

(call $enqueue)

(br $l) ) )

Now, enqueuing tasks $task1 and $task2 as before and running the scheduler, we
get interleaved output: “10 20 11 21 12 22 23 33”.

##  3\. Language

###  3.1. Syntax

$\begin{array}[]{@{}l@{~\;}r@{~\;}c@{~\;}l@{}}\mbox{(index,
label)}\hfil~{}&\mathit{x},\mathit{l}~{}&\in\hfil~{}&\mathbb{N}\\\
\mbox{(value type)}\hfil~{}&\mathit{t}~{}&::=\hfil~{}&\mathsf{i\scriptstyle
32}\mid\mathsf{i\scriptstyle 64}\mid\mathsf{ref}~{}\mathit{f\\!t}\\\
\mbox{(function type)}\hfil~{}&\mathit{f\\!t}~{}&::=\hfil~{}&\leavevmode\hbox
to22.96pt{\vbox to9.8pt{\pgfpicture\makeatletter\hbox{\hskip
11.48137pt\lower-4.90118pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{7.48137pt}{4.90118pt}\pgfsys@lineto{-7.48137pt}{4.90118pt}\pgfsys@curveto{-9.69054pt}{4.90118pt}{-11.48137pt}{3.11035pt}{-11.48137pt}{0.90118pt}\pgfsys@lineto{-11.48137pt}{-0.90118pt}\pgfsys@curveto{-11.48137pt}{-3.11035pt}{-9.69054pt}{-4.90118pt}{-7.48137pt}{-4.90118pt}\pgfsys@lineto{7.48137pt}{-4.90118pt}\pgfsys@curveto{9.69054pt}{-4.90118pt}{11.48137pt}{-3.11035pt}{11.48137pt}{-0.90118pt}\pgfsys@lineto{11.48137pt}{0.90118pt}\pgfsys@curveto{11.48137pt}{3.11035pt}{9.69054pt}{4.90118pt}{7.48137pt}{4.90118pt}\pgfsys@closepath\pgfsys@moveto{-11.48137pt}{-4.90118pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.62779pt}{-4.0476pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathsf{cont}^{?}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}\mathit{t}^{\ast}\to\mathit{t}^{\ast}\\\
\mbox{(instruction)}\hfil~{}&\mathit{e}~{}&::=\hfil~{}&\mathit{t}\mathsf{.}\textsf{const}~{}i\mid\textsf{local.get}~{}\mathit{x}\mid\textsf{local.set}~{}\mathit{x}\mid\\\
\hfil~{}&~{}&\hfil~{}&\textsf{block}_{\mathit{f\\!t}}~{}\mathit{e}^{\ast}\mid\textsf{loop}_{\mathit{f\\!t}}~{}\mathit{e}^{\ast}\mid\textsf{br}~{}\mathit{l}\mid\textsf{br\\_if}~{}\mathit{l}\mid\\\
\hfil~{}&~{}&\hfil~{}&\textsf{call\\_ref}_{\\!\mathit{f\\!t}}\mid\textsf{ref{.}null}_{\mathit{f\\!t}}\mid\textsf{ref{.}func}~{}\mathit{x}\mid\textsf{throw}~{}\mathit{x}\mid\\\
\hfil~{}&~{}&\hfil~{}&\leavevmode\hbox to41.54pt{\vbox
to9.8pt{\pgfpicture\makeatletter\hbox{\hskip 20.77031pt\lower-4.90118pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{16.77031pt}{4.90118pt}\pgfsys@lineto{-16.77031pt}{4.90118pt}\pgfsys@curveto{-18.97948pt}{4.90118pt}{-20.77031pt}{3.11035pt}{-20.77031pt}{0.90118pt}\pgfsys@lineto{-20.77031pt}{-0.90118pt}\pgfsys@curveto{-20.77031pt}{-3.11035pt}{-18.97948pt}{-4.90118pt}{-16.77031pt}{-4.90118pt}\pgfsys@lineto{16.77031pt}{-4.90118pt}\pgfsys@curveto{18.97948pt}{-4.90118pt}{20.77031pt}{-3.11035pt}{20.77031pt}{-0.90118pt}\pgfsys@lineto{20.77031pt}{0.90118pt}\pgfsys@curveto{20.77031pt}{3.11035pt}{18.97948pt}{4.90118pt}{16.77031pt}{4.90118pt}\pgfsys@closepath\pgfsys@moveto{-20.77031pt}{-4.90118pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.91673pt}{-2.10318pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{cont{.}new}_{\\!\mathit{f\\!t}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox
to46.59pt{\vbox to11.9pt{\pgfpicture\makeatletter\hbox{\hskip
23.2936pt\lower-5.9494pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{19.2936pt}{5.9494pt}\pgfsys@lineto{-19.2936pt}{5.9494pt}\pgfsys@curveto{-21.50276pt}{5.9494pt}{-23.2936pt}{4.15857pt}{-23.2936pt}{1.9494pt}\pgfsys@lineto{-23.2936pt}{-1.9494pt}\pgfsys@curveto{-23.2936pt}{-4.15857pt}{-21.50276pt}{-5.9494pt}{-19.2936pt}{-5.9494pt}\pgfsys@lineto{19.2936pt}{-5.9494pt}\pgfsys@curveto{21.50276pt}{-5.9494pt}{23.2936pt}{-4.15857pt}{23.2936pt}{-1.9494pt}\pgfsys@lineto{23.2936pt}{1.9494pt}\pgfsys@curveto{23.2936pt}{4.15857pt}{21.50276pt}{5.9494pt}{19.2936pt}{5.9494pt}\pgfsys@closepath\pgfsys@moveto{-23.2936pt}{-5.9494pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-22.44002pt}{-3.1514pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{resume}_{\mathit{f\\!t}}~{}\mathit{h}^{\ast}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox
to45.15pt{\vbox to10.6pt{\pgfpicture\makeatletter\hbox{\hskip
22.57414pt\lower-5.29802pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{18.57414pt}{5.29802pt}\pgfsys@lineto{-18.57414pt}{5.29802pt}\pgfsys@curveto{-20.78331pt}{5.29802pt}{-22.57414pt}{3.50719pt}{-22.57414pt}{1.29802pt}\pgfsys@lineto{-22.57414pt}{-1.29802pt}\pgfsys@curveto{-22.57414pt}{-3.50719pt}{-20.78331pt}{-5.29802pt}{-18.57414pt}{-5.29802pt}\pgfsys@lineto{18.57414pt}{-5.29802pt}\pgfsys@curveto{20.78331pt}{-5.29802pt}{22.57414pt}{-3.50719pt}{22.57414pt}{-1.29802pt}\pgfsys@lineto{22.57414pt}{1.29802pt}\pgfsys@curveto{22.57414pt}{3.50719pt}{20.78331pt}{5.29802pt}{18.57414pt}{5.29802pt}\pgfsys@closepath\pgfsys@moveto{-22.57414pt}{-5.29802pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.72057pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{suspend}~{}\mathit{x}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\\\
\hfil~{}&~{}&\hfil~{}&\leavevmode\hbox to47.87pt{\vbox
to11.68pt{\pgfpicture\makeatletter\hbox{\hskip 23.93703pt\lower-5.84245pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{19.93703pt}{5.84245pt}\pgfsys@lineto{-19.93703pt}{5.84245pt}\pgfsys@curveto{-22.1462pt}{5.84245pt}{-23.93703pt}{4.05162pt}{-23.93703pt}{1.84245pt}\pgfsys@lineto{-23.93703pt}{-1.84245pt}\pgfsys@curveto{-23.93703pt}{-4.05162pt}{-22.1462pt}{-5.84245pt}{-19.93703pt}{-5.84245pt}\pgfsys@lineto{19.93703pt}{-5.84245pt}\pgfsys@curveto{22.1462pt}{-5.84245pt}{23.93703pt}{-4.05162pt}{23.93703pt}{-1.84245pt}\pgfsys@lineto{23.93703pt}{1.84245pt}\pgfsys@curveto{23.93703pt}{4.05162pt}{22.1462pt}{5.84245pt}{19.93703pt}{5.84245pt}\pgfsys@closepath\pgfsys@moveto{-23.93703pt}{-5.84245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.08345pt}{-1.95555pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{cont{.}bind}_{\\!\mathit{f\\!t},\mathit{f\\!t}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\leavevmode\hbox
to86.67pt{\vbox to11.95pt{\pgfpicture\makeatletter\hbox{\hskip
43.3336pt\lower-5.97719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{39.3336pt}{5.97719pt}\pgfsys@lineto{-39.3336pt}{5.97719pt}\pgfsys@curveto{-41.54277pt}{5.97719pt}{-43.3336pt}{4.18636pt}{-43.3336pt}{1.97719pt}\pgfsys@lineto{-43.3336pt}{-1.97719pt}\pgfsys@curveto{-43.3336pt}{-4.18636pt}{-41.54277pt}{-5.97719pt}{-39.3336pt}{-5.97719pt}\pgfsys@lineto{39.3336pt}{-5.97719pt}\pgfsys@curveto{41.54277pt}{-5.97719pt}{43.3336pt}{-4.18636pt}{43.3336pt}{-1.97719pt}\pgfsys@lineto{43.3336pt}{1.97719pt}\pgfsys@curveto{43.3336pt}{4.18636pt}{41.54277pt}{5.97719pt}{39.3336pt}{5.97719pt}\pgfsys@closepath\pgfsys@moveto{-43.3336pt}{-5.97719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-42.48003pt}{-3.12361pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{resume\\_throw}_{\\!\mathit{f\\!t}}~{}\mathit{x}~{}\mathit{h}^{\ast}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mid\\\
\leavevmode\hbox to71.79pt{\vbox
to11.71pt{\pgfpicture\makeatletter\hbox{\hskip 35.89531pt\lower-5.85358pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{31.89531pt}{5.85358pt}\pgfsys@lineto{-31.89531pt}{5.85358pt}\pgfsys@curveto{-34.10448pt}{5.85358pt}{-35.89531pt}{4.06274pt}{-35.89531pt}{1.85358pt}\pgfsys@lineto{-35.89531pt}{-1.85358pt}\pgfsys@curveto{-35.89531pt}{-4.06274pt}{-34.10448pt}{-5.85358pt}{-31.89531pt}{-5.85358pt}\pgfsys@lineto{31.89531pt}{-5.85358pt}\pgfsys@curveto{34.10448pt}{-5.85358pt}{35.89531pt}{-4.06274pt}{35.89531pt}{-1.85358pt}\pgfsys@lineto{35.89531pt}{1.85358pt}\pgfsys@curveto{35.89531pt}{4.06274pt}{34.10448pt}{5.85358pt}{31.89531pt}{5.85358pt}\pgfsys@closepath\pgfsys@moveto{-35.89531pt}{-5.85358pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.04173pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\mbox{(handler
clause)}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\hfil~{}&\leavevmode\hbox
to7.26pt{\vbox to8.65pt{\pgfpicture\makeatletter\hbox{\hskip
3.63136pt\lower-4.32579pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{-0.36864pt}{4.32579pt}\pgfsys@lineto{0.36864pt}{4.32579pt}\pgfsys@curveto{-1.84053pt}{4.32579pt}{-3.63136pt}{2.53496pt}{-3.63136pt}{0.32579pt}\pgfsys@lineto{-3.63136pt}{-0.32579pt}\pgfsys@curveto{-3.63136pt}{-2.53496pt}{-1.84053pt}{-4.32579pt}{0.36864pt}{-4.32579pt}\pgfsys@lineto{-0.36864pt}{-4.32579pt}\pgfsys@curveto{1.84053pt}{-4.32579pt}{3.63136pt}{-2.53496pt}{3.63136pt}{-0.32579pt}\pgfsys@lineto{3.63136pt}{0.32579pt}\pgfsys@curveto{3.63136pt}{2.53496pt}{1.84053pt}{4.32579pt}{-0.36864pt}{4.32579pt}\pgfsys@closepath\pgfsys@moveto{-3.63136pt}{-4.32579pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.77779pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathit{h}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}&::=\hfil~{}&\leavevmode\hbox
to26.98pt{\vbox to8.65pt{\pgfpicture\makeatletter\hbox{\hskip
13.48909pt\lower-4.32579pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{9.48909pt}{4.32579pt}\pgfsys@lineto{-9.48909pt}{4.32579pt}\pgfsys@curveto{-11.69826pt}{4.32579pt}{-13.48909pt}{2.53496pt}{-13.48909pt}{0.32579pt}\pgfsys@lineto{-13.48909pt}{-0.32579pt}\pgfsys@curveto{-13.48909pt}{-2.53496pt}{-11.69826pt}{-4.32579pt}{-9.48909pt}{-4.32579pt}\pgfsys@lineto{9.48909pt}{-4.32579pt}\pgfsys@curveto{11.69826pt}{-4.32579pt}{13.48909pt}{-2.53496pt}{13.48909pt}{-0.32579pt}\pgfsys@lineto{13.48909pt}{0.32579pt}\pgfsys@curveto{13.48909pt}{2.53496pt}{11.69826pt}{4.32579pt}{9.48909pt}{4.32579pt}\pgfsys@closepath\pgfsys@moveto{-13.48909pt}{-4.32579pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.63551pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{on}~{}\mathit{x}~{}\mathit{l}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\
\mbox{(function)}\hfil~{}&\mathit{f}~{}&::=\hfil~{}&\textsf{func}~{}\mathit{f\\!t}~{}\mathit{t}^{\ast}~{}\mathit{e}^{\ast}\\\
\mbox{(tag)}\hfil~{}&\textit{tg}~{}&::=\hfil~{}&\textsf{tag}~{}\mathit{f\\!t}\\\
\mbox{(module)}\hfil~{}&\mathit{m}~{}&::=\hfil~{}&\textsf{module}~{}\textit{tg}^{\ast}~{}\mathit{f}^{\ast}\end{array}$
Figure 1. WasmFX Syntax

In the formal definition in this paper, we focus on a minimal language
_WasmFX_ , given in Figure 1, and omit much of Wasm’s complete feature set
(Rossberg, 2023), since it is largely orthogonal to our proposal (features
omitted relative to Wasm 2.0 include additional control instructions,
arithmetics, floating point and vector types, subtyping, globals, tables, and
linear memory). Nevertheless, the proposal is compatible with the full
language, and in examples we take the liberty to assume a more complete
instruction set, e.g., obvious features such as arithmetics.

Our proposal builds on top of extensions of Wasm with function references
(Rossberg, 2022), which we extend to continuations, and with exceptions (Ahn,
2022), from which we adapt _tag_ declarations. We also use exceptions whenever
we want to abort a continuation that we do not intend to resume. Both of these
extensions are not yet in the standard, but part of proposals that are close
to reaching the final states of standardisation. Features added by our
proposal are highlighted in grey in our figures. But let us turn to the pre-
existing constructs (in black) first.

_Types._ As a low-level language, Wasm only provides primitive data types
available in hardware, such as integer numbers of different bit width, such as
$\mathsf{i\scriptstyle 32}$ and $\mathsf{i\scriptstyle 64}$. To support
function references, Wasm 2.0 introduced _reference types_ of the form
$\mathsf{ref}\mathit{f\\!t}$, where a _function type_ is of the form
$\mathit{t}_{1}^{\ast}\to\mathit{t}_{2}^{\ast}$, mapping arguments
$\mathit{t}_{1}^{\ast}$ to results $\mathit{t}_{2}^{\ast}$. In our extension,
continuations are assigned a similar type, except annotated with a
$\mathsf{cont}$ keyword.

_Instructions._ The core building block of Wasm are _instructions_. The
instruction set we consider here includes basic constants, locals, control
blocks block and loop, and basic branches br and br_if. Certain instructions
are annotated with types (type-set as subscripts) to ensure unique typing. In
examples, we denote locals, functions, tags, or labels through symbolic names
of the form $name, but these just stand in for integer de Bruijn indices that
index into respective definition lists.

We include call_ref (Rossberg, 2022), which performs a function call through a
first-class function, a null reference ref.null, and a function reference
ref.func. When calling a reference, a runtime check that it is not null
occurs; if it is, execution _traps_ , i.e. immediately aborts. Given call_ref,
a regular $\textsf{call}\;x$ instruction invoking function $x$, as available
in bare Wasm, can be viewed as a shorthand for the instruction sequence
$(\textsf{ref{.}func}\,x)\,(\textsf{call\\_ref}_{\\!\mathit{f\\!t}})$, so we
omit it from our core. After declaring an exception tag $x$, we may throw it
using the $\textsf{throw}\,x$ instruction. The exception proposal (Ahn, 2022)
also contains an instruction for handling exceptions, which we omit for
simplicity.

Next, the new instructions! As described in Section 2,
$\textsf{cont{.}new}_{\\!\mathit{f\\!t}}$ creates a new continuation (i.e., a
stack) from a function reference,
$\textsf{resume}_{\\!\mathit{f\\!t}}\,h^{\ast}$ resumes it under the specified
handlers $h^{\ast}$, and $\textsf{suspend}\,x$ suspends the current
continuation and transfers control to the handler for tag $x$.

WasmFX adds two more instructions for special purposes. The instruction
cont.bind partially applies a given continuation. Unlike partial application
for function references, this instruction requires no allocation: since a
continuation can be resumed only once, an implementation can modify it in-
place. To abort and finalise a continuation, we reuse the existing exception
mechanism: the $\textsf{resume\\_throw}\,x\,h^{\ast}$ instruction injects an
exception $x$ at the suspension site and thereby unwinds the aborted stack.
Correct code is expected to consume all continuations _linearly_ , i.e.,
either resume them or abort them explicitly with resume_throw — both will
ultimately terminate the computation and reclaim the stack. This prevents
memory leaks and triggers any user defined resource finalisation that was in
place when the continuation was suspended (e.g., through exception handlers).
Handling exception $x$ may trigger further suspensions, which are handled with
$h^{\ast}$.

_Modules._ All Wasm code is organised into modules. Each module encapsulates
local definitions, such as functions or tags, which can optionally be exported
or imported from other modules. Here, we only include the bare minimum of
concepts from modules. In particular, we assume a single global module and
omit the ability to export or import definitions, which is needed to link
multiple modules together. In particular, the full language allows
importing/exporting tags.

A tag definition includes a function type whose argument types determine the
arguments of the exception. For an exception, the result of this function type
must be empty, but when used as control tags, the result types specify values
to be transferred back upon resumption.

###  3.2. Typing

Wasm code is typed in a context $C$ recording types of locals, functions, tags
and labels. Recall that Wasm uses de Bruijn indices, thus contexts are simply
indexed lists for each namespace. We denote the type associated with label $l$
by $C_{\mathsf{label}}(l)$, and similarly for other constructs.

$\begin{array}[]{@{}l@{~\;}r@{~\;}c@{~\;}l@{}}\mbox{(contexts)}\hfil~{}&C~{}&::=\hfil~{}&\epsilon~{}|~{}C,\mathsf{func}~{}\mathit{f\\!t}~{}|~{}C,\mathsf{tag}~{}\mathit{f\\!t}~{}|~{}C,\mathsf{local}~{}\mathit{t}~{}|~{}C,\mathsf{label}~{}\mathit{t}^{\ast}\end{array}$

To each Wasm instruction we assign a function type through a judgement
$C\vdash e:t_{1}^{\ast}\to t_{2}^{\ast}$ describing the types $t_{1}^{\ast}$
of values it expects to pop off the stack and the types $t_{2}^{\ast}$ of
values it is expected to push back. The typing rules for instructions are
given in Figure 2.

$\displaystyle\boxed{C\vdash e^{\ast}:t_{1}^{\ast}\to t_{2}^{\ast}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\boxed{C\vdash\mathit{h}:t^{\ast}\mathrel{\mbox{clause}}}\hfill\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
25.2974pt\vbox{\vbox{}\hbox{\hskip-25.29738pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\epsilon:\epsilon\to\epsilon$}}}}}}$}}\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
60.15123pt\vbox{\hbox{\hskip-60.15123pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\mathit{e}_{1}:t_{1}^{\ast}\to t_{2}^{\ast}\qquad
C\vdash\mathit{e}_{2}^{\ast}:t_{2}^{\ast}\to
t_{3}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
30.3628pt\vbox{\vbox{}\hbox{\hskip-30.3628pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\mathit{e}_{1}~{}\mathit{e}_{2}^{\ast}:t_{1}^{\ast}\to
t_{3}^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.0756pt\vbox{\hbox{\hskip-25.0756pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\mathit{e}^{\ast}:t_{1}^{\ast}\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
32.01665pt\vbox{\vbox{}\hbox{\hskip-32.01665pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\mathit{e}^{\ast}:t~{}t_{1}^{\ast}\to
t~{}t_{2}^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
41.04257pt\vbox{\vbox{}\hbox{\hskip-41.04257pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash t\mathsf{.}\textsf{const}~{}i:\epsilon\to t$}}}}}}$}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
24.82773pt\vbox{\hbox{\hskip-24.82773pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{local}}(x)=t$}}}\vbox{}}}\over\hbox{\hskip
44.37215pt\vbox{\vbox{}\hbox{\hskip-44.37213pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{local.get}~{}x:\epsilon\to t$}}}}}}$}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
24.82773pt\vbox{\hbox{\hskip-24.82773pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{local}}(x)=t$}}}\vbox{}}}\over\hbox{\hskip
43.84436pt\vbox{\vbox{}\hbox{\hskip-43.84435pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{local.set}~{}x:t\to\epsilon$}}}}}}$}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
63.69795pt\vbox{\hbox{\hskip-63.69795pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}\qquad
C,\mathsf{label}\,(t_{2}^{\ast})\vdash\mathit{e}^{\ast}:\mathit{f\\!t}$}}}\vbox{}}}\over\hbox{\hskip
30.49628pt\vbox{\vbox{}\hbox{\hskip-30.49626pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{block}_{\mathit{f\\!t}}~{}\mathit{e}^{\ast}:\mathit{f\\!t}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
63.69795pt\vbox{\hbox{\hskip-63.69795pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}\qquad
C,\mathsf{label}\,(t_{1}^{\ast})\vdash\mathit{e}^{\ast}:\mathit{f\\!t}$}}}\vbox{}}}\over\hbox{\hskip
28.27405pt\vbox{\vbox{}\hbox{\hskip-28.27405pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{loop}_{\mathit{f\\!t}}~{}\mathit{e}^{\ast}:\mathit{f\\!t}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.11595pt\vbox{\hbox{\hskip-25.11594pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{label}}(l)=t^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
35.70413pt\vbox{\vbox{}\hbox{\hskip-35.70413pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{br}~{}l:t_{1}^{\ast}~{}t^{\ast}\to
t_{2}^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
25.11595pt\vbox{\hbox{\hskip-25.11594pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{label}}(l)=t^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
44.05415pt\vbox{\vbox{}\hbox{\hskip-44.05414pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{br\\_if}~{}l:t^{\ast}~{}\mathsf{i\scriptstyle 32}\to
t^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
18.21666pt\vbox{\hbox{\hskip-18.21666pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
55.1462pt\vbox{\vbox{}\hbox{\hskip-55.1462pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{call\\_ref}_{\\!\mathit{f\\!t}}:t_{1}^{\ast}~{}(\mathsf{ref}\,\mathit{f\\!t})\to
t_{2}^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
48.09962pt\vbox{\vbox{}\hbox{\hskip-48.09962pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{ref{.}null}_{\mathit{f\\!t}}:\epsilon\to(\mathsf{ref}\,\mathit{f\\!t})$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
23.80559pt\vbox{\hbox{\hskip-23.80559pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{func}}(x)=\mathit{f\\!t}$}}}\vbox{}}}\over\hbox{\hskip
53.84439pt\vbox{\vbox{}\hbox{\hskip-53.84439pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{ref{.}func}~{}x:\epsilon\to(\mathsf{ref}\,\mathit{f\\!t})$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
30.35722pt\vbox{\hbox{\hskip-30.35722pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{tag}}(x)=t^{\ast}\to\epsilon$}}}\vbox{}}}\over\hbox{\hskip
44.88817pt\vbox{\vbox{}\hbox{\hskip-44.88815pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{throw}~{}x:t_{1}^{\ast}~{}t^{\ast}\to
t_{2}^{\ast}$}}}}}}$}}\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt\leavevmode\hbox to146.63pt{\vbox
to35.71pt{\pgfpicture\makeatletter\hbox{\hskip
73.31262pt\lower-17.85358pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{69.31262pt}{17.85358pt}\pgfsys@lineto{-69.31262pt}{17.85358pt}\pgfsys@curveto{-71.52179pt}{17.85358pt}{-73.31262pt}{16.06274pt}{-73.31262pt}{13.85358pt}\pgfsys@lineto{-73.31262pt}{-13.85358pt}\pgfsys@curveto{-73.31262pt}{-16.06274pt}{-71.52179pt}{-17.85358pt}{-69.31262pt}{-17.85358pt}\pgfsys@lineto{69.31262pt}{-17.85358pt}\pgfsys@curveto{71.52179pt}{-17.85358pt}{73.31262pt}{-16.06274pt}{73.31262pt}{-13.85358pt}\pgfsys@lineto{73.31262pt}{13.85358pt}\pgfsys@curveto{73.31262pt}{16.06274pt}{71.52179pt}{17.85358pt}{69.31262pt}{17.85358pt}\pgfsys@closepath\pgfsys@moveto{-73.31262pt}{-17.85358pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-72.45905pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle$}}}\vbox{}}}\over\hbox{\hskip
72.45905pt\vbox{\vbox{}\hbox{\hskip-72.45905pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{cont{.}new}_{\mathit{f\\!t}}:(\mathsf{ref}\,\mathit{f\\!t})\to(\mathsf{ref}\,\mathsf{cont}\mathit{f\\!t})$}}}}}}$}}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\leavevmode\hbox to140.35pt{\vbox
to36.45pt{\pgfpicture\makeatletter\hbox{\hskip
70.17586pt\lower-18.22719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{66.17586pt}{18.22719pt}\pgfsys@lineto{-66.17586pt}{18.22719pt}\pgfsys@curveto{-68.38503pt}{18.22719pt}{-70.17586pt}{16.43636pt}{-70.17586pt}{14.22719pt}\pgfsys@lineto{-70.17586pt}{-14.22719pt}\pgfsys@curveto{-70.17586pt}{-16.43636pt}{-68.38503pt}{-18.22719pt}{-66.17586pt}{-18.22719pt}\pgfsys@lineto{66.17586pt}{-18.22719pt}\pgfsys@curveto{68.38503pt}{-18.22719pt}{70.17586pt}{-16.43636pt}{70.17586pt}{-14.22719pt}\pgfsys@lineto{70.17586pt}{14.22719pt}\pgfsys@curveto{70.17586pt}{16.43636pt}{68.38503pt}{18.22719pt}{66.17586pt}{18.22719pt}\pgfsys@closepath\pgfsys@moveto{-70.17586pt}{-18.22719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-69.32228pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
63.72568pt\vbox{\hbox{\hskip-63.72568pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}\qquad(C\vdash\mathit{h}:t_{2}^{\ast}\mathrel{\mbox{clause}})^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
69.32228pt\vbox{\vbox{}\hbox{\hskip-69.32227pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{resume}_{\mathit{f\\!t}}~{}\mathit{h}^{\ast}:t_{1}^{\ast}~{}(\mathsf{ref}\,\mathsf{cont}\mathit{f\\!t})\to
t_{2}^{\ast}$}}}}}}$}}}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\leavevmode\hbox to88.06pt{\vbox
to35.11pt{\pgfpicture\makeatletter\hbox{\hskip
44.02753pt\lower-17.55258pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{40.02753pt}{17.55258pt}\pgfsys@lineto{-40.02753pt}{17.55258pt}\pgfsys@curveto{-42.2367pt}{17.55258pt}{-44.02753pt}{15.76175pt}{-44.02753pt}{13.55258pt}\pgfsys@lineto{-44.02753pt}{-13.55258pt}\pgfsys@curveto{-44.02753pt}{-15.76175pt}{-42.2367pt}{-17.55258pt}{-40.02753pt}{-17.55258pt}\pgfsys@lineto{40.02753pt}{-17.55258pt}\pgfsys@curveto{42.2367pt}{-17.55258pt}{44.02753pt}{-15.76175pt}{44.02753pt}{-13.55258pt}\pgfsys@lineto{44.02753pt}{13.55258pt}\pgfsys@curveto{44.02753pt}{15.76175pt}{42.2367pt}{17.55258pt}{40.02753pt}{17.55258pt}\pgfsys@closepath\pgfsys@moveto{-44.02753pt}{-17.55258pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-43.17395pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
31.53326pt\vbox{\hbox{\hskip-31.53326pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{tag}}(x)=t_{1}^{\ast}\to t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
43.17395pt\vbox{\vbox{}\hbox{\hskip-43.17395pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{suspend}~{}\mathit{x}:t_{1}^{\ast}\to t_{2}^{\ast}$}}}}}}$}}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\leavevmode\hbox to146.51pt{\vbox
to37.68pt{\pgfpicture\makeatletter\hbox{\hskip
73.25427pt\lower-18.84245pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{69.25427pt}{18.84245pt}\pgfsys@lineto{-69.25427pt}{18.84245pt}\pgfsys@curveto{-71.46344pt}{18.84245pt}{-73.25427pt}{17.05162pt}{-73.25427pt}{14.84245pt}\pgfsys@lineto{-73.25427pt}{-14.84245pt}\pgfsys@curveto{-73.25427pt}{-17.05162pt}{-71.46344pt}{-18.84245pt}{-69.25427pt}{-18.84245pt}\pgfsys@lineto{69.25427pt}{-18.84245pt}\pgfsys@curveto{71.46344pt}{-18.84245pt}{73.25427pt}{-17.05162pt}{73.25427pt}{-14.84245pt}\pgfsys@lineto{73.25427pt}{14.84245pt}\pgfsys@curveto{73.25427pt}{17.05162pt}{71.46344pt}{18.84245pt}{69.25427pt}{18.84245pt}\pgfsys@closepath\pgfsys@moveto{-73.25427pt}{-18.84245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-72.4007pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
69.57391pt\vbox{\hbox{\hskip-69.57391pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=\mathsf{cont}\,t^{\ast}~{}t_{1}^{\ast}\to
t_{2}^{\ast}\qquad\mathit{f\\!t}^{\prime}=\mathsf{cont}\,t_{1}^{\ast}\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
72.4007pt\vbox{\vbox{}\hbox{\hskip-72.4007pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{cont{.}bind}_{\mathit{f\\!t},\mathit{f\\!t}^{\prime}}:t^{\ast}~{}(\mathsf{ref}\,\mathit{f\\!t})\to(\mathsf{ref}\,\mathit{f\\!t}^{\prime})$}}}}}}$}}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\leavevmode\hbox to209.87pt{\vbox
to36.45pt{\pgfpicture\makeatletter\hbox{\hskip
104.9365pt\lower-18.22719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{100.9365pt}{18.22719pt}\pgfsys@lineto{-100.9365pt}{18.22719pt}\pgfsys@curveto{-103.14566pt}{18.22719pt}{-104.9365pt}{16.43636pt}{-104.9365pt}{14.22719pt}\pgfsys@lineto{-104.9365pt}{-14.22719pt}\pgfsys@curveto{-104.9365pt}{-16.43636pt}{-103.14566pt}{-18.22719pt}{-100.9365pt}{-18.22719pt}\pgfsys@lineto{100.9365pt}{-18.22719pt}\pgfsys@curveto{103.14566pt}{-18.22719pt}{104.9365pt}{-16.43636pt}{104.9365pt}{-14.22719pt}\pgfsys@lineto{104.9365pt}{14.22719pt}\pgfsys@curveto{104.9365pt}{16.43636pt}{103.14566pt}{18.22719pt}{100.9365pt}{18.22719pt}\pgfsys@closepath\pgfsys@moveto{-104.9365pt}{-18.22719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-104.08292pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
104.08292pt\vbox{\hbox{\hskip-104.08292pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}\qquad
C_{\mathsf{tag}}(x)=t^{\ast}\to\epsilon\qquad(C\vdash\mathit{h}:t_{2}^{\ast}\mathrel{\mbox{clause}})^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
89.36229pt\vbox{\vbox{}\hbox{\hskip-89.36229pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{resume\\_throw}_{\\!\mathit{f\\!t}}~{}\mathit{x}~{}\mathit{h}^{\ast}:t^{\ast}~{}(\mathsf{ref}\,\mathsf{cont}\mathit{f\\!t})\to
t_{2}^{\ast}$}}}}}}$}}}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\leavevmode\hbox to205.68pt{\vbox
to34.97pt{\pgfpicture\makeatletter\hbox{\hskip
102.83951pt\lower-17.48257pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{98.83951pt}{17.48257pt}\pgfsys@lineto{-98.83951pt}{17.48257pt}\pgfsys@curveto{-101.04868pt}{17.48257pt}{-102.83951pt}{15.69174pt}{-102.83951pt}{13.48257pt}\pgfsys@lineto{-102.83951pt}{-13.48257pt}\pgfsys@curveto{-102.83951pt}{-15.69174pt}{-101.04868pt}{-17.48257pt}{-98.83951pt}{-17.48257pt}\pgfsys@lineto{98.83951pt}{-17.48257pt}\pgfsys@curveto{101.04868pt}{-17.48257pt}{102.83951pt}{-15.69174pt}{102.83951pt}{-13.48257pt}\pgfsys@lineto{102.83951pt}{13.48257pt}\pgfsys@curveto{102.83951pt}{15.69174pt}{101.04868pt}{17.48257pt}{98.83951pt}{17.48257pt}\pgfsys@closepath\pgfsys@moveto{-102.83951pt}{-17.48257pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-101.98593pt}{-6.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
101.98593pt\vbox{\hbox{\hskip-101.98593pt\hbox{\hbox{$\displaystyle\displaystyle
C_{\mathsf{tag}}(x)={t^{\prime}_{1}}^{\ast}\to{t^{\prime}_{2}}^{\ast}\qquad
C_{\mathsf{label}}(l)={t^{\prime}_{1}}^{\ast}~{}(\mathsf{ref}\,\mathsf{cont}\,({t^{\prime}_{2}}^{\ast}\to
t_{2}^{\ast}))$}}}\vbox{}}}\over\hbox{\hskip
40.07784pt\vbox{\vbox{}\hbox{\hskip-40.07782pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{on}~{}\mathit{x}~{}\mathit{l}:t_{2}^{\ast}\mathrel{\mbox{clause}}$}}}}}}$}}}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

$\displaystyle\boxed{C\vdash\textit{tg}:t_{1}^{\ast}\to t_{2}^{\ast}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt\boxed{C\vdash\mathit{f}:t_{1}^{\ast}\to t_{2}^{\ast}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt\boxed{\vdash m\
{\mathrel{\mbox{ok}}}}\hfill\penalty-10000\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
18.21666pt\vbox{\hbox{\hskip-18.21666pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
23.65182pt\vbox{\vbox{}\hbox{\hskip-23.65182pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{tag}~{}\mathit{f\\!t}:\mathit{f\\!t}$}}}}}}$}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
72.27567pt\vbox{\hbox{\hskip-72.27567pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{f\\!t}=t_{1}^{\ast}\to
t_{2}^{\ast}\qquad
C,\mathsf{local}\,t_{1}^{\ast}~{}t^{\ast}\vdash\mathit{e}^{\ast}:\epsilon\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
36.17065pt\vbox{\vbox{}\hbox{\hskip-36.17064pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{func}~{}\mathit{f\\!t}~{}t^{\ast}~{}\mathit{e}^{\ast}:\mathit{f\\!t}$}}}}}}$}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
101.15274pt\vbox{\hbox{\hskip-101.15273pt\hbox{\hbox{$\displaystyle\displaystyle
C=\mathsf{func}~{}\mathit{f\\!t}^{\ast},\mathsf{tag}~{}{\mathit{f\\!t}^{\prime}}^{\ast}\qquad(C\vdash\textit{tg}:\mathit{f\\!t}^{\prime})^{\ast}\qquad(C\vdash\mathit{f}:\mathit{f\\!t})^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
37.65776pt\vbox{\vbox{}\hbox{\hskip-37.65776pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\textsf{module}~{}\textit{tg}^{\ast}~{}\mathit{f}^{\ast}{\mathrel{\mbox{ok}}}$}}}}}}$}}$

Figure 2. Typing rules for WasmFX

The first half of the figure contains the typing rules for plain Wasm
instructions, essentially unchanged from Haas et al. (2017). We add the rules
for call_ref, ref.null, ref.func and throw taken from aforementioned
proposals, which should be self-explanatory.111The function references
proposal (Rossberg, 2022) distinguishes non-nullable references, but we omit
that distinction.

Note that br and throw are _stack-polymorphic_ : they allow arbitrary inputs
$t_{1}^{\ast}$ and outputs $t_{2}^{\ast}$ to be assumed for the stack — that
is fine, because these instructions pass control unconditionally and never
return.

Let’s turn our attention to what’s new. The cont.new instruction converts a
function reference into a continuation reference of analogous type. The resume
instruction expects a continuation of type $t_{1}^{\ast}\to t_{2}^{\ast}$ on
the stack. The stack must also hold values of types $t_{1}^{\ast}$ to be
consumed by the continuation. If the continuation terminates and hence resume
returns, it yields results of type $t_{2}^{\ast}$. The handler clauses are
assigned types matching the result type of the continuation ($t_{2}^{\ast}$).
The auxiliary judgement
$C\vdash\textsf{on}~{}\mathit{x}~{}\mathit{l}:t_{2}^{\ast}\mathrel{\mbox{clause}}$
defined at the end ensures that each label $\mathit{l}$ used to handle a tag
$\mathit{x}$ expects the corresponding tag arguments ${t^{\prime}_{1}}^{\ast}$
and a continuation reference as parameters. The continuation will produce
$t_{2}^{\ast}$ (corresponding to the type of the handler) once supplied with
the tag results ${t^{\prime}_{2}}^{\ast}$. Typing of resume_throw is
analogous, except that it expects arguments for the thrown tag $x$ instead of
the continuation parameters.

The suspend instruction behaves similarly to throw in that it expects
appropriate tag operands of type $t_{1}^{\ast}$. The main difference is that
the continuation can be subsequently resumed with values of type
$t_{2}^{\ast}$. The cont.bind instruction consumes and produces a continuation
reference, which is the same except that its leading arguments $t^{\ast}$ have
been partially applied.

Typing rules for the included module-level constructs are straightforward.
When we declare a function of a type $t_{1}^{\ast}\to t_{2}^{\ast}$, we may
declare locals of type $t^{\ast}$ in addition to the locals of type
$t_{1}^{\ast}$ that hold the function’s arguments. The context $C$ for typing
a module is constructed recursively from the types of the individual
definitions. In effect, a module is one big recursive definition.

###  3.3. Execution

The operational semantics of Wasm is given in terms of small-step reductions
between configurations consisting of the executed instruction sequence
together with a global store and the current stack frame. To concisely express
the reductions, we introduce additional syntax in Figure 3. Again, it is
largely inherited from plain Wasm (Haas et al., 2017; Rossberg, 2023); we
focus on the novelties.

$\begin{array}[]{@{}l@{~\;}r@{~\;}c@{~\;}l@{}}\mbox{(cont
address)}\hfil~{}&\mathit{k}~{}&\in\hfil~{}&\mathbb{N}\\\ \mbox{(admin
instruction)}\hfil~{}&\mathit{e}~{}&::=\hfil~{}&\dots~{}|~{}\textsf{trap}~{}|~{}\leavevmode\hbox
to43.12pt{\vbox to8.65pt{\pgfpicture\makeatletter\hbox{\hskip
21.56024pt\lower-4.32579pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{17.56024pt}{4.32579pt}\pgfsys@lineto{-17.56024pt}{4.32579pt}\pgfsys@curveto{-19.76941pt}{4.32579pt}{-21.56024pt}{2.53496pt}{-21.56024pt}{0.32579pt}\pgfsys@lineto{-21.56024pt}{-0.32579pt}\pgfsys@curveto{-21.56024pt}{-2.53496pt}{-19.76941pt}{-4.32579pt}{-17.56024pt}{-4.32579pt}\pgfsys@lineto{17.56024pt}{-4.32579pt}\pgfsys@curveto{19.76941pt}{-4.32579pt}{21.56024pt}{-2.53496pt}{21.56024pt}{-0.32579pt}\pgfsys@lineto{21.56024pt}{0.32579pt}\pgfsys@curveto{21.56024pt}{2.53496pt}{19.76941pt}{4.32579pt}{17.56024pt}{4.32579pt}\pgfsys@closepath\pgfsys@moveto{-21.56024pt}{-4.32579pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-20.70667pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{ref{.}cont}~{}\mathit{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}|{}\\\
\hfil~{}&~{}&\hfil~{}&\textsf{label}_{n}\\{\mathit{e}^{\ast}\\}~{}\mathit{e}^{\ast}~{}|~{}\textsf{frame}\\{\mathit{f\\!\\!f}\\}~{}\mathit{e}^{\ast}~{}|~{}\leavevmode\hbox
to63.44pt{\vbox to12.45pt{\pgfpicture\makeatletter\hbox{\hskip
31.72137pt\lower-6.22719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{27.72137pt}{6.22719pt}\pgfsys@lineto{-27.72137pt}{6.22719pt}\pgfsys@curveto{-29.93054pt}{6.22719pt}{-31.72137pt}{4.43636pt}{-31.72137pt}{2.22719pt}\pgfsys@lineto{-31.72137pt}{-2.22719pt}\pgfsys@curveto{-31.72137pt}{-4.43636pt}{-29.93054pt}{-6.22719pt}{-27.72137pt}{-6.22719pt}\pgfsys@lineto{27.72137pt}{-6.22719pt}\pgfsys@curveto{29.93054pt}{-6.22719pt}{31.72137pt}{-4.43636pt}{31.72137pt}{-2.22719pt}\pgfsys@lineto{31.72137pt}{2.22719pt}\pgfsys@curveto{31.72137pt}{4.43636pt}{29.93054pt}{6.22719pt}{27.72137pt}{6.22719pt}\pgfsys@closepath\pgfsys@moveto{-31.72137pt}{-6.22719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-30.8678pt}{-2.87361pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}\mathit{e}^{\ast}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\
\mbox{(value)}\hfil~{}&\mathit{v}~{}&::=\hfil~{}&\mathit{t}.\textsf{const}~{}i~{}|~{}\textsf{ref{.}null}_{\mathit{f\\!t}}~{}|~{}\textsf{ref{.}func}~{}x~{}|~{}\leavevmode\hbox
to43.12pt{\vbox to8.65pt{\pgfpicture\makeatletter\hbox{\hskip
21.56024pt\lower-4.32579pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{17.56024pt}{4.32579pt}\pgfsys@lineto{-17.56024pt}{4.32579pt}\pgfsys@curveto{-19.76941pt}{4.32579pt}{-21.56024pt}{2.53496pt}{-21.56024pt}{0.32579pt}\pgfsys@lineto{-21.56024pt}{-0.32579pt}\pgfsys@curveto{-21.56024pt}{-2.53496pt}{-19.76941pt}{-4.32579pt}{-17.56024pt}{-4.32579pt}\pgfsys@lineto{17.56024pt}{-4.32579pt}\pgfsys@curveto{19.76941pt}{-4.32579pt}{21.56024pt}{-2.53496pt}{21.56024pt}{-0.32579pt}\pgfsys@lineto{21.56024pt}{0.32579pt}\pgfsys@curveto{21.56024pt}{2.53496pt}{19.76941pt}{4.32579pt}{17.56024pt}{4.32579pt}\pgfsys@closepath\pgfsys@moveto{-21.56024pt}{-4.32579pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-20.70667pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{ref{.}cont}~{}\mathit{k}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\ \mbox{(evaluation
context)}\hfil~{}&E~{}&::=\hfil~{}&[\\_]~{}|~{}\mathit{v}^{\ast}~{}E~{}\mathit{e}^{\ast}~{}|~{}\textsf{label}_{n}\\{\mathit{e}^{\ast}\\}~{}E~{}|~{}\leavevmode\hbox
to64.16pt{\vbox to12.45pt{\pgfpicture\makeatletter\hbox{\hskip
32.07831pt\lower-6.22719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{28.07831pt}{6.22719pt}\pgfsys@lineto{-28.07831pt}{6.22719pt}\pgfsys@curveto{-30.28748pt}{6.22719pt}{-32.07831pt}{4.43636pt}{-32.07831pt}{2.22719pt}\pgfsys@lineto{-32.07831pt}{-2.22719pt}\pgfsys@curveto{-32.07831pt}{-4.43636pt}{-30.28748pt}{-6.22719pt}{-28.07831pt}{-6.22719pt}\pgfsys@lineto{28.07831pt}{-6.22719pt}\pgfsys@curveto{30.28748pt}{-6.22719pt}{32.07831pt}{-4.43636pt}{32.07831pt}{-2.22719pt}\pgfsys@lineto{32.07831pt}{2.22719pt}\pgfsys@curveto{32.07831pt}{4.43636pt}{30.28748pt}{6.22719pt}{28.07831pt}{6.22719pt}\pgfsys@closepath\pgfsys@moveto{-32.07831pt}{-6.22719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.22473pt}{-2.87361pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}E$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\ \leavevmode\hbox
to77.85pt{\vbox to11.71pt{\pgfpicture\makeatletter\hbox{\hskip
38.9231pt\lower-5.85358pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{34.9231pt}{5.85358pt}\pgfsys@lineto{-34.9231pt}{5.85358pt}\pgfsys@curveto{-37.13226pt}{5.85358pt}{-38.9231pt}{4.06274pt}{-38.9231pt}{1.85358pt}\pgfsys@lineto{-38.9231pt}{-1.85358pt}\pgfsys@curveto{-38.9231pt}{-4.06274pt}{-37.13226pt}{-5.85358pt}{-34.9231pt}{-5.85358pt}\pgfsys@lineto{34.9231pt}{-5.85358pt}\pgfsys@curveto{37.13226pt}{-5.85358pt}{38.9231pt}{-4.06274pt}{38.9231pt}{-1.85358pt}\pgfsys@lineto{38.9231pt}{1.85358pt}\pgfsys@curveto{38.9231pt}{4.06274pt}{37.13226pt}{5.85358pt}{34.9231pt}{5.85358pt}\pgfsys@closepath\pgfsys@moveto{-38.9231pt}{-5.85358pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-38.06952pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mbox{(handler
context)}$}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\hfil~{}&\leavevmode\hbox
to12.62pt{\vbox to9.75pt{\pgfpicture\makeatletter\hbox{\hskip
6.31052pt\lower-4.873pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{2.31052pt}{4.873pt}\pgfsys@lineto{-2.31052pt}{4.873pt}\pgfsys@curveto{-4.51968pt}{4.873pt}{-6.31052pt}{3.08217pt}{-6.31052pt}{0.873pt}\pgfsys@lineto{-6.31052pt}{-0.873pt}\pgfsys@curveto{-6.31052pt}{-3.08217pt}{-4.51968pt}{-4.873pt}{-2.31052pt}{-4.873pt}\pgfsys@lineto{2.31052pt}{-4.873pt}\pgfsys@curveto{4.51968pt}{-4.873pt}{6.31052pt}{-3.08217pt}{6.31052pt}{-0.873pt}\pgfsys@lineto{6.31052pt}{0.873pt}\pgfsys@curveto{6.31052pt}{3.08217pt}{4.51968pt}{4.873pt}{2.31052pt}{4.873pt}\pgfsys@closepath\pgfsys@moveto{-6.31052pt}{-4.873pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.45694pt}{-4.01942pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$E^{\mathit{x}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}&::=\hfil~{}&\leavevmode\hbox
to277.75pt{\vbox to12.45pt{\pgfpicture\makeatletter\hbox{\hskip
138.87466pt\lower-6.22719pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{134.87466pt}{6.22719pt}\pgfsys@lineto{-134.87466pt}{6.22719pt}\pgfsys@curveto{-137.08383pt}{6.22719pt}{-138.87466pt}{4.43636pt}{-138.87466pt}{2.22719pt}\pgfsys@lineto{-138.87466pt}{-2.22719pt}\pgfsys@curveto{-138.87466pt}{-4.43636pt}{-137.08383pt}{-6.22719pt}{-134.87466pt}{-6.22719pt}\pgfsys@lineto{134.87466pt}{-6.22719pt}\pgfsys@curveto{137.08383pt}{-6.22719pt}{138.87466pt}{-4.43636pt}{138.87466pt}{-2.22719pt}\pgfsys@lineto{138.87466pt}{2.22719pt}\pgfsys@curveto{138.87466pt}{4.43636pt}{137.08383pt}{6.22719pt}{134.87466pt}{6.22719pt}\pgfsys@closepath\pgfsys@moveto{-138.87466pt}{-6.22719pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-138.02109pt}{-2.87361pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$[\\_]~{}|~{}\mathit{v}^{\ast}\,E^{\mathit{x}}\mathit{e}^{\ast}~{}|~{}\textsf{label}_{n}\\{\mathit{e}^{\ast}\\!\\}\,E^{\mathit{x}}\\!\\!~{}|~{}\textsf{frame}\\{\mathit{f\\!\\!f}\\!\\}\,E^{\mathit{x}}\\!\\!~{}|~{}\textsf{handler}\\{\mathit{h}^{\ast}\\!\\}\,E^{\mathit{x}}~{}(\mathit{x}\notin\mathit{h}^{\ast})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to63.93pt{\vbox
to11.71pt{\pgfpicture\makeatletter\hbox{\hskip 31.96477pt\lower-5.85358pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{27.96477pt}{5.85358pt}\pgfsys@lineto{-27.96477pt}{5.85358pt}\pgfsys@curveto{-30.17393pt}{5.85358pt}{-31.96477pt}{4.06274pt}{-31.96477pt}{1.85358pt}\pgfsys@lineto{-31.96477pt}{-1.85358pt}\pgfsys@curveto{-31.96477pt}{-4.06274pt}{-30.17393pt}{-5.85358pt}{-27.96477pt}{-5.85358pt}\pgfsys@lineto{27.96477pt}{-5.85358pt}\pgfsys@curveto{30.17393pt}{-5.85358pt}{31.96477pt}{-4.06274pt}{31.96477pt}{-1.85358pt}\pgfsys@lineto{31.96477pt}{1.85358pt}\pgfsys@curveto{31.96477pt}{4.06274pt}{30.17393pt}{5.85358pt}{27.96477pt}{5.85358pt}\pgfsys@closepath\pgfsys@moveto{-31.96477pt}{-5.85358pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.11119pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mbox{(continuation)}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\hfil~{}&\leavevmode\hbox
to20.32pt{\vbox to7.86pt{\pgfpicture\makeatletter\hbox{\hskip
10.15915pt\lower-3.92897pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{6.15915pt}{3.92897pt}\pgfsys@lineto{-6.15915pt}{3.92897pt}\pgfsys@curveto{-8.36832pt}{3.92897pt}{-10.15915pt}{2.13814pt}{-10.15915pt}{-0.07103pt}\pgfsys@lineto{-10.15915pt}{0.07103pt}\pgfsys@curveto{-10.15915pt}{-2.13814pt}{-8.36832pt}{-3.92897pt}{-6.15915pt}{-3.92897pt}\pgfsys@lineto{6.15915pt}{-3.92897pt}\pgfsys@curveto{8.36832pt}{-3.92897pt}{10.15915pt}{-2.13814pt}{10.15915pt}{0.07103pt}\pgfsys@lineto{10.15915pt}{-0.07103pt}\pgfsys@curveto{10.15915pt}{2.13814pt}{8.36832pt}{3.92897pt}{6.15915pt}{3.92897pt}\pgfsys@closepath\pgfsys@moveto{-10.15915pt}{-3.92897pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-9.30557pt}{-3.0754pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathit{cont}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}&::=\hfil~{}&\leavevmode\hbox
to28.73pt{\vbox to12.25pt{\pgfpicture\makeatletter\hbox{\hskip
14.36264pt\lower-6.123pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{10.36264pt}{6.123pt}\pgfsys@lineto{-10.36264pt}{6.123pt}\pgfsys@curveto{-12.57181pt}{6.123pt}{-14.36264pt}{4.33217pt}{-14.36264pt}{2.123pt}\pgfsys@lineto{-14.36264pt}{-2.123pt}\pgfsys@curveto{-14.36264pt}{-4.33217pt}{-12.57181pt}{-6.123pt}{-10.36264pt}{-6.123pt}\pgfsys@lineto{10.36264pt}{-6.123pt}\pgfsys@curveto{12.57181pt}{-6.123pt}{14.36264pt}{-4.33217pt}{14.36264pt}{-2.123pt}\pgfsys@lineto{14.36264pt}{2.123pt}\pgfsys@curveto{14.36264pt}{4.33217pt}{12.57181pt}{6.123pt}{10.36264pt}{6.123pt}\pgfsys@closepath\pgfsys@moveto{-14.36264pt}{-6.123pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-13.50906pt}{-2.76942pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$E^{\mathit{x}}~{}|~{}\dagger$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\\
\mbox{(store)}\hfil~{}&\mathit{s}~{}&::=\hfil~{}&\\{\begin{array}[t]{@{}l@{}}\mathsf{func}~{}\mathit{f}^{\ast},\mathsf{tag}~{}\textit{tg}^{\ast},\leavevmode\hbox
to45.06pt{\vbox to9.16pt{\pgfpicture\makeatletter\hbox{\hskip
22.52968pt\lower-4.58035pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.825,0.825,0.825}\pgfsys@color@gray@fill{0.825}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{18.52968pt}{4.58035pt}\pgfsys@lineto{-18.52968pt}{4.58035pt}\pgfsys@curveto{-20.73885pt}{4.58035pt}{-22.52968pt}{2.78952pt}{-22.52968pt}{0.58035pt}\pgfsys@lineto{-22.52968pt}{-0.58035pt}\pgfsys@curveto{-22.52968pt}{-2.78952pt}{-20.73885pt}{-4.58035pt}{-18.52968pt}{-4.58035pt}\pgfsys@lineto{18.52968pt}{-4.58035pt}\pgfsys@curveto{20.73885pt}{-4.58035pt}{22.52968pt}{-2.78952pt}{22.52968pt}{-0.58035pt}\pgfsys@lineto{22.52968pt}{0.58035pt}\pgfsys@curveto{22.52968pt}{2.78952pt}{20.73885pt}{4.58035pt}{18.52968pt}{4.58035pt}\pgfsys@closepath\pgfsys@moveto{-22.52968pt}{-4.58035pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.6761pt}{-3.72678pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{cont}~{}\mathit{cont}^{\ast}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}\\\ \end{array}\\\
\mbox{(frame)}\hfil~{}&\mathit{f\\!\\!f}~{}&::=\hfil~{}&\\{\mathsf{local}\,\mathit{v}^{\ast}\\}\\\
\mbox{(configuration)}\hfil~{}&\mathit{c}~{}&::=\hfil~{}&\mathit{s};\mathit{f\\!\\!f};\mathit{e}^{\ast}\\\
\end{array}$ Figure 3. Syntax of WasmFX reductions

Instructions are extended into _administrative instructions_ , which represent
internal values or operators not directly expressible in Wasm’s source
instruction set. The new instruction $\textsf{ref{.}cont}~{}\mathit{k}$, which
also is a value, represents a reference to a continuation allocated at address
$\mathit{k}$ in the global store. The instruction
$\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}\mathit{e}^{\ast}$ represents
execution of $\mathit{e}^{\ast}$ under an active handler $\mathit{h}^{\ast}$.
Handlers can occur as part of evaluation contexts. For specifying the
semantics of suspension, we use a restricted version of _handler contexts_
$E^{\mathit{x}}$, which are similar to evaluation contexts, except that they
cannot contain any handlers for the given tag index $\mathit{x}$. The store
holds function and tag declarations as well as allocated continuations. A
frame consists of a sequence of local values. A continuation is given either
by an evaluation context, or by the sentinel token $\mathsf{dead}$ when it is
already used up.

$\begin{array}[]{@{}l@{~\;}c@{~\;}ll@{}}\mathit{f\\!\\!f}[x=\mathit{v}];(\textsf{local.get}\,x)\hfil~{}&\hookrightarrow\hfil~{}&\mathit{f\\!\\!f}[x=\mathit{v}];\mathit{v}\\\
\mathit{f\\!\\!f}[x=\mathit{v}];\mathit{v}^{\prime}\,(\textsf{local.set}\,x)\hfil~{}&\hookrightarrow\hfil~{}&\mathit{f\\!\\!f}[x=\mathit{v}^{\prime}];\epsilon\\\\[4.30554pt]
\mathit{v}^{n}\,(\textsf{block}_{\mathit{f\\!t}}\;\mathit{e}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&(\textsf{label}_{m}\\{\epsilon\\}\,\mathit{v}^{n}\,\mathit{e}^{\ast})&\mathrel{\mbox{if}}\mathit{f\\!t}=t_{1}^{n}\to
t_{2}^{m}\\\
\mathit{v}^{n}\,(\textsf{loop}_{\\!\mathit{f\\!t}}\;\mathit{e}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&(\textsf{label}_{n}\\{(\textsf{loop}_{\\!\mathit{f\\!t}}\;\mathit{e}^{\ast})\\}\,\mathit{v}^{n}\,\mathit{e}^{\ast})&\mathrel{\mbox{if}}\mathit{f\\!t}=t_{1}^{n}\to
t_{2}^{m}\\\\[4.30554pt]
(\textsf{label}_{n}\\{\mathit{e}^{\ast}\\}\,\mathit{v}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{\ast}\\\
(\textsf{label}_{n}\\{\mathit{e}_{1}^{\ast}\\}\,\mathit{v}^{\ast}\,\mathit{v}^{n}\,(\textsf{br}\,0)\,\mathit{e}_{2}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{n}~{}\mathit{e}_{1}^{\ast}\\\
(\textsf{label}_{n}\\{\mathit{e}_{1}^{\ast}\\}\,\mathit{v}^{\ast}\,(\textsf{br}\,l{+}1)\,\mathit{e}_{2}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{\ast}~{}(\textsf{br}~{}l)\\\
(\textsf{handler}\\{\mathit{h}^{\ast}\\}\,\mathit{v}^{\ast}\,(\textsf{br}\,l)\,\mathit{e}_{2}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{\ast}~{}(\textsf{br}~{}l)\\\\[4.30554pt]
(\mathsf{i\scriptstyle
32}.\textsf{const}\,i)~{}(\textsf{br\\_if}\,l)\hfil~{}&\hookrightarrow\hfil~{}&(\textsf{br}\,l)&\mathrel{\mbox{if}}i\neq
0\\\ (\mathsf{i\scriptstyle
32}.\textsf{const}\,i)~{}(\textsf{br\\_if}\,l)\hfil~{}&\hookrightarrow\hfil~{}&\epsilon&\mathrel{\mbox{if}}i=0\\\\[4.30554pt]
\mathit{s};\mathit{v}^{n}\,(\textsf{ref{.}func}~{}x)\,(\textsf{call\\_ref}_{\\!\mathit{f\\!t}})\hfil~{}&\hookrightarrow\hfil~{}&\lx@intercol\mathit{s};(\textsf{frame}\\{\mathsf{local}\,\mathit{v}^{n}\,(\mathsf{i\scriptstyle
32}.\textsf{const}\,0)^{k}\\}\,\mathit{e}^{\ast})\hfil\\\
\hfil~{}&\hfil~{}&\lx@intercol\mathrel{\mbox{if}}\mathit{s}_{\mathsf{func}}[x]=\mathsf{func}\;(t_{1}^{n}\to
t_{2}^{m})\;\mathit{t}^{k}\;\mathit{e}^{\ast}\hfil\\\
(\textsf{frame}\\{\mathit{f\\!\\!f}\\}\,E[\mathit{e}^{\ast}])\hfil~{}&\hookrightarrow\hfil~{}&(\textsf{frame}\\{\mathit{f\\!\\!f}^{\prime}\\}\,E[{\mathit{e}^{\prime}}^{\ast}])\\\
\hfil~{}&\hfil~{}&\mathrel{\mbox{if}}\mathit{f\\!\\!f};\mathit{e}^{\ast}\hookrightarrow\mathit{f\\!\\!f}^{\prime};{\mathit{e}^{\prime}}^{\ast}\\\
(\textsf{frame}\\{\mathit{f\\!\\!f}\\}\,\mathit{v}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{\ast}\\\
\mathit{s};(\textsf{frame}\\{\mathit{f\\!\\!f}\\}\,E[\mathit{v}^{n}\,(\textsf{throw}\,\mathit{x})])\hfil~{}&\hookrightarrow\hfil~{}&\mathit{s};\mathit{v}^{n}\,(\textsf{throw}\,x)\\\
\hfil~{}&\hfil~{}&\mathrel{\mbox{if}}\mathit{s}_{\mathsf{tag}}[x]=\mathit{t}^{n}\to\mathit{t}^{\ast}\\\\[4.30554pt]
\mathit{s};(\textsf{ref{.}func}~{}x)\,(\textsf{cont{.}new}_{\\!\mathit{f\\!t}})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{s}[+\mathit{k}=E];(\textsf{ref{.}cont}~{}\mathit{k})\\\
\hfil~{}&\hfil~{}&\lx@intercol\mbox{where~{}}E=[\\_]~{}(\textsf{ref{.}func}~{}x)~{}(\textsf{call\\_ref}_{\\!\mathit{f\\!t}})\hfil\\\
\mathit{s}[\mathit{k}=E];\mathit{v}^{n}\,(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{resume}_{\mathit{f\\!t}}~{}\mathit{h}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\lx@intercol\mathit{s}[\mathit{k}=\dagger];\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}E[\mathit{v}^{n}]\hfil\\\
\hfil~{}&\hfil~{}&\lx@intercol\mathrel{\mbox{if}}\mathit{f\\!t}=\mathsf{cont}~{}\mathit{t}_{1}^{n}\to\mathit{t}_{2}^{\ast}\hfil\\\\[4.30554pt]
(\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}\mathit{v}^{*})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{v}^{*}\\\
\mathit{s};(\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}E^{\mathit{x}}[\mathit{v}^{n}~{}(\textsf{suspend}~{}\mathit{x})])\hfil~{}&\hookrightarrow\hfil~{}&\lx@intercol\mathit{s}[+\mathit{k}=E^{\mathit{x}}];\mathit{v}^{n}\;(\textsf{ref{.}cont}~{}\mathit{k})~{}(\textsf{br}~{}\mathit{l})\hfil\\\
\hfil~{}&\hfil~{}&\lx@intercol\mathrel{\mbox{if}}\mathit{h}^{\ast}=\mathit{h}_{1}^{\ast}~{}(\textsf{on}~{}\mathit{x}~{}\mathit{l})~{}\mathit{h}_{2}^{\ast}\land\mathit{x}\notin\mathit{h}_{1}^{\ast}\hfil\\\
\hfil~{}&\hfil~{}&\lx@intercol\land\;\mathit{s}_{\mathsf{tag}}[\mathit{x}]=\mathit{t}_{1}^{n}\to\mathit{t}_{2}^{\ast}\hfil\\\\[4.30554pt]
\mathit{s}[\mathit{k}=E];\mathit{v}^{n}\,(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{cont{.}bind}_{\mathit{f\\!t},\mathit{f\\!t}^{\prime}})\hfil~{}&\hookrightarrow\hfil~{}&\lx@intercol\mathit{s}[\mathit{k}=\dagger,+\mathit{k}^{\prime}=E[\mathit{v}^{n}\,\\_]];(\textsf{ref{.}cont}~{}\mathit{k}^{\prime})\hfil\\\
\hfil~{}&\hfil~{}&\lx@intercol\begin{array}[t]{@{}l@{~}l@{~}c@{~}l@{}}\mathrel{\mbox{if}}\hfil~{}&\mathit{f\\!t}\hfil~{}&=\hfil~{}&\mathsf{cont}~{}\mathit{t}^{n}\;\mathit{t}_{1}^{m}\to\mathit{t}_{2}^{\ast}\\\
\land\hfil~{}&\mathit{f\\!t}^{\prime}\hfil~{}&=\hfil~{}&\mathsf{cont}~{}\mathit{t}_{1}^{m}\to\mathit{t}_{2}^{\ast}\\\
\end{array}\hfil\\\\[4.30554pt]
\mathit{s}[\mathit{k}=E];\mathit{v}^{n}\,(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{resume\\_throw}_{\\!\mathit{f\\!t}}~{}x~{}\mathit{h}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\lx@intercol\mathit{s}[\mathit{k}=\dagger];\textsf{handler}\\{\mathit{h}^{\ast}\\}~{}E[\mathit{v}^{n}~{}(\textsf{throw}~{}x)]\hfil\\\
<EMAIL_ADDRESS>\mathit{s}[\mathit{k}=\dagger];(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{resume}_{\mathit{f\\!t}}~{}\mathit{h}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{s}[\mathit{k}=\dagger];\textsf{trap}\\\
\mathit{s}[\mathit{k}=\dagger];(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{cont{.}bind}_{\mathit{f\\!t},\mathit{f\\!t}^{\prime}})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{s}[\mathit{k}=\dagger];\textsf{trap}\\\
\mathit{s}[\mathit{k}=\dagger];(\textsf{ref{.}cont}~{}\mathit{k})\,(\textsf{resume\\_throw}_{\\!\mathit{f\\!t}}~{}x~{}\mathit{h}^{\ast})\hfil~{}&\hookrightarrow\hfil~{}&\mathit{s}[\mathit{k}=\dagger];\textsf{trap}\\\
\end{array}$ Figure 4. WasmFX Reduction

The reduction rules are given in Figure 4 and are of the form
$\mathit{s}_{1};\mathit{f\\!\\!f}_{1};\mathit{e}_{1}^{\ast}\hookrightarrow\mathit{s}_{2};\mathit{f\\!\\!f}_{2};\mathit{e}_{2}^{\ast}$.
For brevity, we omit the store when it is not used; the same convention
applies to frames. We write $\mathit{f\\!\\!f}[x=\mathit{v}]$ to denote the
same frame as $\mathit{f\\!\\!f}$ but with the value $\mathit{v}$ assigned to
local $x$. Similarly, $\mathit{s}[\mathit{k}=E]$ binds the continuation $k$ to
$E$ in store $\mathit{s}$, and $\mathit{s}[+\mathit{k}=E]$ is the _extension_
of $\mathit{s}$ with a fresh continuation $k$.

The first set of rules involving locals, blocks, labels and branches, is once
more inherited from plain Wasm, and we refer to Haas et al. (2017) for
details. The only change here is that we allow branches to cross handlers,
which uninstalls the handler. A call to a function introduces a suitable frame
encapsulating the function body. Evaluation is performed inside a frame until
it either results in values or throws.

The cont.new instruction extends the store with a fresh continuation that will
immediately invoke the referenced function when it is resumed.

A continuation is resumed by installing a handler and inside it,
reestablishing the evaluation context that represents the continuation. At the
same time, the continuation is marked dead, so it cannot be resumed twice. A
handler is removed once evaluation terminates with values. If it suspends with
a tag for the handler, and there is no intervening handler for it in-between
(expressed by the $E^{\mathit{x}}$ context), then the appropriate number of
tag arguments are extracted and the rest of the evaluation context up to the
handler is reified into a freshly allocated continuation, arguments and
continuation are pushed to the stack, and execution branches to the label
associated with the tag.

Partially applying a continuation with cont.bind discards the old continuation
in the store and adds a new one with the evaluation context extended with the
supplied arguments.

Executing resume_throw also installs a handler, reestablishes the
continuation’s evaluation context, and marks the continuation dead. However,
it inserts a throw instruction into the hole.

Finally, any attempt to consume a continuation that is already dead causes a
trap.

###  3.4. Soundness

Type Preservation for Wasm (Haas et al., 2017; Watt et al., 2021) extends to
the new instruction set. To prove this, we need to formulate adequate typing
rules for the new administrative instructions:

$\displaystyle\displaystyle{\hbox{\hskip
33.2055pt\vbox{\hbox{\hskip-33.2055pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{s}\vdash\mathit{s}_{\mathsf{cont}}(\mathit{k}):t_{1}^{\ast}\to
t_{2}^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
75.89447pt\vbox{\vbox{}\hbox{\hskip-75.89445pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{s};C\vdash\textsf{ref{.}cont}~{}\mathit{k}:\epsilon\to(\mathsf{ref}~{}\mathsf{cont}~{}t_{1}^{\ast}\to
t_{2}^{\ast})$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
70.81973pt\vbox{\hbox{\hskip-70.81973pt\hbox{\hbox{$\displaystyle\displaystyle(C^{\circ}\vdash\mathit{h}:t^{\ast}\mathrel{\mbox{clause}})^{\ast}\qquad
C^{\circ}\vdash\mathit{e}^{\ast}:\epsilon\to
t^{\ast}$}}}\vbox{}}}\over\hbox{\hskip
51.70236pt\vbox{\vbox{}\hbox{\hskip-51.70235pt\hbox{\hbox{$\displaystyle\displaystyle
C\vdash\textsf{handler}\\{\mathit{h}^{\ast}\\}\,\mathit{e}^{\ast}:\epsilon\to
t^{\ast}$}}}}}}$

Here, $C^{\circ}$ is the same as $C$ but with all bindings for locals and
labels removed. This restriction is necessary, because Wasm does not have
closures. Without this restriction, we would allow dangling occurrences of
local or label names to enter the store in the reduction rule for suspend. The
restriction is preserved because all continuations start, via cont.new, from a
separate function.

With that, and a couple of additional auxiliary judgements not shown here, we
get:

###### Theorem 3.1 (Preservation).

If $\vdash\mathit{s};\mathit{f\\!\\!f};\mathit{e}^{\ast}:t^{\ast}$ and
$\mathit{s};\mathit{f\\!\\!f};\mathit{e}^{\ast}\hookrightarrow\mathit{s}^{\prime};\mathit{f\\!\\!f}^{\prime}\\!;{\mathit{e}^{\prime}}^{\ast}$,
then
$\vdash\mathit{s}^{\prime};\mathit{f\\!\\!f}^{\prime}\\!;{\mathit{e}^{\prime}}^{\ast}:t^{\ast}$.

For Progress, we need to define what the legal _results_ of a computation are,
namely, either multiple values, a trap, or an unhandled exception or
suspension:

$\begin{array}[]{@{}l@{~\;}r@{~\;}c@{~\;}l@{}}\mbox{(result)}\hfil~{}&r~{}&::=\hfil~{}&\mathit{v}^{\ast}~{}|~{}\textsf{trap}~{}|~{}E[(\textsf{throw}~{}\mathit{x})]~{}|~{}E^{\mathit{x}}[(\textsf{suspend}~{}\mathit{x})]\\\
\end{array}$

Then we can prove, in the usual manner:

###### Theorem 3.2 (Progress).

If $\vdash\mathit{s};\mathit{f\\!\\!f};\mathit{e}^{\ast}:t^{\ast}$, then
either $\mathit{e}^{\ast}=r$, or
$\mathit{s};\mathit{f\\!\\!f};\mathit{e}^{\ast}\hookrightarrow\mathit{s}^{\prime};\mathit{f\\!\\!f}^{\prime}\\!;{\mathit{e}^{\prime}}^{\ast}$.

##  4\. Applications

###  4.1. Generators

When using generators, we deal with two concurrent computations. One
sequentially consumes values while the other one produces (or yields) them one
at a time. We can capture the production of values with a single tag $gen
which carries the produced value as a parameter:

⬇

(tag $gen (param i32))

Then, we can write the following function which indefinitely produces natural
numbers from 0:

⬇

(func $naturals

(local $n i32) ;; zero-initialised

(loop $l

(suspend $gen (local.get $n))

(local.set $n (i32.add (local.get $n) (i32.const 1)))

(br $l) ) )

Produced values can be consumed with a handler for $gen, for example one that
sums up values until one exceeds $upto:

⬇

(func $sum_until (param $upto i32) (result i32)

(local $v i32)

(local $sum i32)

(local $k (ref $cont))

(local.set $k (cont.new (ref.func $naturals)))

(loop $l

(block $on_yield (result i32 (ref $cont))

(resume $cont (on $yield $on_yield) (local.get $k))

(unreachable) ;; $naturals never returns, so we can never get here

) ;; $on_yield (result i32 (ref $cont))

(local.set $k) ;; store the new continuation for later resumption

(local.set $v) ;; store the produced value

(local.set $sum (i32.add (local.get $sum) (local.get $v))) ;; add $v to $sum

(br_if $l (i32.lt_u (local.get $v) (local.get $upto)))

(local.get $sum) )

Now, although the function $naturals is an infinite loop, we get 5050 by
calling:

⬇

(call $sum_until (i32.const 101))

Using a global table of active generators, we can implement a more ergonomic
interface to generators, in which a programmer does not use handlers directly,
but interacts solely through functions $init, which takes a continuation and
returns a unique identifier, and $next, which takes the identifier and returns
the next value.

###  4.2. Dynamic lightweight threads

We can make our lightweight threads functionality from Section 2 considerably
more expressive by allowing new threads to be forked dynamically. For that, we
declare a new $fork tag that takes a continuation as a parameter and (like
$yield) returns no result.

⬇

(tag $fork (param (ref $cont)))

Thus, instead of manually enqueuing the threads, we can use the $fork tag:

⬇

(suspend $fork (cont.new $cont (ref.func $task1)))

(suspend $fork (cont.new $cont (ref.func $task2)))

Of course, we can obtain much more involved behaviour, as threads themselves
may fork new ones. The scheduler only needs to be extended with a new clause
for handling the $fork tag:

⬇

(func $scheduler (param $nextk (ref $cont))

(loop $l

(if (ref.is_null (local.get $nextk)) (then (return)))

(block $on_yield (result (ref $cont))

(block $on_fork (result (ref $cont) (ref $cont))

(resume $cont (on $yield $on_yield) (on $fork $on_fork) (local.get $nextk))

(local.set $nextk (call $dequeue))

(br $l) )

;; $on_fork, forkee and forker continuations on stack

(local.set $nextk) ;; forker is next

(call $enqueue) ;; queue up forkee

(br $l) )

;; $on_yield, yielder continuation on stack

(call $enqueue) ;; queue it up

(local.set $nextk (call $dequeue)) ;; take next

(br $l) ) )

When handling a fork, there are two continuations on the stack. On top, we
have the suspended continuation, and below it, the newly created thread that
was given as an argument to $fork. We have three threads to choose from for
the next step: the suspended active thread, the newly created thread, and the
first inactive thread waiting in the queue. In the example above, we continue
running the active thread and enqueue the new one, but we could easily adopt a
different strategy.

###  4.3. Promises

We can adapt a similar approach for async/await-style _promises_ (Bierman et
al., 2012), in which one asynchronously runs a function that will compute a
value, obtains an opaque promise, and then _awaits_ that promise once the
value is required. It is important to note that the function does not simply
return the value, but uses it to _fulfill_ a promise. If we represent promises
with $\mathsf{i\scriptstyle 32}$ identifiers, we can define a type of
continuations that take and fulfill them:

⬇

(type $i32_func (func (param i32)))

(type $i32_cont (cont $i32_func))

We interface promises through four tags: $yield asynchronously yields as
before, $fulfill takes a promise and a value to fulfill it with, $await takes
a promise, awaits its fulfilled value, and returns it, and $async returns a
new promise that will be fulfilled by the given continuation. We represent
values with $\mathsf{i\scriptstyle 64}$ in order to easily distinguish them
from promise identifiers.

⬇

(tag $yield)

(tag $fulfill (param i32) (param i64))

(tag $await (param i32) (result i64))

(tag $async (param (ref $i32_cont)) (result i32))

Next, assume an external implementation of promises through externally defined
functions $prom_* accessing a table that keeps a (perhaps unfulfilled) value
for each promise and a continuation that awaits its result. Then, we can write
a handler similar to the one for light-weight threads, except also handling
the three additional tags. We describe the body of the four handlers; the
overall structure mirrors that of the other examples.

When handling $fulfill, the stack contains the suspended continuation, the
value, and the promise to be fulfilled. We keep the first as the active
continuation $nextk and pass the other two to the external implementation,
which returns the continuation awaiting the promise if any. If there is none,
we do nothing, otherwise, we enqueue it as it is now unblocked.

⬇

(local.set $nextk)

(local.set $waiterk (call $prom_fulfill)) ;; the call pops two operands off
the stack

(if (i32.eqz (ref.is_null (local.get $waiterk))) ;; i32.eqz encodes negation

(then (call $enqueue (local.get $waiterk))) )

When handling $await, the stack contains the current continuation and the
promise it is waiting for. We first call the external function and check if
the promise has already been fulfilled. If it has, then we can partially apply
the current continuation and resume it. Otherwise, we attach the continuation
to the promise and continue with the next thread in the queue.

⬇

(local.set $waiterk) (local.set $prom)

(if (call $prom_fulfilled (local.get $prom))

(then

(local.set $nextk

(cont.bind $i32_cont $cont (call $prom_value (local.get $prom)) (local.get
$waiterk)) ))

(else

(call $prom_await (local.get $prom) (local.get $waiterk))

(local.set $nextk (call $dequeue)) ))

Finally, when handling $async, the stack contains the current continuation
waiting for the new promise, and the asynchronous task that is meant to
fulfill it. We create a new promise and pass it to both continuations; we
enqueue the suspended continuation and run the new one.

⬇

(local.set $waiterk) (local.set $asynck)

(local.set $prom (call $prom_new))

(call $enqueue (cont.bind $i32_cont $cont (local.get $prom) (local.get
$waiterk)))

(local.set $nextk (cont.bind $i32_cont $cont (local.get $prom) (local.get
$asynck)))

###  4.4. Actors

As an example of handler composition, we consider Erlang-style _actors_
(Armstrong et al., 1996). These are independent processes that can spawn new
actors and communicate to each other through mailboxes. We represent their
interface through four tags: $send sends a message to a given mailbox,
$receive receives the next incoming message, $spawn creates a new actor from a
given continuation and returns its address, and $self returns the address of
the current process. Like previously, we use $\mathsf{i\scriptstyle 32}$ for
addresses and $\mathsf{i\scriptstyle 64}$ for messages.

⬇

(tag $send (param i64 i32))

(tag $self (result i32))

(tag $spawn (param (ref $cont)) (result i32))

(tag $recv (result i64))

To provide suitable type annotations, we need to define a number of additional
continuation types:

⬇

(type $i64_func (func (param i64))) (type $i64_cont (cont $i64_func))

(type $i64_cont_func (func (param i64 (ref $cont)))) (type $i64_cont_cont
(cont $i64_cont_func))

(type $cont_func (func (param (ref $cont)))) (type $cont_cont (cont
$cont_func))

As an example, here is a function that receives a message and forwards it to
actor $p:

⬇

(func $forward (param $p i32)

(local $s i64)

(local.set $s (suspend $recv))

(suspend $send (local.get $s) (local.get $p)) )

And another that creates a chain of $n actors that forwards a message $m to
the originating actor:

⬇

(func $chain (param $n i32) (param $m i64)

(local $p i32) ;; mailbox of the currently last actor in the chain

(local.set $p (suspend $self))

(loop $l

(if (i32.eqz (local.get $n))

(then (suspend $send (local.get $m) (local.get $p))) ;; once done, send $m to
the last actor

(else

(cont.new $i32_cont (ref.func $forward)) ;; set up a new forwarding
continuation

(cont.bind $i32_cont $cont (local.get $p) ;; pass it the address of the
currently last actor

(local.set $p (suspend $spawn)) ;; spawn a new actor and set it as the
currently last

(local.set $n (i32.sub (local.get $n) (i32.const 1))) ;; decrement $n and
repeat

(br $l) ) ) ) ) )

If an actor tries to receive a message, but its mailbox is empty, it must
wait. The easiest way to implement this is by using threads as described in
Section 4.2. We assume an interface to mailboxes through externally defined
functions $mb_* and define a main function $act, which takes a continuation
$k, creates a new mailbox and passes its address and the continuation to an
auxiliary function $act_aux.

⬇

(func $act (param $k (ref $cont))

(call $act_aux (call $mb_new) (local.get $k)))

The function $act_aux stores the mailbox address in a local $mine and resumes
the continuation under a handler with the handler clauses as follows:

On $self, we take the existing continuation expecting the address, partially
bind it to $mine, and store it as the next resumption.

⬇

(local.set $ik)

(local.set $nextk (cont.bind $i32_cont $cont (local.get $mine) (local.get
$ik)))

On spawning a new actor $you, we create a new mailbox, store its address in
$yours, fork a new thread to run $you using $act_aux again, and pass the new
address back to the continuation $ik.

⬇

(local.set $ik) (local.set $you) (local.set $yours (call $mb_new))

(suspend $fork

(cont.bind $i64_cont_cont $cont (local.get $yours) (local.get $you)

(cont.new $i64_cont_cont (ref.func $act_aux)) ) )

(local.set $nextk (cont.bind $i32_cont $cont (local.get $yours) (local.get
$ik)))

On sending a message, we simply pass the tag argument (message) to the
external function and resume:

⬇

(local.set $k)

(call $mb_send)

(local.set $nextk (local.get $k))

Finally, on receiving a message, we first block until the mailbox $mine is no
longer empty. Repeatedly, we check if it is empty, and if it is, we yield the
control to other actors and try again later. Once the mailbox is non-empty, we
read the message and pass it to the continuation $ik:

⬇

(local.set $ik)

(loop $blocked

(if (call $mb_empty (local.get $mine))

(then (suspend $yield) (br $blocked)) ) )

(local.set $nextk (cont.bind $i64_cont $cont (call $mb_recv (local.get $mine))
(local.get $ik)))

Note that in the clauses for $spawn and $recv, we use tags $yield and $fork
that provide an interface to threads and need to be handled. To run the actor
$p, we first need to pass it to the $act handler. This needs to be converted
to a continuation so that it can be further passed to the $scheduler handler
as defined in Section 4.2.

⬇

(func $run_actor (param $p (ref $cont))

(cont.new $cont_cont (ref.func $act)) ;; convert the $act function into a
continuation

(cont.bind $cont_cont $cont (local.get $p)) ;; partially apply the
continuation to actor $a

(call $scheduler) ) ;; handle fork & yield in the applied continuation

##  5\. Implementation

We have implemented the full instruction set of WasmFX as an extension to the
Wasm reference interpreter. Moreover, we have implemented a prototype of
WasmFX in Wasmtime, a production-grade Wasm engine. In this section we
describe the latter implementation. Wasmtime features an optimising just-in-
time compiler for Wasm modules. We classify our implementation in Wasmtime as
a prototype for three reasons. Firstly, at the time of writing we support only
WasmFX programs on x86-64, whereas Wasmtime supports a much wider range of
architectures including ARM64, ARM, RISC-V64, s390x, and x86. Secondly, we
cannot implement resume_throw as Wasmtime does not yet support exceptions,
thus we currently support only the other four instructions. We plan to
implement resume_throw once support for exceptions lands in Wasmtime. Thirdly,
and most importantly, our implementation piggybacks on the existing fiber API
in Wasmtime (Crichton, 2021), which enables the Wasm host to run functions
asynchronously. Targeting the fiber API allows us to quickly prototype the
design in a production-grade setting, and its implementation integrates well
with standard debugging and profiling tools as it already emits the necessary
information to construct DWARF unwind tables. On the other hand, it has the
problem that fibers exist _outside_ the Wasm world, meaning that every
interaction with a fiber necessarily needs to call out to the host, a
relatively expensive operation. Moreover, it requires us to _box_ continuation
parameters and results, because the host function cannot be polymorphic over
continuation types.

_The Fiber API._ Figure 5 shows the interface to the Wasmtime fiber API. The
FiberStack::new method allocates a new stack of minimum size bytes. Figure 6
details the actual stack layout. The first 32 bytes are reserved for the
header. The initial 8 bytes are used to store the payload for resumes,
suspends, and returns. The next 8 bytes are used for the local stack pointer.
The next 8 bytes store the pointer to the parent fiber. These bytes were added
by us to implement the dynamic scoping of handlers. Finally, there is a guard
page to detect stack overflow. We also extend the instance context of Wasmtime
with an additional field to keep track of the currently executing fiber such
that we can retrieve its pointer when resuming and suspending.

The key entity is the Fiber structure, which is parameterised by three type
variables for resume payloads (R), suspend payloads (S), and return values
(A). We instantiate R and A to the unit type, because we store payloads
directly in the bespoke buffer on the fiber stack. The reason for using this
approach is that we do not a priori which types the user provided program will
use. Consequently, we are forced to box everything that crosses the Wasm-Host
boundary and vice versa. Meanwhile, we instantiate S to u32 as we use it to
communicate index of the control tag supplied to suspend.

Fiber::new takes a fresh FiberStack, and the suspended computation to run on
the said stack. It installs the launchpad code necessary to run the
computation when the initial Fiber::resume occurs. The Fiber::resume method
suspends the currently executing fiber and continues execution of the provided
Fiber. The Suspend::suspend method works similarly.

_Stack Switching._ Stack switching in the fibers library is implemented in
x86_64 assembly code. Figure 5 shows the stack switching routine. It
pessimistically saves any necessary registers to the stack. The pointer to the
stack is passed in register rdi, from which we load the saved rsp (local stack
pointer); subsequently we store the current stack pointer in the same header
spot. The actual stack swapping occurs by overriding the value of rsp with the
previously loaded value. After restoring saved registers, the top of the stack
holds the return location saved when the fiber was suspended; a return
instruction is executed, continuing execution from the suspended point.

_Compiling WasmFX to Wasmtime Fiber._ The translation from WasmFX continuation
instructions to Wasmtime fibers is mostly straightforward. We implement each
instruction as a _libcall_ which calls from compiled Wasm code to Wasmtime
runtime code. We realise each instruction as follows.

We map cont.new to Fiber::new. We box the resulting fiber so we can null out
the continuation object once it has been supplied to resume. The suspended
computation merely marshals values to the provided Wasm function. For
cont.bind we write the payload directly to the heap-allocated result cell and
return a new continuation object (containing the same fiber reference).

The handler clauses on the resume instruction get compiled to the core Wasm
instruction br_table, which is a jump table. The table jumps to handler blocks
for tags that are handled, and re-suspends to the parent (if any) for tags
that are not. The libcall for resume boxes the arguments, sets the parent
pointer of the fiber to the currently executing fiber, and invokes
Fiber::resume. We return the result of this function to the handler in Wasm,
distinguishing return from suspend with a sentinel value.

The libcall for suspend replaces the current stack pointer in the context with
its parent. It then writes the payload, including the name of the tag, to its
result cell and transfers control.

⬇

trait FiberStack {

fn new(size: usize) -> io::Result<Self>

}

trait<R, S, A> Fiber<R, S, A> {

fn new(stack: FiberStack,

func: FnOnce(R, &S<R, S, A>) -> A

fn resume(&self, val: R) -> Result<A, S>

}

trait Suspend<R, S, A> {

fn suspend(&self, S) -> R

}

(a) The Essence of the Wasmtime Fiber API

⬇

.wasmtime_fiber_switch:

// Save callee-saved registers

push …

// Load resume pointer, save previous

mov rax, -0x20[rdi]

mov -0x20[rdi], rsp

// Swap stacks

mov rsp, rax

pop … // restore callee-saved registers

ret

(b) Fiber Switching x86_64 Assembly Code

Figure 5. Wasmtime Fiber API and Context Switching Code 0x0000guard
page0x1000$\cdots$actual native stack space to use0xAfe08 bytes padding16-byte
aligned0xAfe8*const u8parent stack pointer0xAff0*const u8last sp to resume
from0xAff8&Cell<RunResult>where to store results0xB000top of stack Figure 6.
Fiber Stack Layout

###  5.1. Experiments

We perform some preliminary experiments to gather data to obtain insight into
our prototype implementation of WasmFX fares against the state-of-the-art. We
perform two experiments: 1) we measure the performance characteristics, i.e.
binary size, run time, and memory performance on a micro benchmark provided by
Leijen and Sivaramakrishnan (2021); 2) we compare the binary size of programs
produced by the TinyGo compiler with and without WasmFX as a backend. The
experiments are conducted on an AMD Ryzen 9 5900X 12-core 3.75GHz CPU with 32
GB memory powered machine running Ubuntu 22.04 LTS.

The first benchmark, provided by Leijen and Sivaramakrishnan (2021), simulates
a web server workload. It is written in C. The benchmark runs 10000 coroutines
concurrently (each intended to represent a unique http request), each
coroutine simply suspends to simulate I/O and then performs some stack-heavy
computation. The benchmark performs 10 million requests, meaning it spawns 10
million coroutines in total.

We run the benchmark in three ways: 1) using WasmFX; 2) Asyncify; and 3) a
bespoke hand-written state machine transformation of the benchmark program. It
is worth noting that the WasmFX and Asyncify approaches require no programmer
intervention, whereas the latter approach requires a complete rewrite of the
program. We run each benchmark program five times and measure the size of the
compiled Wasm binary, median wall clock time, and maximum physical memory
usage. We use Wasmtime to run each benchmark. To compile the C program to Wasm
we use clang version 14 with optimisation flag -O3 and the binaryen toolchain
version 105. For the experiments, we modify the Wasmtime implementation of
WasmFX to allocate fiber stacks using malloc instead of mmap as this is the
memory allocation scheme used by the Asyncify and hand-written program. In
particular, we use the optimised mimalloc allocator (Leijen et al., 2019)
rather than the default system allocator. Finally, WasmFX and Asyncify
allocate stacks with the fixed size of 4096 bytes.

Figure 7 reports the results for the first benchmark. The space performance of
WasmFX is on par with the state-of-the-art (optimised Asyncify) in both binary
file size and memory usage. Though, the binary file size is better when
compiling with WasmFX. However, the run time performance of the WasmFX
implementation is more than a factor of four slower. Performance analysis
indicates that about 37% of samples are spent in wasmtime_fiber_switch (Figure
5) with an additional 33% of samples in the Rust libcall code supporting the
continuation instructions, which are both highly unoptimised. Saving
registers, calling between the host and Wasm, and boxing values likely
accounts for much of this cost. As expected the bespoke implementation is
fastest and exhibits the best memory utilisation of all. The primary reason
for the space efficiency is that it does not allocate 4096 bytes stack for
each coroutine.

| Binary Size | Wall Time | Memory Usage
---|---|---|---
WasmFX | 24 KB | 2310 ms | 63.9 MB
Asyncify | 36 KB | 480 ms | 64.8 MB
Bespoke | 27 KB | 140 ms | 18.9 MB
(a) Performance Results for WasmFX, Asyncify, and Bespoke

| main-kjp.go | coroutines.go
---|---|---
WasmFX | 156 KB | 7.2 KB
Asyncify | 597 KB | 40 KB
(b) Binary Size Comparison for TinyGo Programs

Figure 7. Preliminary Results

In the second experiment we measure the potential effect that WasmFX and
Asyncify have on the Wasm binary size. Specifically, we compile two off-the-
shelf Go micro-benchmark programs, both of which makes heavy use of coroutines
(KJP, 2019). We compare the size of the Wasm binary generated by the TinyGo
compiler with WasmFX as a backend and optimised Asyncify as a backend. For the
WasmFX backend, we use a coroutine scheduler which closely resembles that of
Section 2. The results are present in Figure 7. The compiled size of the
WasmFX powered binary is significantly smaller than the state-of-the-art.

##  6\. Discussion

###  6.1. Design Considerations

In this section we elaborate on the motivations for the design choices of
WasmFX.

_Direct-style._ The goal of WasmFX is to provide a universal mechanism for
implementing non-local control features. So-called “stackless” approaches such