Runtime Structure¶
Store,stack, and otherruntime structure forming the WebAssembly abstract machine, such asvalues ormodule instances, are made precise in terms of additional auxiliary syntax.
Values¶
WebAssembly computations manipulatevalues of either the four basicnumber types, i.e.,integers andfloating-point data of 32 or 64 bit width each, orvectors of 128 bit width, or ofreference 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\(\mathsf{const}\)instructions and\(\mathsf{ref{.}null}\) producing them.
References other than null are represented with additionaladministrative instructions.They either arescalar references, containing a 31-bitinteger,structure references, pointing to a specificstructure address,array references, pointing to a specificarray address,function references, pointing to a specificfunction address,exception references, pointing to a specificexception address,orhost references pointing to an uninterpreted form ofhost address defined by theembedder.Any of the aformentioned references can furthermore be wrapped up as anexternal reference.
Note
Future versions of WebAssembly may add additional forms of values.
Value types can have an associateddefault value;it is the respective value\(0\) fornumber types,\(0\) forvector types, and null for nullablereference types.For other references, no default value is defined,\({{\href{../exec/runtime.html#aux-default}{\mathrm{default}}}}_{t}\) hence is an optional value\({{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^?}\).
Convention¶
The meta variable\(r\) ranges over reference values where clear from context.
Results¶
Aresult is the outcome of a computation.It is either a sequence ofvalues, a thrownexception, or atrap.
Store¶
Thestore represents all global state that can be manipulated by WebAssembly programs.It consists of the runtime representation of allinstances offunctions,tables,memories,globals,tags,element segments,data segments,andstructures,arrays orexceptionsthat have beenallocated during the life time of the abstract machine.
It is an invariant of the semantics that no element or data instance isaddressed from anywhere else but the owning module instances.
Syntactically, the store is defined as arecord listing the existing instances of each category:
Note
In practice, implementations may apply techniques like garbage collection or reference counting to remove objects from the store that are no longer referenced.However, such techniques are not semantically observable,and hence outside the scope of this specification.
Convention¶
The meta variable\(s\) ranges over stores where clear from context.
Addresses¶
Function instances,table instances,memory instances,global instances,tag instances,element instances,data instancesandstructure,array orexception instancesin thestore are referenced with abstractaddresses.These are simply indices into the respective store component.In addition, anembedder may supply an uninterpreted set ofhost addresses.
Anembedder may assign identity toexported store objects corresponding to their addresses,even where this identity is not observable from within WebAssembly code itself(such as forfunction instances or immutableglobals).
Note
Addresses aredynamic, globally unique references to runtime objects,in contrast toindices,which arestatic, module-local references to their original definitions.Amemory address\(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}\) denotes the abstract addressof a memoryinstance in the store,not an offsetinside 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.
Conventions¶
The notation\({\mathrm{addr}}(A)\) denotes the set of addresses from address space\({\href{../exec/runtime.html#syntax-addr}{\mathit{addr}}}\) occurring free in\(A\). We sometimes reinterpret this set as thelist of its elements, without assuming any particular order.
External Addresses¶
Anexternal address is the runtimeaddress of an entity that can be imported or exported.It is anaddress denoting either afunction instance,global instance,table instance,memory instance, ortag instancein the sharedstore.
Module Instances¶
Amodule instance is the runtime representation of amodule.It is created byinstantiating a module,and collects runtime representations of all entities that are imported, defined, or exported by the module.
Each component references runtime instances corresponding to respective declarations from the original module – whether imported or defined – in the order of their staticindices.Function instances,table instances,memory instances,global instances, andtag instancesare denoted by their respectiveaddresses in thestore.
It is an invariant of the semantics that allexport instances in a given module instance have differentnames.
Note
All record fields except\(\mathsf{exports}\) are to be consideredprivate components of a module instance.They are not accessible to other modules,only to function instances originating from the same module.
Function Instances¶
Afunction instance is the runtime representation of afunction.It effectively is aclosure of the original function over the runtimemodule instance of its originatingmodule.The module instance is used to resolve references to other definitions during execution of the function.
Ahost function is a function expressed outside WebAssembly but passed to amodule as animport.The definition and behavior of host functions are outside the scope of this specification.For the purpose of this specification, it is assumed that wheninvoked,a host function behaves non-deterministically,but within certainconstraints that ensure the integrity of the runtime.
Table Instances¶
Atable instance is the runtime representation of atable.It records itstype and holds a sequence ofreference values.
Table elements can be mutated throughtable instructions, the execution of an activeelement segment, or by external means provided by theembedder.
It is an invariant of the semantics that all table elements have a typematching the element type of\({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\).It also is an invariant that the length of the element sequence never exceeds the maximum size of\({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\).
Memory Instances¶
Amemory instance is the runtime representation of a linearmemory.It records itstype and holds a sequence ofbytes.
The length of the sequence always is a multiple of the WebAssemblypage size, which is defined to be the constant\(65536\) – abbreviated\(64~{\mathrm{Ki}}\).
A memory’s bytes can be mutated throughmemory instructions, the execution of an activedata segment, or by external means provided by theembedder.
It is an invariant of the semantics that the length of the byte sequence, divided by page size, never exceeds the maximum size of\({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\).
Global Instances¶
Aglobal instance is the runtime representation of aglobal variable.It records itstype and holds an individualvalue.
The value of mutable globals can be mutated throughvariable instructions or by external means provided by theembedder.
It is an invariant of the semantics that the value has a typematching thevalue type of\({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\).
Tag Instances¶
Atag instance is the runtime representation of atag definition.It records thedefined type of the tag.
Element Instances¶
Anelement instance is the runtime representation of anelement segment.It holds a list of references and itstype.
It is an invariant of the semantics that all elements of a segment have a typematching\({\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}}\).
Data Instances¶
Adata instance is the runtime representation of adata segment.It holds a list ofbytes.
Export Instances¶
Anexport instance is the runtime representation of anexport.It defines the export’sname and the associatedexternal address.
Conventions¶
The following auxiliary functions are assumed on sequences of external addresses.They extract addresses of a specific kind in an order-preserving fashion:
\({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{funcs}}}({{\mathit{xa}}^\ast})\) extracts allfunction addresses from\({{\mathit{xa}}^\ast}\),
\({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tables}}}({{\mathit{xa}}^\ast})\) extracts alltable addresses from\({{\mathit{xa}}^\ast}\),
\({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{mems}}}({{\mathit{xa}}^\ast})\) extracts allmemory addresses from\({{\mathit{xa}}^\ast}\),
\({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{globals}}}({{\mathit{xa}}^\ast})\) extracts allglobal addresses from\({{\mathit{xa}}^\ast}\),
\({\href{../exec/runtime.html#syntax-externaddr}{\mathrm{tags}}}({{\mathit{xa}}^\ast})\) extracts alltag addresses from\({{\mathit{xa}}^\ast}\).
Aggregate Instances¶
Astructure instance is the runtime representation of a heap object allocated from astructure type.Likewise, anarray instance is the runtime representation of a heap object allocated from anarray type.Both record their respectivedefined type and hold a list of the values of theirfields.
Conventions¶
Conversion of a regularvalue to afield value is defined as follows:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}({\href{../exec/runtime.html#syntax-val}{\mathit{val}}}) & = & {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\{{\href{../exec/runtime.html#aux-packfield}{\mathrm{pack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}(\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~i) & = & {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~{{\href{../exec/numerics.html#op-wrap}{\mathrm{wrap}}}}_{32, {|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}}(i) \\\end{array}\end{split}\]The inverse conversion of afield value to a regularvalue is defined as follows:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}}^{\epsilon}}}{({\href{../exec/runtime.html#syntax-val}{\mathit{val}}})} & = & {\href{../exec/runtime.html#syntax-val}{\mathit{val}}} \\{{{{\href{../exec/runtime.html#aux-unpackfield}{\mathrm{unpack}}}}_{{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}{.}\href{../exec/runtime.html#syntax-packval}{\mathsf{pack}}~i)} & = & \href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}{.}\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~{{{{\href{../exec/numerics.html#op-extend}{\mathrm{extend}}}}_{{|{\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}|}, 32}^{{\href{../syntax/instructions.html#syntax-sx}{\mathit{sx}}}}}}{(i)} \\\end{array}\end{split}\]
Exception Instances¶
Anexception instance is the runtime representation of anexception produced by a\(\mathsf{throw}\) instruction.It holds theaddress of the respectivetag and the argumentvalues.
Stack¶
Besides thestore, mostinstructions interact with an implicitstack.The stack contains the two kinds of entries:
Values: theoperands of instructions.
Control Frames: currently active control flow structures.
The latter can in turn be one of the following:
Labels: activestructured control instructions that can be targeted by branches.
(Call) Frames: theactivation records of activefunction calls.
Handlers: active exception handlers.
Note
Where clear from context,call frame is abbreviated to justframe.
All 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.
Values¶
Values are represented bythemselves.
Labels¶
Labels carry an argument arity\(n\) and their associated branchtarget, which is expressed syntactically as aninstruction sequence:
Intuitively,\({{\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}}^\ast}\) is thecontinuation to execute when the branch is taken, in place of the original control construct.
Note
For example, a loop label has the form
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
When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructions.
Call Frames¶
Call frames carry the return arity\(n\) of the respective function,hold the values of itslocals (including arguments) in the order corresponding to their staticlocal indices,and a reference to the function’s ownmodule instance:
Locals may be uninitialized, in which case they are empty.Locals are mutated by respectivevariable instructions.
Exception Handlers¶
Exception handlers are installed by\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try\_table}}\) instructions and record the corresponding list ofcatch clauses:
The handlers on the stack are searched when an exception isthrown.
Conventions¶
The meta variable\(L\) ranges over labels where clear from context.
The meta variable\(f\) ranges over frame states where clear from context.
The meta variable\(H\) ranges over exception handlers where clear from context.
The following auxiliary definition takes ablock type and looks up theinstruction type that it denotes in the current frame:
\[\begin{split}\begin{array}[t]{@{}lcl@{}l@{}}{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}(x) & = & {t_1^\ast} \rightarrow {t_2^\ast} & \quad \mbox{if}~ z{.}\href{../exec/runtime.html#syntax-state}{\mathsf{types}}{}[x] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} \\{{\href{../exec/runtime.html#aux-blocktype}{\mathrm{instrtype}}}}_{z}({t^?}) & = & \epsilon \rightarrow {t^?} \\\end{array}\end{split}\]
Administrative Instructions¶
Note
This section is only relevant for theformal notation.
In order to express the reduction oftraps,calls,exception handling, andcontrol instructions, the syntax of instructions is extended to include the followingadministrative instructions:
Anaddress reference represents an allocatedreference value of respective form“on the stack”.
The\(\mathsf{label}\),\(\mathsf{frame}\), and\(\mathsf{handler}\) instructions modellabels,frames, and activeexception handlers, respectively,“on the stack”.Moreover, the administrative syntax maintains the nesting structure of the originalstructured control instruction orfunction body and theirinstruction sequences.
The\(\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\(\mathsf{trap}\) instruction, signalling abrupt termination.
Note
For example, thereduction rule for\(\mathsf{block}\) is:
if theblock type\({\mathit{bt}}\) denotes afunction type\(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^{m}} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^{n}}\),such that\(n\) is the block’s result arity.This rule replaces the block with a label instruction,which can be interpreted as “pushing” the label on the stack.When its end is reached, i.e., the inner instruction sequence has been reduced to the empty sequence – or rather, a sequence of\(n\)values representing the results – then the\(\mathsf{label}\) instruction is eliminated courtesy of its ownreduction rule:
This can be interpreted as removing the label from the stack and only leaving the locally accumulated operand values.Validation guarantees that\(n\) matches the number\({|{{\href{../exec/runtime.html#syntax-val}{\mathit{val}}}^\ast}|}\) of resulting values at this point.
Configurations¶
Aconfiguration describes the current computation.It consists of the computations’sstate and the sequence ofinstructions left to execute.The state in turn consists of a globalstore and a currentframe referring to themodule instance in which the computation runs, i.e., where the current function originates from.
Note
The current version of WebAssembly is single-threaded,but configurations with multiple threads may be supported in the future.
Conventions¶
The meta variable\(z\) ranges over frame states where clear from context.
The following shorthands are defined for accessing a state\(z = (s ; f)\):
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{types}}{}[x] & = & f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}{}[x] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{tags}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tags}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tags}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{globals}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{mems}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{tables}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{funcs}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcs}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{datas}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{datas}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{elems}}{}[x] & = & s{.}\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elems}}{}[x]] \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){.}\href{../exec/runtime.html#syntax-state}{\mathsf{locals}}{}[x] & = & f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}{}[x] \\ \end{array}\)
These shorthands also extend tonotation for updating state:
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){}[{.}\href{../exec/runtime.html#syntax-state}{\mathsf{globals}}{}[x]{.}\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v] & = & s{}[{.}\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globals}}{}[x]]{.}\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}} = v] ; f \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){}[{.}\href{../exec/runtime.html#syntax-state}{\mathsf{mems}}{}[x]{.}\href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}{}[i : j] = {b^\ast}] & = & s{}[{.}\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{mems}}{}[x]]{.}\href{../exec/runtime.html#syntax-meminst}{\mathsf{bytes}}{}[i : j] = {b^\ast}] ; f \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){}[{.}\href{../exec/runtime.html#syntax-state}{\mathsf{tables}}{}[x]{.}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}{}[i] = r] & = & s{}[{.}\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}{}[f{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}{.}\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tables}}{}[x]]{.}\href{../exec/runtime.html#syntax-tableinst}{\mathsf{refs}}{}[i] = r] ; f \\ \end{array}\)
\(\begin{array}[t]{@{}l@{~}c@{~}l@{}l@{}} (s ; f){}[{.}\href{../exec/runtime.html#syntax-state}{\mathsf{locals}}{}[x] = v] & = & s ; f{}[{.}\href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}{}[x] = v] \\ \end{array}\)