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 be a function instance $\{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \dots\}$.
Then $\href{../exec/runtime.html#syntax-externval}{\mathsf{func}}~a$ is valid with external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}$.

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[a] = \{\href{../exec/runtime.html#syntax-funcinst}{\mathsf{type}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}, \dots\} }{ 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}} }\]

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

The store entry $S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a]$ must be a table instance $\{\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^?\}$.
Then $\href{../exec/runtime.html#syntax-externval}{\mathsf{table}}~a$ is valid with external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}})$.

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a] = \{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\mathit{fa}^?)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \} }{ 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}}~(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathsf{funcref}}) }\]

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

The store entry $S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a]$ must be a memory instance $\{\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^{n\cdot64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^?\}$, for some $n$.
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}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\})$.

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~b^{n\cdot64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \} }{ 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}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\} }\]

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

The store entry $S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a]$ must be a global instance $\{\href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}}\}$.
Then $\href{../exec/runtime.html#syntax-externval}{\mathsf{global}}~a$ is valid with external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t)$.

\[\frac{ S.\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}[a] = \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~(t.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \} }{ 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}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t) }\]

Import Matching¶

When instantiating a module, external values must be provided whose types are matched against the respective external types classifying each import. In some cases, this allows for a simple form of subtyping, as defined below.

Limits¶

Limits $\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \}$ match limits $\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2^? \}$ if and only if:

$n_1$ is larger than or equal to $n_2$.
Either:
- $m_2^?$ is empty.
Or:
- Both $m_1^?$ and $m_2^?$ are non-empty.
- $m_1$ is smaller than or equal to $m_2$.

\[\begin{split}~\\[-1ex] \frac{ n_1 \geq n_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \} \href{../exec/modules.html#match}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~\epsilon \} } \quad \frac{ n_1 \geq n_2 \qquad m_1 \leq m_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1 \} \href{../exec/modules.html#match}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2 \} }\end{split}\]

Functions¶

An external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1$ matches $\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2$ if and only if:

Both $\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1$ and $\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2$ are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\end{split}\]

Tables¶

An external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_1)$ matches $\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_2)$ if and only if:

Limits $\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1$ match $\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2$.
Both $\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_1$ and $\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}_2$ are the same.

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}) \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}}) }\]

Memories¶

An external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1$ matches $\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2$ if and only if:

Limits $\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1$ match $\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2$.

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }\]

Globals¶

An external type $\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1$ matches $\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2$ if and only if:

Both $\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1$ and $\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2$ are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\end{split}\]

Allocation¶

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

Functions ¶

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.
Let $a$ be the first free function address in $S$.
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}}]$.
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}} \}$.
Append $\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}$ to the $\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}$ of $S$.
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 ¶

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.
Let $a$ be the first free function address in $S$.
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}} \}$.
Append $\href{../exec/runtime.html#syntax-funcinst}{\mathit{funcinst}}$ to the $\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}$ of $S$.
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 ¶

Let $\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}$ be the table type to allocate.
Let $(\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}})$ be the structure of table type $\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}$.
Let $a$ be the first free table address in $S$.
Let $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}$ be the table instance $\{ \href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}~(\epsilon)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \}$ with $n$ empty elements.
Append $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}$ to the $\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}$ of $S$.
Return $a$.

\[\begin{split}\begin{array}{rlll} \href{../exec/modules.html#alloc-table}{\mathrm{alloctable}}(S, \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}) &=& 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-elemtype}{\mathit{elemtype}} \\ \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{elem}}~(\epsilon)^n, \href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}~m^? \} \\ 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 ¶

Let $\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}$ be the memory type to allocate.
Let $\{\href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^?\}$ be the structure of memory type $\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}$.
Let $a$ be the first free memory address in $S$.
Let $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}$ be the memory instance $\{ \href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef1219#1{\mathtt{0x#1}}\mathdef1219{00})^{n \cdot 64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \}$ that contains $n$ pages of zeroed bytes.
Append $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}$ to the $\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}$ of $S$.
Return $a$.

