Runtime Structure
Store, stack, and other runtime structure forming the WebAssembly abstract machine, such as values or module instances, are made precise in terms of additional auxiliary syntax.
Values
WebAssembly computations manipulate values of either the four basic number types, i.e., integers and floating-point data of 32 or 64 bit width each, or vectors of 128 bit width, or of reference type.
In most places of the semantics, values of different types can occur.
In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit.
It is convenient to reuse the same notation as for the \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) instructions and \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}\) producing them.
References other than null are represented with additional administrative instructions.
They either are function references, pointing to a specific function address,
or external references pointing to an uninterpreted form of extern address that can be defined by the embedder to represent its own objects.
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{number} & \href{../exec/runtime.html#syntax-num}{\mathit{num}} &::=&
\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i32}} \\&&|&
\href{../syntax/types.html#syntax-valtype}{\mathsf{i64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i64}} \\&&|&
\href{../syntax/types.html#syntax-valtype}{\mathsf{f32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f32}} \\&&|&
\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-float}{\mathit{f64}} \\
\def\mathdef2488#1{{}}\mathdef2488{vector} & \href{../exec/runtime.html#syntax-vec}{\mathit{vec}} &::=&
\href{../syntax/types.html#syntax-valtype}{\mathsf{v128}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../syntax/values.html#syntax-int}{\mathit{i128}} \\
\def\mathdef2488#1{{}}\mathdef2488{reference} & \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} &::=&
\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t \\&&|&
\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|&
\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \\
\def\mathdef2488#1{{}}\mathdef2488{value} & \href{../exec/runtime.html#syntax-val}{\mathit{val}} &::=&
\href{../exec/runtime.html#syntax-num}{\mathit{num}} ~|~ \href{../exec/runtime.html#syntax-vec}{\mathit{vec}} ~|~ \href{../exec/runtime.html#syntax-ref}{\mathit{ref}} \\
\end{array}\end{split}\]
Note
Future versions of WebAssembly may add additional forms of reference.
Each value type has an associated default value;
it is the respective value \(0\) for number types, \(0\) for vector types, and null for reference types.
\[\begin{split}\begin{array}{lcl@{\qquad}l}
\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}) \\
\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& t{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0 & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}) \\
\href{../exec/runtime.html#default-val}{\mathrm{default}}_t &=& \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t & (\mathrel{\mbox{if}} t = \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}) \\
\end{array}\end{split}\]
Results
A result is the outcome of a computation.
It is either a sequence of values or a trap.
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{result} & \href{../exec/runtime.html#syntax-result}{\mathit{result}} &::=&
\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast \\&&|&
\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}
\end{array}\end{split}\]
Store
The store represents all global state that can be manipulated by WebAssembly programs.
It consists of the runtime representation of all instances of functions, tables, memories, and globals, element segments, and data segments that have been allocated during the life time of the abstract machine.
It is an invariant of the semantics that no element or data instance is addressed from anywhere else but the owning module instances.
Syntactically, the store is defined as a record listing the existing instances of each category:
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{store} & \href{../exec/runtime.html#syntax-store}{\mathit{store}} &::=& \{~
\begin{array}[t]{l@{~}ll}
\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{tables}} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{mems}} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{globals}} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{elems}} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}^\ast, \\
\href{../exec/runtime.html#syntax-store}{\mathsf{datas}} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}^\ast ~\} \\
\end{array}
\end{array}\end{split}\]
Addresses
Function instances, table instances, memory instances, and global instances, element instances, and data instances in the store are referenced with abstract addresses.
These are simply indices into the respective store component.
In addition, an embedder may supply an uninterpreted set of host addresses.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{address} & \href{../exec/runtime.html#syntax-addr}{\mathit{addr}} &::=&
0 ~|~ 1 ~|~ 2 ~|~ \dots \\
\def\mathdef2488#1{{}}\mathdef2488{function address} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{table address} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{memory address} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{global address} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{element address} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{data address} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\def\mathdef2488#1{{}}\mathdef2488{extern address} & \href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}} \\
\end{array}\end{split}\]
An embedder may assign identity to exported store objects corresponding to their addresses,
even where this identity is not observable from within WebAssembly code itself
(such as for function instances or immutable globals).
Note
Addresses are dynamic, globally unique references to runtime objects,
in contrast to indices,
which are static, module-local references to their original definitions.
A memory address \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) denotes the abstract address of a memory instance in the store,
not an offset inside a memory instance.
There is no specific limit on the number of allocations of store objects,
hence logical addresses can be arbitrarily large natural numbers.
Time Stamps
In order to track the relative ordering in the execution of multiple threads and the occurrence of events,
the semantics uses a notion of abstract time stamps.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{(time stamp)} & \href{../exec/runtime.html#syntax-time}{\mathit{time}} &::=&
\dots \\
\end{array}\end{split}\]
Each time stamp denotes a discrete point in time, and is drawn from an infinite set.
The shape of time stamps is not specified or observable.
Time stamps are associated with a total order – if a time stamp \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1\) is totally ordered before time stamp \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_2\), this is written as \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 \href{../exec/runtime.html#relaxed-prectot}{\mathrel{\prec_{\mathsf{tot}}}} \href{../exec/runtime.html#syntax-time}{\mathit{time}}_2\).
Time stamps are also associated with a happens before partial order – if a time stamp \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1\) happens before \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_2\), this is written as \(\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} \href{../exec/runtime.html#syntax-time}{\mathit{time}}_2\).
During the execution of WebAssembly code, time stamped events may be emitted which are related by one or both of these orderings, thus constraining the code’s observable behaviours according to WebAssembly’s relaxed memory model.
Module Instances
A module instance is the runtime representation of a module.
It is created by instantiating a module,
and collects runtime representations of all entities that are imported, defined, or exported by the module.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{module instance} & \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &::=& \{
\begin{array}[t]{l@{~}ll}
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}} & \href{../syntax/types.html#syntax-functype}{\mathit{functype}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}} & \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}} & \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}} & \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}} & \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}} & \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{dataaddrs}} & \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast, \\
\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast ~\} \\
\end{array}
\end{array}\end{split}\]
Each component references runtime instances corresponding to respective declarations from the original module – whether imported or defined – in the order of their static indices.
Function instances, table instances, memory instances, and global instances are referenced with an indirection through their respective addresses in the store.
It is an invariant of the semantics that all export instances in a given module instance have different names.
Function Instances
A function instance is the runtime representation of a function.
It effectively is a closure of the original function over the runtime module instance of its originating module.
The module instance is used to resolve references to other definitions during execution of the function.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{function instance} & \href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}} &::=&
\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{code}}~\href{../syntax/modules.html#syntax-func}{\mathit{func}} \} \\ &&|&
\{ \href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-funcinst}{\mathsf{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\
\def\mathdef2488#1{{}}\mathdef2488{host function} & \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} &::=& \dots \\
\end{array}\end{split}\]
A host function is a function expressed outside WebAssembly but passed to a module as an import.
The definition and behavior of host functions are outside the scope of this specification.
For the purpose of this specification, it is assumed that when invoked,
a host function behaves non-deterministically,
but within certain constraints that ensure the integrity of the runtime.
Note
Function instances are immutable, and their identity is not observable by WebAssembly code.
However, the embedder might provide implicit or explicit means for distinguishing their addresses.
Table Instances
A table instance is the runtime representation of a table.
It records its type and holds a vector of reference values.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{table instance} & \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} &::=&
\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\
\end{array}\end{split}\]
Table elements can be mutated through table instructions, the execution of an active element segment, or by external means provided by the embedder.
It is an invariant of the semantics that all table elements have a type equal to the element type of \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).
It also is an invariant that the length of the element vector never exceeds the maximum size of \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\), if present.
Memory Instances
A memory instance is the runtime representation of a linear memory.
It records its original memory type
and takes one of two different shapes depending on whether that type is shared or not.
It is an invariant of the semantics that the shape always matches the type.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{(memory instance)} & \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &::=&
\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\ &&|&
\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}} \} \\
\end{array}\end{split}\]
The instance of a memory with unshared type holds a vector of bytes directly representing its state.
The length of the vector always is a multiple of the WebAssembly page size, which is defined to be the constant \(65536\) – abbreviated \(64\,\mathrm{Ki}\).
The bytes can be mutated through memory instructions, the execution of an active data segment, or by external means provided by the embedder.
It is an invariant of the semantics that the length of the byte vector, divided by page size, never exceeds the maximum size of \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\), if present.
For memories of shared type, no state is recorded in the instance itself.
Global Instances
A global instance is the runtime representation of a global variable.
It records its type and holds an individual value.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{global instance} & \href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}} &::=&
\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} \\
\end{array}\end{split}\]
The value of mutable globals can be mutated through variable instructions or by external means provided by the embedder.
It is an invariant of the semantics that the value has a type equal to the value type of \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\).
Element Instances
An element instance is the runtime representation of an element segment.
It holds a vector of references and their common type.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{element instance} & \href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}} &::=&
\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) \} \\
\end{array}\end{split}\]
Data Instances
An data instance is the runtime representation of a data segment.
It holds a vector of bytes.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{data instance} & \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &::=&
\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~\href{../syntax/conventions.html#syntax-vec}{\mathit{vec}}(\href{../syntax/values.html#syntax-byte}{\mathit{byte}}) \} \\
\end{array}\end{split}\]
Export Instances
An export instance is the runtime representation of an export.
It defines the export’s name and the associated external value.
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{export instance} & \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}} &::=&
\{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~\href{../syntax/values.html#syntax-name}{\mathit{name}}, \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}} \} \\
\end{array}\end{split}\]
External Values
An external value is the runtime representation of an entity that can be imported or exported.
It is an address denoting either a function instance, table instance, memory instance, or global instances in the shared store.
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{external value} & \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} &::=&
\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\&&|&
\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\&&|&
\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} \\&&|&
\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\
\end{array}\end{split}\]
Conventions
The following auxiliary notation is defined for sequences of external values.
It filters out entries of a specific kind in an order-preserving fashion:
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
\(\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast) = [\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} ~|~ (\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}) \in \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^\ast]\)
Stack
Besides the store, most instructions interact with an implicit stack.
The stack contains three kinds of entries:
These entries can occur on the stack in any order during the execution of a program.
Stack entries are described by abstract syntax as follows.
Note
It is possible to model the WebAssembly semantics using separate stacks for operands, control constructs, and calls.
However, because the stacks are interdependent, additional book keeping about associated stack heights would be required.
For the purpose of this specification, an interleaved representation is simpler.
Labels
Labels carry an argument arity \(n\) and their associated branch target, which is expressed syntactically as an instruction sequence:
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{label} & \href{../exec/runtime.html#syntax-label}{\mathit{label}} &::=&
\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\} \\
\end{array}\end{split}\]
Intuitively, \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) is the continuation to execute when the branch is taken, in place of the original control construct.
Note
For example, a loop label has the form
\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\dots~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\]
When performing a branch to this label, this executes the loop, effectively restarting it from the beginning.
Conversely, a simple block label has the form
\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}\]
When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
Activation Frames
Activation frames carry the return arity \(n\) of the respective function,
hold the values of its locals (including arguments) in the order corresponding to their static local indices,
and a reference to the function’s own module instance:
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{frame} & \href{../exec/runtime.html#syntax-frame}{\mathit{frame}} &::=&
\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \} \\
\end{array}\end{split}\]
The values of the locals are mutated by respective variable instructions.
Conventions
The meta variable \(L\) ranges over labels where clear from context.
The meta variable \(F\) ranges over frames where clear from context.
The following auxiliary definition takes a block type and looks up the function type that it denotes in the current frame:
\[\begin{split}\begin{array}{lll}
\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}) &=& F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] \\
\href{../exec/runtime.html#exec-expand}{\mathrm{expand}}_F([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]) &=& [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] \\
\end{array}\end{split}\]
Administrative Instructions
In order to express the reduction of traps, calls, and control instructions, the syntax of instructions is extended to include the following administrative instructions:
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{administrative instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=&
\dots \\ &&|&
\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\ &&|&
\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|&
\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~\href{../exec/runtime.html#syntax-externaddr}{\mathit{externaddr}} \\ &&|&
\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\ &&|&
\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|&
\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|&
\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{wait'}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../syntax/values.html#syntax-int}{\mathit{s64}} \\ &&|&
\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{perform}}~\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast \\ &&|&
\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{host}}~\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \\
\end{array}\end{split}\]
The \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) instruction represents the occurrence of a trap.
Traps are bubbled up through nested instruction sequences, ultimately reducing the entire program to a single \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\) instruction, signalling abrupt termination.
The \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}\) instruction represents function reference values. Similarly, \(\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}\) represents external references.
The \(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}\) instruction represents the imminent invocation of a function instance, identified by its address.
It unifies the handling of different forms of calls.
The \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) and \(\href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}\) instructions model labels and frames “on the stack”.
Moreover, the administrative syntax maintains the nesting structure of the original structured control instruction or function body and their instruction sequences with an \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) marker.
That way, the end of the inner instruction sequence is known when part of an outer sequence.
The \(\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{wait'}}\) instruction models a thread suspending further execution as the result of executing a \(\href{../syntax/instructions.html#syntax-instr-atomic-memory}{\mathsf{memory.atomic.wait}}\) instruction. If its \(\href{../syntax/values.html#syntax-int}{\mathit{s64}}\) argument is non-negative, execution may resume after at least \(\href{../syntax/values.html#syntax-int}{\mathit{s64}}\) nanoseconds. Otherwise, execution will only resume after \(\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}\) is the target of a corresponding \(\href{../syntax/instructions.html#syntax-instr-atomic-memory}{\mathsf{memory.atomic.notify}}\) instruction.
The \(\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{perform}}\) instruction is used to perform an action at a precise point in execution. These actions are used by the Relaxed Memory Model to determine the behaviours that are observable in a concurrent execution.
The \(\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{host}}\) instruction models the execution of the host environment.
Note
For example, the reduction rule for \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}\) is:
\[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~[t^n]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#formal-notation}{\hookrightarrow}\quad
\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\epsilon\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\]
This replaces the block with a label instruction,
which can be interpreted as “pushing” the label on the stack.
When \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\) is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of \(n\) \(\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}\) instructions representing the resulting values – then the \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) instruction is eliminated courtesy of its own reduction rule:
\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_m\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#formal-notation}{\hookrightarrow}\quad \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n\]
This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values.
Block Contexts
In order to specify the reduction of branches, the following syntax of block contexts is defined, indexed by the count \(k\) of labels surrounding a hole \([\_]\) that marks the place where the next step of computation is taking place:
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^0 &::=&
\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~[\_]~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\
\def\mathdef2488#1{{}}\mathdef2488{block contexts} & \href{../exec/runtime.html#syntax-ctxt-block}{B}^{k+1} &::=&
\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^k~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \\
\end{array}\end{split}\]
This definition allows to index active labels surrounding a branch or return instruction.
Note
For example, the reduction of a simple branch can be defined as follows:
\[\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_0\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~\href{../exec/runtime.html#syntax-ctxt-block}{B}^l[\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l]~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \quad\href{../exec/conventions.html#formal-notation}{\hookrightarrow}\quad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\]
Here, the hole \([\_]\) of the context is instantiated with a branch instruction.
When a branch occurs,
this rule replaces the targeted label and associated instruction sequence with the label’s continuation.
The selected label is identified through the label index \(l\), which corresponds to the number of surrounding \(\href{../exec/runtime.html#syntax-label}{\mathsf{label}}\) instructions that must be hopped over – which is exactly the count encoded in the index of a block context.
Events
The interaction of a computation with the store is described through events.
An event is a (possibly empty) set of actions, such as reads and writes,
that are atomically performed by the execution of an individual instruction.
Each event is annotated with two time stamps: the first records the time stamp of the event’s immediate predecessor while the second uniquely identifies the event.
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{(event)} & \href{../exec/runtime.html#syntax-evt}{\mathit{evt}} &::=&
\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}} \\
\def\mathdef2488#1{{}}\mathdef2488{(action)} & \href{../exec/runtime.html#syntax-act}{\mathit{act}} &::=&
\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}_{\href{../exec/runtime.html#syntax-ord}{\mathit{ord}}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../exec/runtime.html#syntax-storeval}{\mathit{storeval}}~\href{../exec/runtime.html#syntax-ord}{\mathsf{notears}}^? \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathit{ord}}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../exec/runtime.html#syntax-storeval}{\mathit{storeval}}~\href{../exec/runtime.html#syntax-ord}{\mathsf{notears}}^? \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{rmw}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../exec/runtime.html#syntax-storeval}{\mathit{storeval}}~\href{../exec/runtime.html#syntax-storeval}{\mathit{storeval}} \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{wait}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../syntax/values.html#syntax-int}{\mathit{s64}} \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{woken}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~ \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{timeout}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~ \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{notify}}~\href{../exec/runtime.html#syntax-loc}{\mathit{loc}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}}~\href{../syntax/values.html#syntax-int}{\mathit{u32}} \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{fence}} \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathsf{spawn}} \\&&|&
\href{../exec/runtime.html#syntax-act}{\mathit{hostact}} \\
\def\mathdef2488#1{{}}\mathdef2488{(ordering)} & \href{../exec/runtime.html#syntax-ord}{\mathit{ord}} &::=&
\href{../exec/runtime.html#syntax-ord}{\mathsf{unord}} ~|~
\href{../exec/runtime.html#syntax-ord}{\mathsf{seqcst}} ~|~
\href{../exec/runtime.html#syntax-ord}{\mathsf{init}} \\
\def\mathdef2488#1{{}}\mathdef2488{(location)} & \href{../exec/runtime.html#syntax-loc}{\mathit{loc}} &::=&
\href{../exec/runtime.html#syntax-reg}{\mathit{reg}}[\href{../syntax/values.html#syntax-int}{\mathit{u32}}] \\
\def\mathdef2488#1{{}}\mathdef2488{(region)} & \href{../exec/runtime.html#syntax-reg}{\mathit{reg}} &::=&
\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}.\href{../exec/runtime.html#syntax-fld}{\mathit{fld}} \\
\def\mathdef2488#1{{}}\mathdef2488{(field)} & \href{../exec/runtime.html#syntax-fld}{\mathit{fld}} &::=&
\href{../exec/runtime.html#syntax-loc}{\mathsf{len}} ~|~
\href{../exec/runtime.html#syntax-loc}{\mathsf{data}} \\
\def\mathdef2488#1{{}}\mathdef2488{(store value)} & \href{../exec/runtime.html#syntax-storeval}{\mathit{storeval}} &::=&
\href{../exec/runtime.html#syntax-val}{\mathit{val}} ~|~
\href{../syntax/values.html#syntax-byte}{\mathit{byte}}^\ast \\
\end{array}\end{split}\]
The access of mutable shared state is performed through the \(\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}\), \(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}\), and \(\href{../exec/runtime.html#syntax-act}{\mathsf{rmw}}\) actions.
Each action accesses an abstract location, which consists of an address of a shared memory instance, a symbolic field name in the respective object (either \(\href{../exec/runtime.html#syntax-loc}{\mathsf{len}}\) for the size or \(\href{../exec/runtime.html#syntax-loc}{\mathsf{data}}\) for the vector of bytes), and an offset index into the field.
In each case, read and write actions record the store value that has been read or written, which is either a regular value or a sequence of bytes, depending on the location accessed.
An \(\href{../exec/runtime.html#syntax-act}{\mathsf{rmw}}\) event, performing an atomic read-modify-write access, records both the store values read (first) and written (second);
it is an invariant of the semantics that both are either regular values of the same type or byte sequences of the same length.
\(\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}\) and \(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}\) events are further annotated by a memory ordering, which describes whether the access is unordered, as e.g. performed by a regular load or store instruction, or sequentially consistent, as e.g. performed by atomic memory instructions.
A third ordering, initialisation, is used to record the initial value taken by the memory location upon its creation.
A \(\href{../exec/runtime.html#syntax-act}{\mathsf{rmw}}\) action always is sequentially consistent.
Note
Future versions of WebAssembly may introduce additional orderings.
Finally, a host action is an action performed outside of WebAssembly code.
Its form and meaning is outside the scope of this specification.
Note
An embedder may define a custom set of host actions and respective ordering constraints to model other forms of interactions that are not expressible within WebAssembly, but whose ordering relative to WebAssembly events is relevant for the combined semantics.
Conventions
The actions \(\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}_{\href{../exec/runtime.html#syntax-ord}{\mathit{ord}}}\) and \(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathit{ord}}}\) are abbreviated to just \(\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}\) and \(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}\) when \(\href{../exec/runtime.html#syntax-ord}{\mathit{ord}}\) is \(\href{../exec/runtime.html#syntax-ord}{\mathsf{unord}}\).
A location may syntactically elide its \([\href{../syntax/values.html#syntax-int}{\mathit{u32}}]\) offset in the case that it is 0.
The following auxiliary definition is used to classify whether an access will tear - that is, whether it will observably decompose into bytewise accesses when it participates in a data race.
\[\begin{split}\begin{array}{lcl@{\qquad}l}
\href{../exec/relaxed.html#syntax-ord}{\mathrm{tearing}}(\href{../syntax/values.html#syntax-int}{\mathit{i}N}', N, \href{../syntax/values.html#syntax-int}{\mathit{u32}}) &=& \href{../exec/runtime.html#syntax-ord}{\mathsf{notears}} & (\mathrel{\mbox{if}} \href{../syntax/values.html#syntax-int}{\mathit{u32}} \mathbin{\mathrm{mod}} N/8 = 0 \wedge N \leq 32) \\
\href{../exec/relaxed.html#syntax-ord}{\mathrm{tearing}}(\href{../syntax/values.html#syntax-int}{\mathit{i}N}', N, \href{../syntax/values.html#syntax-int}{\mathit{u32}}) &=& \epsilon &(otherwise) \\
\href{../exec/relaxed.html#syntax-ord}{\mathrm{tearing}}(\href{../syntax/values.html#syntax-float}{\mathit{f}N}', N, \href{../syntax/values.html#syntax-int}{\mathit{u32}}) &=& \epsilon \\
\end{array}\end{split}\]
Relations between time stamps are lifted to relations between events.
\[\begin{split}\begin{array}{lclclcl}
\href{../exec/runtime.html#syntax-act}{\mathit{act}}_1^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_p~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 & \href{../exec/runtime.html#relaxed-prectot}{\mathrel{\prec_{\mathsf{tot}}}} & \href{../exec/runtime.html#syntax-act}{\mathit{act}}_2^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}'_p~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_2 &=& \href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 & \href{../exec/runtime.html#relaxed-prectot}{\mathrel{\prec_{\mathsf{tot}}}} & \href{../exec/runtime.html#syntax-time}{\mathit{time}}_2 \\
\href{../exec/runtime.html#syntax-act}{\mathit{act}}_1^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_p~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 & \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} & \href{../exec/runtime.html#syntax-act}{\mathit{act}}_2^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}}'_p~\href{../exec/runtime.html#syntax-time}{\mathit{time}}_2 &=& \href{../exec/runtime.html#syntax-time}{\mathit{time}}_1 & \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} & \href{../exec/runtime.html#syntax-time}{\mathit{time}}_2 \\
\end{array}\end{split}\]
Configurations
A thread is a computation over instructions that operates relative to a current frame referring to the module instance in which the current computation runs. The thread is annotated with the time it was last active.
A global configuration consists of the current store and a list of executing threads.
A local configuration describes the state of a single executing thread.
\[\begin{split}\begin{array}{llcl}
\def\mathdef2488#1{{}}\mathdef2488{(thread)} & \href{../exec/runtime.html#syntax-thread}{\mathit{thread}} &::=&
\href{../exec/runtime.html#syntax-frame}{\mathit{frame}}; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~\href{../exec/runtime.html#syntax-time}{\mathit{time}} \\
\def\mathdef2488#1{{}}\mathdef2488{(configuration)} & \href{../exec/runtime.html#syntax-config}{\mathit{config}} &::=&
\href{../exec/runtime.html#syntax-store}{\mathit{store}}; \href{../exec/runtime.html#syntax-thread}{\mathit{thread}}^\ast \\
\def\mathdef2488#1{{}}\mathdef2488{(local configuration)} & \href{../exec/runtime.html#syntax-config}{\mathit{lconfig}} &::=&
\href{../exec/runtime.html#syntax-store}{\mathit{store}}; \href{../exec/runtime.html#syntax-thread}{\mathit{thread}} \\
\end{array}\end{split}\]
A thread has terminated when its instruction sequence has been reduced to a result,
that is, either a sequence of values or to a \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\).
Reduction
Formally, WebAssembly computation is defined by two small-step reduction relations on global and local configurations
that define how a single step of execution modifies these configurations, respectively.
Global Reduction
Global reduction is concerned with allocation in the global store and synchronization between multiple threads.
It emits a (possibly empty) set of events that are produced by the corresponding step of computation.
Formally, global reduction is a relation
\[\href{../exec/runtime.html#syntax-config}{\mathit{config}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-evt}{\mathit{evt}}} \href{../exec/runtime.html#syntax-config}{\mathit{config}}\]
defined by inductive rewrite rules on global configurations.
The following structural rule for global reduction delegates to local reduction for single thread execution:
\[\begin{split}\begin{array}{@{}c@{}}
S; P_1^\ast~(F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}} h)~P_2^\ast
\qquad \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~h~h'} \qquad
S'; P_1^\ast~(F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast \href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}} h')~P_2^\ast \\
\qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\mathrel{\mbox{if}} & S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast} S'; F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast \\
\wedge & h \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} h' \\
\wedge & \href{../exec/runtime.html#syntax-act}{\mathsf{spawn}} \notin \href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast) \\
\end{array}
\end{array}\end{split}\]
The following rule for global reduction describes the creation of a new thread by the host:
\[\begin{split}\begin{array}{@{}c@{}}
S; P_1^\ast~(F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}} h)~P_2^\ast
\qquad \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\epsilon~\href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}}~h~h'} \qquad
S'; P_1^\ast~(F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast \href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}} h')~P_2^\ast~(\epsilon; (\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{host}}~[\epsilon]) \href{../exec/runtime.html#syntax-time}{\mathbin{\mathsf{at}}} h'') \\
\qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\mathrel{\mbox{if}} & S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathsf{spawn}}} S'; F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast \\
\wedge & h \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} h' \\
\wedge & h \href{../exec/runtime.html#relaxed-prechb}{\mathrel{\prec_{\mathsf{hb}}}} h'' \\
\end{array}
\end{array}\end{split}\]
Note
The time stamp \(h'\) indicates the point in time at which the computation step takes place,
marking both the emitted atomic event and the updated time of the thread.
This time stamp is chosen non-deterministically in the rule.
However, the second side condition ensures that the time \(h\) of the last activity of the thread happened before \(h'\), thereby imposing program order for any events originating from the same thread.
Local Reduction
Local reduction defines the execution of individual instructions.
Each execution step can perform a (possibly empty) set of actions.
Formally, this is described by a labelled relation
\[\href{../exec/runtime.html#syntax-config}{\mathit{lconfig}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast} \href{../exec/runtime.html#syntax-config}{\mathit{lconfig}}\]
To avoid unnecessary clutter, the following conventions are employed in the notation for local reduction rules:
Evaluation Contexts
Finally, the following definition of evaluation context and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps:
\[\begin{split}\begin{array}{llll}
\def\mathdef2488#1{{}}\mathdef2488{evaluation contexts} & E &::=&
[\_] ~|~
\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast~E~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast ~|~
\href{../exec/runtime.html#syntax-label}{\mathsf{label}}_n\{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\}~E~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}{rcl}
S; F; E[\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast] &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast}& S'; F'; E[{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast] \\
&& (\mathrel{\mbox{if}} S; F; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast} S'; F'; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast) \\
S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F'\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast}& S'; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F''\}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\
&& (\mathrel{\mbox{if}} S; F'; \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast} S'; F''; {\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}'}^\ast) \\[1ex]
S; F; E[\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}] &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}
\qquad (\mathrel{\mbox{if}} E \neq [\_]) \\
S; F; \href{../exec/runtime.html#syntax-frame}{\mathsf{frame}}_n\{F'\}~\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S; F; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} \\
\end{array}\end{split}\]
Reduction terminates when a thread’s instruction sequence has been reduced to a result,
that is, either a sequence of values or to a \(\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\).
Note
The restriction on evaluation contexts rules out contexts like \([\_]\) and \(\epsilon~[\_]~\epsilon\) for which \(E[\href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}] = \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}}\).
For an example of reduction under evaluation contexts, consider the following instruction sequence.
\[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\]
This can be decomposed into \(E[(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_2)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{neg}}]\) where
\[E = (\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_1)~[\_]~(\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~x_3)~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{add}}~\href{../syntax/types.html#syntax-valtype}{\mathsf{f64}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{mul}}\]
Moreover, this is the only possible choice of evaluation context where the contents of the hole matches the left-hand side of a reduction rule.
