Modules

For modules, the execution semantics primarily defines instantiation, which allocates instances for a module and its contained definitions, initializes tables and memories from contained element and data segments, and invokes the start function if present. It also includes invocation of exported functions.

Instantiation depends on a number of auxiliary notions for type-checking imports and allocating instances.

External Typing

For the purpose of checking external values against imports, such values are classified by external types. The following auxiliary typing rules specify this typing relation relative to a store \(S\) in which the referenced instances live.

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a]\) must exist.

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]\) must exist.

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\).

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} }\]

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) must exist.

• If \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) is \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}}\), then:

  • \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}})\).

• Else:

  • Assert: \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) is \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}}\).

  • Let \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~x, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~y^? \}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}}\) be the memory type \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\).

  • Assert: the current length of \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]\) in bytes, \(l\), is given by the action \((\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{seqcst}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{len}}~l)\).

  • \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~l, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~y^? \}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}})\).

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}} }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}}) }\]

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} = \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~x, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~y^? \}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}} }{ S; (\href{../exec/runtime.html#syntax-act}{\mathsf{rd}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{seqcst}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{len}}~l) \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~l, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~y^? \}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}}) }\]

Note

In the \(\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}}\) case, the associated action is performed as part of instantiation, in order to record in the Relaxed Memory Model that a sequentially consistent bounds check on the shared memory has occurred.

\(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\)

• The store entry \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]\) must exist.

• Then \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a\) is valid with external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}\).

\[\frac{ }{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a].\href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}} }\]

Value Typing

For the purpose of checking argument values against the parameter types of exported functions, values are classified by value types. The following auxiliary typing rules specify this typing relation relative to a store \(S\) in which possibly referenced addresses live.

Numeric Values \(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c\)

• The value is valid with number type \(t\).

\[\frac{ }{ S \href{../appendix/properties.html#valid-val}{\vdash} t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c : t }\]

Null References \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t\)

• The value is valid with reference type \(t\).

\[\frac{ }{ S \href{../appendix/properties.html#valid-val}{\vdash} \href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t : t }\]

Function References \(\href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a\)

• The external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a\) must be valid.

• Then the value is valid with reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}}\).

\[\frac{ S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a : \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ S \href{../appendix/properties.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref}{\mathsf{ref}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{funcref}} }\]

External References \(\href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~a\)

• The value is valid with reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{externref}}\).

\[\frac{ }{ S \href{../appendix/properties.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-ref.extern}{\mathsf{ref{.}extern}}~a : \href{../syntax/types.html#syntax-reftype}{\mathsf{externref}} }\]

Allocation

New instances of functions, tables, memories, and globals are allocated in a store \(S\), as defined by the following auxiliary functions.

Functions

1. Let \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}\) be the function to allocate and \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) its module instance.

2. Let \(a\) be the first free function address in \(S\).

3. Let \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) be the function type \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}]\).

4. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \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}} \}\).

5. Append \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) of \(S\).

6. Return \(a\).

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}(S, \href{../syntax/modules.html#syntax-func}{\mathit{func}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \href{../syntax/types.html#syntax-functype}{\mathit{functype}} &=& \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}[\href{../syntax/modules.html#syntax-func}{\mathit{func}}.\href{../syntax/modules.html#syntax-func}{\mathsf{type}}] \\ \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}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

Host Functions

1. Let \(\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}\) be the host function to allocate and \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) its function type.

2. Let \(a\) be the first free function address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(\{ \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}} \}\).

4. Append \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}\) of \(S\).

5. Return \(a\).

\[\begin{split}~\\[-1ex] \begin{array}{rlll} \href{../exec/modules.html#alloc-hostfunc}{\mathrm{allochostfunc}}(S, \href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}}) &=& S', \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}| \\ \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{hostcode}}~\href{../exec/runtime.html#syntax-hostfunc}{\mathit{hostfunc}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}~\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\} \\ \end{array}\end{split}\]

Note

Host functions are never allocated by the WebAssembly semantics itself, but may be allocated by the embedder.

Tables

1. Let \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) be the table type to allocate and \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) the initialization value.