\[\begin{split}\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}} \\[1ex] \mbox{where:} \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{../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{data}}~(\def\mathdef1220#1{\mathtt{0x#1}}\mathdef1220{00})^{n \cdot 64\,\mathrm{Ki}}, \href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}~m^? \} \\ 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{split}\]

Globals ¶

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.
Let $\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t$ be the structure of global type $\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}$.
Let $a$ be the first free global address in $S$.
Let $\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}$ be the global instance $\{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \}$.
Append $\href{../exec/runtime.html#syntax-globalinst}{\mathit{globalinst}}$ to the $\href{../exec/runtime.html#syntax-store}{\mathsf{globals}}$ of $S$.
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{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} &=& \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t \\ \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{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}}, \href{../exec/runtime.html#syntax-globalinst}{\mathsf{mut}}~\href{../syntax/types.html#syntax-mut}{\mathit{mut}} \} \\ 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}\]

Growing tables ¶

Let $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}$ be the table instance to grow and $n$ the number of elements by which to grow it.
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}}$.
If $\mathit{len}$ is larger than or equal to $2^{32}$, then fail.
If $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}}$ is not empty and its value is smaller than $\mathit{len}$, then fail.
Append $n$ empty elements to $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}$.

\[\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-tableinst}{\mathit{tableinst}} \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}}~(\epsilon)^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{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}} = \epsilon \vee \mathit{len} \leq \href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{max}})) \\ \end{array} \\ \end{array}\end{split}\]

Growing memories ¶

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.
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}$.
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}$.
If $\mathit{len}$ is larger than $2^{16}$, then fail.
If $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}}$ is not empty and its value is smaller than $\mathit{len}$, then fail.
Append $n$ times $64\,\mathrm{Ki}$ bytes with value $\def\mathdef1221#1{\mathtt{0x#1}}\mathdef1221{00}$ to $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}$.

\[\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{data}} = \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}~(\def\mathdef1222#1{\mathtt{0x#1}}\mathdef1222{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{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}} = \epsilon \vee \mathit{len} \leq \href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}.\href{../exec/runtime.html#syntax-meminst}{\mathsf{max}})) \\ \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, and a list of initialization values for the module’s globals.

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, and $\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast$ the initialization values of the module’s globals.

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.
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{../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}}$.
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$ be the memory address resulting from allocating $\href{../syntax/modules.html#syntax-mem}{\mathit{mem}}_i.\href{../syntax/modules.html#syntax-mem}{\mathsf{type}}$.
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]$.
Let $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}^\ast$ be the the concatenation of the function addresses $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_i$ in index order.
Let $\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}^\ast$ be the the concatenation of the table addresses $\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i$ in index order.
Let $\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\ast$ be the the concatenation of the memory addresses $\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i$ in index order.
Let $\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}^\ast$ be the the concatenation of the global addresses $\href{../exec/runtime.html#syntax-globaladdr}{\mathit{globaladdr}}_i$ in index order.
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$.
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$.
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$.
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$.
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\}$.
Let $\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}^\ast$ be the the concatenation of the export instances $\href{../exec/runtime.html#syntax-exportinst}{\mathit{exportinst}}_i$ in index order.
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\}$.
Return $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}$.

\[\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) &=& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} \end{array}\end{split}\]

where:

\[\begin{split}\begin{array}{rlll} \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{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) \qquad\qquad\qquad~ (\mathrel{\mbox{where}} \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}}) \\ S_3, \href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}^\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) \qquad\qquad\qquad~ (\mathrel{\mbox{where}} \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}}) \\ S', \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) \qquad\quad~ (\mathrel{\mbox{where}} \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{../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 \quad (\mathrel{\mbox{where}} \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-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-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \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-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \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-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \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-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{exports}})) \\ \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), 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 executing the start function. It is up to the embedder to define how such conditions are reported.

