A binary represents a single module and is divided into sections
according to the different kinds of entities declared in it. Code
for function bodies is deferred to a separate section placed
after all declarations to enable streaming compilation as soon
as function bodies begin arriving over the network. An engine
can also parallelize compilation of function bodies. To aid
this further, each body is preceded by its size so that
a decoder can skip ahead and parallelize even its decoding.
The format also allows user-defined sections that may be
ignored by an engine. For example, a custom section is used
to store debug metadata such as source names in binaries.
The WebAssembly semantics consists of two parts: the static
semantics defining validation, and the dynamic semantics defining execution. In both cases, the presentation as a language
allowed us to adopt off-the-shelf formal methods developed in
programming language research over the past decades. They are
convenient and effective tools for declarative specifications. While
we can not show all of it here, our specification is precise, concise, and comprehensive—validation and execution of all of
WebAssembly fit on just two pages of our original paper. 4
Furthermore, these formulations allow effective proofs of
essential properties of this semantics, as are standard in
programming language research, but so far have rarely ever
been done as part of an industrial-strength design process.
Finally, our formalization enabled other researchers to easily
mechanize the WebAssembly specification with theorem
provers, thereby machine-verifying our correctness results as
well as constructing a provably correct interpreter.
3. 1. Execution
We cannot go into much detail in this article, but we want to
give a sense for the general flavor of our formalization (see
Haas et al. 4 for a more thorough explanation).
Reduction. Execution is defined in terms of a standard
small-step reduction relation, 13 where each step of computation is described as a rewrite rule over a sequence of instructions. Figure 2 gives an excerpt of these rules.
For example, the instruction sequence
( i32.const 3) ( i32.const 4) i32.add
is reduced to the constant ( i32.const 7) according to the
fourth rule. This formulation avoids the need for introducing
the operand stack as a separate notion in the semantics—
that stack simply consists of all leading t.const instructions
in an instruction sequence. Execution terminates when an
instruction sequence has been reduced to just constants,
corresponding to the stack of result values. Therefore, constant instructions can be treated as values and abbreviated v.
To deal with control constructs, we need to squint a little
and extend the syntax with a small number of auxiliary
administrative instructions that only occur temporarily during reduction. For example, label marks the extent of an
active block and records the continuation of a branch to it,
while frame essentially is a call frame for function invocation.
Through nesting these constructs, the intertwined nature of
operand and control stack is captured, avoiding the need for
separate stacks with tricky interrelated invariants.
expected type supplied to the call_indirect instruction and
traps in case of a mismatch. This check protects the integrity
of the execution environment. The heterogeneous nature of
the table is based on experience with asm.js’s multiple
homogeneous tables; it allows more faithful representation
of function pointers and simplifies dynamic linking. To aid
dynamic linking scenarios further, exported tables can be
grown and mutated dynamically through external APIs.
Foreign calls. Functions can be imported into a module.
Both direct and indirect calls can invoke an imported function, and through export/import, multiple module instances
can communicate. Additionally, the import mechanism
serves as a safe Foreign Function Interface (FFI) through
which a WebAssembly program can communicate with its
embedding environment. For example, on the Web imported
functions may be host functions that are defined in
2. 5. Determinism
WebAssembly has sought to provide a portable target for
low-level code without sacrificing performance. Where
hardware behavior differs it usually is corner cases such as
out-of-range shifts, integer divide by zero, overflow or underflow in floating point conversion, and alignment. Our design
gives deterministic semantics to all of these across all hardware with only minimal execution overhead.
However, there remain three sources of implementation-dependent behavior that can be viewed as non-determinism.
NaN payloads. WebAssembly follows the IEEE 754 standard for floating point arithmetic. However, IEEE does not
specify the exact bit pattern for NaN values in all cases,
and we found that CPUs differ significantly, while normalizing after every numeric operation is too expensive. Based
that allow the necessary degree of freedom while still providing enough guarantees to support techniques like
Resource exhaustion. Available resources are always
finite and differ wildly across devices. In particular, an
engine may be out of memory when trying to grow the linear memory—semantically, the memory.grow instruction
can non-deterministically return − 1. A call instruction
may also trap due to stack overflow, but this is not semantically observable from within WebAssembly itself since it
aborts the computation.
Host functions. WebAssembly programs can call host
functions which are themselves non-deterministic or
change WebAssembly state. Naturally, the effect of calling
host functions is outside the realm of WebAssembly’s
WebAssembly does not (yet) have threads, and therefore
no non-determinism arising from concurrent memory
access. Adding threads is the subject of ongoing work.
2. 6. Binary format
WebAssembly is transmitted as a binary encoding of the
abstract syntax presented in Figure 1. This encoding has
been designed to minimize both size and decoding time.