2. Let \((\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}})\) be the structure of table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\).

3. Let \(a\) be the first free table address in \(S\).

4. Let \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) be the table instance \(\{ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \}\) with \(n\) elements set to \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\).

5. Append \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}\) of \(S\).

6. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) &=& S', \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \\ \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}| \\ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}~\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\} \\ \end{array}\end{split}\]

Memories

1. Let \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) be the memory type to allocate.

2. Let \(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-share}{\mathit{share}}\) be the structure of memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\).

3. Let \(a\) be the first free memory address in \(S\).

4. If \(\href{../syntax/types.html#syntax-share}{\mathit{share}}\) is \(\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}}\):

   1. Let \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) be the memory instance \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef2406#1{\mathtt{0x#1}}\mathdef2406{00})^{n \cdot 64\,\mathrm{Ki}} \}\) that contains \(n\) pages of zeroed bytes.

   2. Let \(\mathit{act}^\ast\) be \(\epsilon\).

5. Else:

   1. Let \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) be the memory instance \(\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \}\).

   2. Let \(\mathit{act}^\ast\) be \((\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{seqcst}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{len}}~n)(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{init}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{data}}[0]~(0)^{n \cdot 64})\).

5. Append \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}\) of \(S\).

6. Return \(a, \mathit{act}^\ast\).

\[\begin{split}\begin{array}{l} \begin{array}{rlll} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) &=& S', \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}, \epsilon \\[1ex] \mathrel{\mbox{if}} \hfill \\ \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}} \\ \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}| \\ \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &=& \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef2407#1{\mathtt{0x#1}}\mathdef2407{00})^{n \cdot 64\,\mathrm{Ki}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\} \\ \end{array} \\ % \\ \begin{array}{rlll} \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}(S, \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}) &=& S', a, (\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{seqcst}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{len}}~n)(\href{../exec/runtime.html#syntax-act}{\mathsf{wr}}_{\href{../exec/runtime.html#syntax-ord}{\mathsf{init}}}~a.\href{../exec/runtime.html#syntax-loc}{\mathsf{data}}[0]~(0)^{n \cdot 64}) \\[1ex] \mathrel{\mbox{if}} \hfill \\ \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} &=& \{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-memtype}{\mathsf{shared}} \\ a &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}| \\ \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} &=& \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}~\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\} \\ \end{array} \end{array}\end{split}\]

Globals

1. Let \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) be the global type to allocate and \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}\) the value to initialize the global with.

2. Let \(a\) be the first free global address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\) be the global instance \(\{ \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}} \}\).

4. Append \(\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}\) of \(S\).

5. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}(S, \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}) &=& S', \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}| \\ \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}} \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}~\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}\} \\ \end{array}\end{split}\]

Element segments

1. Let \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\) be the elements’ type and \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast\) the vector of references to allocate.

2. Let \(a\) be the first free element address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\) be the element instance \(\{ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\).

4. Append \(\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}\) of \(S\).

5. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}(S, \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast) &=& S', \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}| \\ \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{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}~\href{../exec/runtime.html#syntax-eleminst}{\mathit{eleminst}}\} \\ \end{array}\end{split}\]

Data segments

1. Let \(b^\ast\) be the vector of bytes to allocate.

2. Let \(a\) be the first free data address in \(S\).

3. Let \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\) be the data instance \(\{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \}\).

4. Append \(\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\) to the \(\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}\) of \(S\).

5. Return \(a\).

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}(S, b^\ast) &=& S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} \\[1ex] \mbox{where:} \hfill \\ \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}} &=& |S.\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}| \\ \href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}} &=& \{ \href{../exec/runtime.html#syntax-datainst}{\mathsf{data}}~b^\ast \} \\ S' &=& S \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../exec/runtime.html#syntax-store}{\mathsf{datas}}~\href{../exec/runtime.html#syntax-datainst}{\mathit{datainst}}\} \\ \end{array}\end{split}\]

Growing tables

1. Let \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}\) be the table instance to grow, \(n\) the number of elements by which to grow it, and \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}\) the initialization value.