If $\href{../syntax/modules.html#syntax-module}{\mathit{module}}$ is not valid, then:
1. Fail.
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.
If the number $m$ of imports is not equal to the number $n$ of provided external values, then:
1. Fail.
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 not valid with an external type $\href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_i$ in store $S$, then:
  1. Fail.
2. 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.

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. Let $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{im}}$ 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)\}$ that only consists of the imported globals.
2. Let $F_{\mathrm{im}}$ be the auxiliary frame $\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}_{\mathrm{im}}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}$.
3. Push the frame $F_{\mathrm{im}}$ to the stack.
4. 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}}$.
5. Assert: due to validation, the frame $F_{\mathrm{im}}$ is now on the top of the stack.
6. Pop the frame $F_{\mathrm{im}}$ from the stack.
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$ and global initializer values $\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast$, and let $S'$ be the extended store produced by module allocation.
Let $F$ be the 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 \}$.
Push the frame $F$ to the stack.
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{elem}}$, do:
1. Let $\mathit{eoval}_i$ be the result of evaluating the expression $\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}$.
2. Assert: due to validation, $\mathit{eoval}_i$ is of the form $\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{eo}_i$.
3. Let $\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i$ be the table index $\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}$.
4. Assert: due to validation, $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i]$ exists.
5. Let $\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i$ be the table address $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[\href{../syntax/modules.html#syntax-tableidx}{\mathit{tableidx}}_i]$.
6. Assert: due to validation, $S'.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i]$ exists.
7. Let $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i$ be the table instance $S'.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}_i]$.
8. Let $\mathit{eend}_i$ be $\mathit{eo}_i$ plus the length of $\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}$.
9. If $\mathit{eend}_i$ is larger than the length of $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}$, then:
  1. Fail.
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{data}}$, do:
1. Let $\mathit{doval}_i$ be the result of evaluating the expression $\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{offset}}$.
2. Assert: due to validation, $\mathit{doval}_i$ is of the form $\href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{do}_i$.
3. Let $\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i$ be the memory index $\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{data}}$.
4. Assert: due to validation, $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i]$ exists.
5. Let $\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i$ be the memory address $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[\href{../syntax/modules.html#syntax-memidx}{\mathit{memidx}}_i]$.
6. Assert: due to validation, $S'.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i]$ exists.
7. Let $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i$ be the memory instance $S'.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}_i]$.
8. Let $\mathit{dend}_i$ be $\mathit{do}_i$ plus the length of $\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}$.
9. If $\mathit{dend}_i$ is larger than the length of $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}$, then:
  1. Fail.
Assert: due to validation, the frame $F$ is now on the top of the stack.
Pop the frame from the stack.
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{elem}}$, do:
1. For each function index $\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}$ in $\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}_i.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}$ (starting with $j = 0$), do:
  1. Assert: due to validation, $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}]$ exists.
  2. Let $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{ij}$ be the function address $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-funcidx}{\mathit{funcidx}}_{ij}]$.
  3. Replace $\href{../exec/runtime.html#syntax-tableinst}{\mathit{tableinst}}_i.\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[\mathit{eo}_i + j]$ with $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}_{ij}$.
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{data}}$, do:
1. For each byte $b_{ij}$ in $\href{../syntax/modules.html#syntax-data}{\mathit{data}}_i.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}$ (starting with $j = 0$), do:
  1. Replace $\href{../exec/runtime.html#syntax-meminst}{\mathit{meminst}}_i.\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[\mathit{do}_i + j]$ with $b_{ij}$.
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. Assert: due to validation, $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}]$ exists.
2. Let $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}$ be the function address $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}]$.
3. Invoke the function instance at $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}$.

