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.

3. SEMANTICS

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 JavaScript. Values crossing the language boundary are automatically converted according to JavaScript rules.

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 on our experience with JavaScript engines, we picked rules that allow the necessary degree of freedom while still providing enough guarantees to support techniques like NaN-tagging.

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 semantics.

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.