2. Let \(\mathit{len}\) be \(n\) added to the length of \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\).

3. If \(\mathit{len}\) is larger than or equal to \(2^{32}\), then fail.

4. Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t\) be the structure of table type \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\).

5. Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) be \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) with \(\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) updated to \(\mathit{len}\).

6. If \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) is not valid, then fail.

7. Append \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n\) to \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}\).

8. Set \(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}}\) to the table type \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'~t\).

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-table}{\mathrm{growtable}}(\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}, n, \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}) &=& \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}'~t \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}} = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}| \\ \wedge & \mathit{len} < 2^{32} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t = \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{type}} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' = \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/types.html#syntax-limits}{\mathsf{min}} = \mathit{len} \\ \wedge & \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \mathrel{\mbox{ok}}) \\ \end{array} \\ \end{array}\end{split}\]

Growing memories

1. Let \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}\) be the memory instance to grow and \(n\) the number of pages by which to grow it.

2. Assert: The length of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) is divisible by the page size \(64\,\mathrm{Ki}\).

3. Let \(\mathit{len}\) be \(n\) added to the length of \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\) divided by the page size \(64\,\mathrm{Ki}\).

4. If \(\mathit{len}\) is larger than \(2^{16}\), then fail.

5. Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) be the structure of memory type \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\).

6. Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) be \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) with \(\href{../syntax/types.html#syntax-limits}{\mathsf{min}}\) updated to \(\mathit{len}\).

7. If \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\) is not valid, then fail.

8. Append \(n\) times \(64\,\mathrm{Ki}\) bytes with value \(\def\mathdef2408#1{\mathtt{0x#1}}\mathdef2408{00}\) to \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}\).

9. Set \(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}}\) to the memory type \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}'\).

\[\begin{split}\begin{array}{rllll} \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}, n) &=& \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} = \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef2409#1{\mathtt{0x#1}}\mathdef2409{00})^{n \cdot 64\,\mathrm{Ki}} \\ && ( \begin{array}[t]{@{}r@{~}l@{}} \mathrel{\mbox{if}} & \mathit{len} = n + |\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}| / 64\,\mathrm{Ki} \\ \wedge & \mathit{len} \leq 2^{16} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{unshared}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{type}} \\ \wedge & \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' = \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../syntax/types.html#syntax-limits}{\mathsf{min}} = \mathit{len} \\ \wedge & \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}' \mathrel{\mbox{ok}}) \\ \end{array} \\ \end{array}\end{split}\]

Modules

The allocation function for modules requires a suitable list of external values that are assumed to match the import vector of the module, a list of initialization values for the module’s globals, and list of reference vectors for the module’s element segments.

1. Let \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) be the module to allocate and \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\) the vector of external values providing the module’s imports, \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) the initialization values of the module’s globals, and \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) the reference vectors of the module’s element segments.

2. For each function \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) be the function address resulting from allocating \(\href{../syntax/modules.html#syntax-func}{\mathit{func}}_i\) for the module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) defined below.

3. For each table \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}\), do:

   1. Let \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_i~t_i\) be the table type \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\).

   2. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) be the table address resulting from allocating \(\href{../syntax/modules.html#syntax-table}{\mathit{table}}_i.\href{../syntax/modules.html#syntax-table}{\mathsf{type}}\) with initialization value \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t_i\).

4. For each memory \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i, \href{../exec/runtime.html#syntax-act}{\mathit{act}}_i^\ast\) be the memory address resulting from allocating \(\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}}\).

5. For each global \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) be the global address resulting from allocating \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{type}}\) with initializer value \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast[i]\).

6. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) be the element address resulting from allocating an element instance of reference type \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}\) with contents \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast[i]\).

7. For each data segment \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\), do:

   1. Let \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\) be the data address resulting from allocating a data instance with contents \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\).

8. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\) be the concatenation of the function addresses \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i\) in index order.

9. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\) be the concatenation of the table addresses \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i\) in index order.

10. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\) be the concatenation of the memory addresses \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i\) in index order.

11. Let \(\href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast\) be the concatenation of the actions \(\href{../exec/runtime.html#syntax-act}{\mathit{act}}_i^\ast\) in index order.

11. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\) be the concatenation of the global addresses \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i\) in index order.

12. Let \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast\) be the concatenation of the element addresses \(\href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}_i\) in index order.

13. Let \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast\) be the concatenation of the data addresses \(\href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}_i\) in index order.

14. Let \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast\) be the list of function addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast\).

15. Let \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast\) be the list of table addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast\).

16. Let \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast\) be the list of memory addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast\).

17. Let \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast\) be the list of global addresses extracted from \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast\), concatenated with \(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast\).

18. For each export \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}\), do:

    1. If \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a function export for function index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast[x])\).

    2. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a table export for table index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~(\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast[x])\).

    3. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a memory export for memory index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{mem}}~(\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast[x])\).

    4. Else, if \(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i\) is a global export for global index \(x\), then let \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) be the external value \(\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~(\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast[x])\).

    5. Let \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) be the export instance \(\{\href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}_i.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\}\).

19. Let \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\) be the concatenation of the export instances \(\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i\) in index order.

20. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) be the module instance \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}),\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_{\mathrm{mod}}^\ast,\) \(\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{exports}}~\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast\}\).

21. Return \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast\).

\[\begin{split}~\\ \begin{array}{rlll} \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast) &=& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast \end{array}\end{split}\]

where:

\[\begin{split}\begin{array}{@{}rlll@{}} \href{../syntax/modules.html#syntax-table}{\mathit{table}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}} \\ \href{../syntax/modules.html#syntax-mem}{\mathit{mem}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}} \\ \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} \\ \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}} \\ \href{../syntax/modules.html#syntax-data}{\mathit{data}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}} \\ \href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast &=& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}} \\[1ex] \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} &=& \{~ \begin{array}[t]{@{}l@{}} \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{types}}~\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{types}}, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \\ \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{im}}^\ast)~\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} \\[1ex] S_1, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast &=& \href{../exec/modules.html#alloc-func}{\mathrm{allocfunc}}^\ast(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}, \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}) \\ S_2, \href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast &=& \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}^\ast(S_1, (\href{../syntax/modules.html#syntax-table}{\mathit{table}}.\href{../syntax/modules.html#syntax-table}{\mathsf{type}})^\ast, (\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~t)^\ast) \quad (\mathrel{\mbox{where}} (\href{../syntax/modules.html#syntax-table}{\mathit{table}}.\href{../syntax/modules.html#syntax-table}{\mathsf{type}})^\ast = (\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~t)^\ast) \\ S_3, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast, \href{../exec/runtime.html#syntax-act}{\mathit{act}}^\ast &=& \href{../exec/modules.html#alloc-mem}{\mathrm{allocmem}}^\ast(S_2, (\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}})^\ast) \\ S_4, \href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast &=& \href{../exec/modules.html#alloc-global}{\mathrm{allocglobal}}^\ast(S_3, (\href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{type}})^\ast, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \\ S_5, \href{../exec/runtime.html#syntax-elemaddr}{\mathit{elemaddr}}^\ast &=& \href{../exec/modules.html#alloc-elem}{\mathrm{allocelem}}^\ast(S_4, (\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{type}})^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast) \\ S', \href{../exec/runtime.html#syntax-dataaddr}{\mathit{dataaddr}}^\ast &=& \href{../exec/modules.html#alloc-data}{\mathrm{allocdata}}^\ast(S_5, (\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{init}})^\ast) \\ \href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast &=& \{ \href{../exec/runtime.html#syntax-exportinst}{\mathsf{name}}~(\href{../syntax/modules.html#syntax-export}{\mathit{export}}.\href{../syntax/modules.html#syntax-export}{\mathsf{name}}), \href{../exec/runtime.html#syntax-exportinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}} \}^\ast \\[1ex] \href{../exec/runtime.html#syntax-externval}{\mathrm{funcs}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x])^\ast \qquad~ (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{funcs}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{tables}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{tables}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{mems}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[x])^\ast \qquad (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{mems}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_{\mathrm{ex}}^\ast) &=& (\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}[x])^\ast \qquad\!\!\! (\mathrel{\mbox{where}} x^\ast = \href{../syntax/modules.html#syntax-exportdesc}{\mathrm{globals}}(\href{../syntax/modules.html#syntax-export}{\mathit{export}}^\ast)) \\ \end{array}\end{split}\]

Here, the notation \(\mathrm{allocx}^\ast\) is shorthand for multiple allocations of object kind \(X\), defined as follows:

\[\begin{split}\begin{array}{rlll} \mathrm{allocx}^\ast(S_0, X^n, \dots) &=& S_n, a^n \\[1ex] \mbox{where for all $i < n$:} \hfill \\ S_{i+1}, a^n[i] &=& \mathrm{allocx}(S_i, X^n[i], \dots) \end{array}\end{split}\]

Moreover, if the dots \(\dots\) are a sequence \(A^n\) (as for globals or tables), then the elements of this sequence are passed to the allocation function pointwise.

Note

The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) is passed to the function allocator as an argument, in order to form the necessary closures. In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step.

Instantiation

Given a store \(S\), a module \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is instantiated with a list of external values \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) supplying the required imports as follows.