\[\begin{split}~\\ \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}}^n) &=& S'; F; \begin{array}[t]{@{}l@{}} (\href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}~\mathit{eo}~\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}})^\ast \\ (\href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}~\mathit{do}~\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{init}})^\ast \\ (\href{../exec/runtime.html#syntax-invoke}{\mathsf{invoke}}~\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}})^? \\ \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}}^n \href{../syntax/types.html#syntax-functype}{\rightarrow} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{ex}}^\ast \\ &\wedge& (S \href{../exec/modules.html#valid-externval}{\vdash} \href{../exec/runtime.html#syntax-externval}{\mathit{externval}} : \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}})^n \\ &\wedge& (\href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}} \href{../exec/modules.html#match}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathit{externtype}}_{\mathrm{im}})^n \\[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{elem}} = \href{../syntax/modules.html#syntax-elem}{\mathit{elem}}^\ast \\ &\wedge& \href{../syntax/modules.html#syntax-module}{\mathit{module}}.\href{../syntax/modules.html#syntax-module}{\mathsf{data}} = \href{../syntax/modules.html#syntax-data}{\mathit{data}}^\ast \\ &\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}}^? \\[1ex] &\wedge& S', \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}} = \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}}^n, \href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast) \\ &\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/modules.html#syntax-global}{\mathit{global}}.\href{../syntax/modules.html#syntax-global}{\mathsf{init}} \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/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{offset}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{eo}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\ &\wedge& (S'; F; \href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{offset}} \href{../exec/conventions.html#formal-notation}{\hookrightarrow}^\ast S'; F; \href{../syntax/types.html#syntax-valtype}{\mathsf{i32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{do}~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}})^\ast \\[1ex] &\wedge& (\mathit{eo} + |\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{init}}| \leq |S'.\href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}}].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}|)^\ast \\ &\wedge& (\mathit{do} + |\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{init}}| \leq |S'.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}}].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}|)^\ast \\[1ex] &\wedge& (\href{../exec/runtime.html#syntax-tableaddr}{\mathit{tableaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{tableaddrs}}[\href{../syntax/modules.html#syntax-elem}{\mathit{elem}}.\href{../syntax/modules.html#syntax-elem}{\mathsf{table}}])^\ast \\ &\wedge& (\href{../exec/runtime.html#syntax-memaddr}{\mathit{memaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{memaddrs}}[\href{../syntax/modules.html#syntax-data}{\mathit{data}}.\href{../syntax/modules.html#syntax-data}{\mathsf{data}}])^\ast \\ &\wedge& (\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}} = \href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[\href{../syntax/modules.html#syntax-start}{\mathit{start}}.\href{../syntax/modules.html#syntax-start}{\mathsf{func}}])^?) \\[2ex] S; F; \href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~a~i~\epsilon &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S; F; \epsilon \\ S; F; \href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~a~i~(x_0~x^\ast) &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S'; F; \href{../exec/runtime.html#syntax-init-elem}{\mathsf{init\_elem}}~a~(i+1)~x^\ast \\ && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{tables}}[a].\href{../exec/runtime.html#syntax-tableinst}{\mathsf{elem}}[i] = F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{funcaddrs}}[x_0]) \\[1ex] S; F; \href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~a~i~\epsilon &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S; F; \epsilon \\ S; F; \href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~a~i~(b_0~b^\ast) &\href{../exec/conventions.html#formal-notation}{\hookrightarrow}& S'; F; \href{../exec/runtime.html#syntax-init-data}{\mathsf{init\_data}}~a~(i+1)~b^\ast \\ && (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a].\href{../exec/runtime.html#syntax-meminst}{\mathsf{data}}[i] = b_0) \end{array}\end{split}\]

Note

Module allocation and the evaluation of global initializers are mutually recursive because the global initialization values $\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast$ are passed to the module allocator but depend on the store $S'$ and module instance $\href{../exec/runtime.html#syntax-moduleinst}{\mathit{moduleinst}}$ returned by allocation. However, this recursion is just a specification device. Due to validation, the initialization values can easily be determined from a simple pre-pass that evaluates global initializers in the initial store.

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:

Assert: $S.\href{../exec/runtime.html#syntax-store}{\mathsf{funcs}}[\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}]$ exists.
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}}]$.
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}}$.
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.
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 $t_i.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c_i$ for some $c_i$, then:
  1. Fail.
Let $F$ be the dummy frame $\{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}$.
Push the frame $F$ to the stack.
Push the values $\href{../exec/runtime.html#syntax-val}{\mathit{val}}^\ast$ to the stack.
Invoke the function instance at address $\href{../exec/runtime.html#syntax-funcaddr}{\mathit{funcaddr}}$.

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

Assert: due to validation, $m$ values are on the top of the stack.
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& \href{../exec/runtime.html#syntax-val}{\mathit{val}}^n = (t_1.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~c)^n \\ &\wedge& F = \{ \href{../exec/runtime.html#syntax-frame}{\mathsf{module}}~\{\}, \href{../exec/runtime.html#syntax-frame}{\mathsf{locals}}~\epsilon \}) \\ \end{array}\end{split}\]

Navigation

Modules¶

External Typing¶

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

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

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

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

Import Matching¶

Limits¶

Functions¶

Tables¶

Memories¶

Globals¶

Allocation¶

Functions ¶

Host Functions ¶

Tables ¶

Memories ¶

Globals ¶

Growing tables ¶

Growing memories ¶

Modules ¶

Instantiation¶

Invocation¶

Modules¶

External Typing¶

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

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

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

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

Import Matching¶

Limits¶

Functions¶

Tables¶

Memories¶

Globals¶

Allocation¶

Functions¶

Host Functions¶

Tables¶

Memories¶

Globals¶

Growing tables¶

Growing memories¶

Modules¶

Instantiation¶

Invocation¶

Functions ¶

Host Functions ¶

Tables ¶

Memories ¶

Globals ¶

Growing tables ¶

Growing memories ¶

Modules ¶