Instantiation checks that the module is valid and the provided imports match the declared types, and may fail with an error otherwise. Instantiation can also result in a trap from initializing a table or memory from an active segment or from executing the start function. It is up to the embedder to define how such conditions are reported.

1. If \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is not valid, then:

   1. Fail.

2. Assert: \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) is valid with external types \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^m\) classifying its imports.

3. If the number \(m\) of imports is not equal to the number \(n\) of provided external values, then:

   1. Fail.

4. For each external value \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) in \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\) and external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\) in \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^n\), do:

   1. If \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\) is valid with an external type \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) in store \(S\), then:

      1. Assert: in checking the validity of \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}_i\), the shared memory actions \(\mathit{act}_i^?\) are performed.

   2. Else:

      1. Fail.

   3. If \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i\) does not match \(\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}'_i\), then:

      1. Fail.

5. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{init}}\) be the auxiliary module instance \(\{\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{globaladdrs}}~\href{../exec/runtime.html#syntax-externval}{\mathrm{globals}}(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n), \href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}\}\) that only consists of the imported globals and the imported and allocated functions from the final module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), defined below.

6. Let \(F_{\mathrm{init}}\) be the auxiliary frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{init}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

7. Push the frame \(F_{\mathrm{init}}\) to the stack.

8. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) be the vector of global initialization values determined by \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) and \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\). These may be calculated as follows.

   1. For each global \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}\), do:

      1. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) be the result of evaluating the initializer expression \(\href{../syntax/modules.html#syntax-global}{\mathit{global}}_i.\href{../syntax/modules.html#syntax-global}{\mathsf{init}}\).

   2. Assert: due to validation, the frame \(F_{\mathrm{init}}\) is now on the top of the stack.

   3. Let \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) be the concatenation of \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) in index order.

9. Let \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) be the list of reference vectors determined by the element segments in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\). These may be calculated as follows.

   1. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\), and for each element expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\) in \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\), do:

      1. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) be the result of evaluating the initializer expression \(\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{ij}\).

   2. Let \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) be the concatenation of function elements \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_{ij}\) in order of index \(j\).

   3. Let \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) be the concatenation of function element vectors \(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast_i\) in order of index \(i\).

10. Pop the frame \(F_{\mathrm{init}}\) from the stack.

11. Let \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) be a new module instance allocated from \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}\) in store \(S\) with imports \(\href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^n\), global initializer values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\), and element segment contents \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\), and let \(S'\) be the extended store produced by module allocation.

12. Assert: in allocating \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\), the shared memory actions \(\mathit{act_{\mathrm{m}}}^\ast\) are performed.

13. Let \(F\) be the auxiliary frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

14. Push the frame \(F\) to the stack.

15. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) whose mode is of the form \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\mathit{einstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\), do:

    1. Let \(n\) be the length of the vector \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}\).

    2. Execute the instruction sequence \(\mathit{einstr}^\ast_i\).

    3. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).

    4. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).

    5. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i~i\).

    6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i\).

16. For each element segment \(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}\) whose mode is of the form \(\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}}\), do:

    1. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i\).

17. For each data segment \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i\) in \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}\) whose mode is of the form \(\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\mathit{dinstr}^\ast_i~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \}\), do:

    1. Assert: \(\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i\) is \(0\).

    2. Let \(n\) be the length of the vector \(\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}\).

    3. Execute the instruction sequence \(\mathit{dinstr}^\ast_i\).

    4. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0\).

    5. Execute the instruction \(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n\).

    6. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i\).

    7. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i\).

18. If the start function \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\) is not empty, then:

    1. Let \(\href{../syntax/modules.html#syntax-start}{\mathit{start}}\) be the start function \(\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}\).

    2. Execute the instruction \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}\).

19. Assert: due to validation, the frame \(F\) is now on the top of the stack.

20. Pop the frame \(F\) from the stack.

\[\begin{split}~\\ \begin{array}{l} \begin{array}{@{}rcll} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k) &=& S'; F; \begin{array}[t]{@{}l@{}} (\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{perform}}~(\mathit{act}^?))^k \\ (\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{perform}}~\mathit{act_{\mathrm{m}}}^\ast) \\ \mathrm{runelem}_0(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[0])~\dots~\mathrm{runelem}_{n-1}(\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n[n-1]) \\ \mathrm{rundata}_0(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[0])~\dots~\mathrm{rundata}_{m-1}(\href{../syntax/modules.html#syntax-data}{\mathit{data}}^m[m-1]) \\ (\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}})^? \\ \end{array} \\ &(\mathrel{\mbox{if}} & \href{../valid/modules.html#valid-module}{\vdash} \href{../syntax/modules.html#syntax-module}{\mathit{module}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}}^k \href{../syntax/types.html#syntax-functype}{\rightarrow} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{ex}}^\ast \\ &\wedge& (S; \mathit{act}^? \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^k \\ &\wedge& (\href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}})^k \\[1ex] &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = \href{../syntax/modules.html#syntax-global}{\mathit{global}}^\ast \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{elems}} = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^n \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{datas}} = \href{../syntax/modules.html#syntax-data}{\mathit{data}}^m \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \href{../syntax/modules.html#syntax-start}{\mathit{start}}^? \\ &\wedge& (\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{g}} = \href{../syntax/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{init}})^\ast \\ &\wedge& (\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{e}}^\ast = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}})^n \\[1ex] &\wedge& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \mathit{act_{\mathrm{m}}}^\ast = \href{../exec/modules.html#alloc-module}{\mathrm{allocmodule}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast, (\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^n) \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \} \\[1ex] &\wedge& (S'; F; \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{g}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\ &\wedge& ((S'; F; \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}_{\mathrm{e}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../exec/runtime.html#syntax-ref}{\mathit{ref}}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast)^n) \end{array} \\[1ex] \begin{array}{@{}rcll} \href{../exec/modules.html#exec-instantiation}{\mathrm{instantiate}}(S, \href{../syntax/modules.html#syntax-module}{\mathit{module}}, \href{../exec/runtime.html#syntax-externval}{\mathit{externval}}^k) &=& S; \epsilon; \href{../exec/runtime.html#syntax-trap}{\mathsf{trap}} & (\mathrel{\mbox{otherwise}}) \end{array} \end{array}\end{split}\]

\[\begin{split}~\\[-1ex] \begin{array}{l} \begin{array}{lcl@{\qquad}l} S; F; (\href{../exec/runtime.html#syntax-instr-admin}{\mathsf{perform}}~\mathit{act}^\ast) &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}^{\mathit{act}^\ast}& S; F; \epsilon \end{array} \end{array}\end{split}\]

where:

\[\begin{split}\begin{array}{@{}l} \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{table.init}}~x~i)~(\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i) \\ \mathrm{runelem}_i(\{\href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~\mathit{et}, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}}\}) \quad=\\ \qquad (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~i) \\[1ex] \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}}\}) \quad=\quad \epsilon \\ \mathrm{rundata}_i(\{\href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^n, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}} \{\href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~0, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\}\}) \quad=\\ \qquad \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~0)~(\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory.init}}~i)~(\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{data.drop}}~i) \\ \end{array}\end{split}\]

Note

Module allocation and the evaluation of global initializers and element segments are mutually recursive because the global initialization values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) and element segment contents \((\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast)^\ast\) are passed to the module allocator while depending on the module instance \(\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}\) and store \(S'\) returned by allocation. However, this recursion is just a specification device. In practice, the initialization values can be determined beforehand by staging module allocation such that first, the module’s own function instances are pre-allocated in the store, then the initializer expressions are evaluated, then the rest of the module instance is allocated, and finally the new function instances’ \(\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}\) fields are set to that module instance. This is possible because validation ensures that initialization expressions cannot actually call a function, only take their reference.

All failure conditions are checked before any observable mutation of the store takes place. Store mutation is not atomic; it happens in individual steps that may be interleaved with other threads.

Evaluation of constant expressions does not affect the store.

Invocation

Once a module has been instantiated, any exported function can be invoked externally via its function address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\) in the store \(S\) and an appropriate list \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) of argument values.

Invocation may fail with an error if the arguments do not fit the function type. Invocation can also result in a trap. It is up to the embedder to define how such conditions are reported.

Note

If the embedder API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.

The following steps are performed:

1. Assert: \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\) exists.

2. Let \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}\) be the function instance \(S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]\).

3. Let \([t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m]\) be the function type \(\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}.\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}\).

4. If the length \(|\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast|\) of the provided argument values is different from the number \(n\) of expected arguments, then:

   1. Fail.

5. For each value type \(t_i\) in \(t_1^n\) and corresponding value \(val_i\) in \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\), do:

   1. If \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_i\) is not valid with value type \(t_i\), then:

      1. Fail.

6. Let \(F\) be the dummy frame \(\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}\).

7. Push the frame \(F\) to the stack.

8. Push the values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast\) to the stack.

9. Invoke the function instance at address \(\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}\).

Once the function has returned, the following steps are executed:

1. Assert: due to validation, \(m\) values are on the top of the stack.

2. Pop \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) from the stack.

The values \(\href{../exec/runtime.html#syntax-val}{\mathit{val}}_{\mathrm{res}}^m\) are returned as the results of the invocation.

\[\begin{split}~\\[-1ex] \begin{array}{@{}lcl} \href{../exec/modules.html#exec-invocation}{\mathrm{invoke}}(S, \href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n) &=& S; F; \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n~(\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}) \\ &(\mathrel{\mbox{if}} & S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}].\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}} = [t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^m] \\ &\wedge& (S \href{../appendix/properties.html#valid-val}{\vdash} \href{../exec/runtime.html#syntax-val}{\mathit{val}} : t_1)^n \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}) \\ \end{array}\end{split}\]