Skip to content

Commit

Permalink
Add share flag to memtype (WebAssembly#58)
Browse files Browse the repository at this point in the history
* Add `share` flag to `memtype`

* Rename notshared -> unshared, fix some nits

* Return multiple values from limit
  • Loading branch information
binji committed Aug 30, 2017
1 parent 5b6ef61 commit 8539394
Show file tree
Hide file tree
Showing 8 changed files with 42 additions and 24 deletions.
18 changes: 13 additions & 5 deletions document/core/binary/types.rst
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,10 @@ Limits
.. math::
\begin{array}{llclll}
\production{limits} & \Blimits &::=&
\hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|&
\hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\
\hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \}, 0 \\ &&|&
\hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \}, 0 \\ &&|&
\hex{02}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \}, 1 \\ &&|&
\hex{03}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \}, 1 \\
\end{array}
Expand All @@ -90,14 +92,20 @@ Limits
Memory Types
~~~~~~~~~~~~

:ref:`Memory types <syntax-memtype>` are encoded with their :ref:`limits <binary-limits>`.
:ref:`Memory types <syntax-memtype>` are encoded with their :ref:`limits <binary-limits>` that includes an extra value to specify whether the the memory is shared.

.. math::
\begin{array}{llclll@{\qquad\qquad}l}
\production{memory type} & \Bmemtype &::=&
\X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\
\X{lim},0{:}\Blimits &\Rightarrow& \X{lim}~\MUNSHARED \\ &&|&
\X{lim},1{:}\Blimits &\Rightarrow& \X{lim}~\MSHARED
\qquad (\iff lim.\LMAX \ne \epsilon) \\
\end{array}
.. note::
Shared storage requires a maximum size to be specified. In future versions
of WebAssembly, shared storage without a maximum size may be allowed.


.. index:: table type, element type, limits
pair: binary format; table type
Expand All @@ -113,7 +121,7 @@ Table Types
.. math::
\begin{array}{llclll}
\production{table type} & \Btabletype &::=&
\X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
\X{et}{:}\Belemtype~~\X{lim},0{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\
\production{element type} & \Belemtype &::=&
\hex{70} &\Rightarrow& \ANYFUNC \\
\end{array}
Expand Down
16 changes: 8 additions & 8 deletions document/core/exec/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -59,15 +59,15 @@ The following auxiliary typing rules specify this typing relation relative to a
:math:`\EVMEM~a`
................

* The store entry :math:`S.\SMEMS[a]` must be a :ref:`memory instance <syntax-meminst>` :math:`\{\MIDATA~b^{n\cdot64\,\F{Ki}}, \MIMAX~m^?\}`, for some :math:`n`.
* The store entry :math:`S.\SMEMS[a]` must be a :ref:`memory instance <syntax-meminst>` :math:`\{\MIDATA~b^{n\cdot64\,\F{Ki}}, \MIMAX~m^?, \MISHARE~s\}`, for some :math:`n`.

* Then :math:`\EVMEM~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETMEM~(\{\LMIN~n, \LMAX~m^?\})`.
* Then :math:`\EVMEM~a` is valid with :ref:`external type <syntax-externtype>` :math:`\ETMEM~(\{\LMIN~n, \LMAX~m^?\}~s)`.

.. math::
\frac{
S.\SMEMS[a] = \{ \MIDATA~b^{n\cdot64\,\F{Ki}}, \MIMAX~m^? \}
S.\SMEMS[a] = \{ \MIDATA~b^{n\cdot64\,\F{Ki}}, \MIMAX~m^?, \MISHARE~s\}
}{
S \vdashexternval \EVMEM~a : \ETMEM~\{\LMIN~n, \LMAX~m^?\}
S \vdashexternval \EVMEM~a : \ETMEM~\{\LMIN~n, \LMAX~m^?\}~s
}
Expand Down Expand Up @@ -321,11 +321,11 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei

1. Let :math:`\memtype` be the :ref:`memory type <syntax-memtype>` to allocate.

2. Let :math:`\{\LMIN~n, \LMAX~m^?\}` be the structure of :ref:`memory type <syntax-memtype>` :math:`\memtype`.
2. Let :math:`\{\LMIN~n, \LMAX~m^?\}~s` be the structure of :ref:`memory type <syntax-memtype>` :math:`\memtype`.

3. Let :math:`a` be the first free :ref:`memory address <syntax-memaddr>` in :math:`S`.

4. Let :math:`\meminst` be the :ref:`memory instance <syntax-meminst>` :math:`\{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^? \}` that contains :math:`n` pages of zeroed :ref:`bytes <syntax-byte>`.
4. Let :math:`\meminst` be the :ref:`memory instance <syntax-meminst>` :math:`\{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^?, \MISHARE~s\}` that contains :math:`n` pages of zeroed :ref:`bytes <syntax-byte>`.

5. Append :math:`\meminst` to the |SMEMS| of :math:`S`.

Expand All @@ -335,9 +335,9 @@ New instances of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tablei
\begin{array}{rlll}
\allocmem(S, \memtype) &=& S', \memaddr \\[1ex]
\mbox{where:} \hfill \\
\memtype &=& \{\LMIN~n, \LMAX~m^?\} \\
\memtype &=& \{\LMIN~n, \LMAX~m^?\}~s \\
\memaddr &=& |S.\SMEMS| \\
\meminst &=& \{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^? \} \\
\meminst &=& \{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^?, \MISHARE~s\} \\
S' &=& S \compose \{\SMEMS~\meminst\} \\
\end{array}
Expand Down
4 changes: 2 additions & 2 deletions document/core/exec/runtime.rst
Original file line number Diff line number Diff line change
Expand Up @@ -217,12 +217,12 @@ Memory Instances
~~~~~~~~~~~~~~~~

A *memory instance* is the runtime representation of a linear :ref:`memory <syntax-mem>`.
It holds a vector of :ref:`bytes <syntax-byte>` and an optional maximum size, if one was specified at the definition site of the memory.
It holds a vector of :ref:`bytes <syntax-byte>` and an optional maximum size, if one was specified at the definition site of the memory. It also contains a flag for whether the memory can be shared.

.. math::
\begin{array}{llll}
\production{(memory instance)} & \meminst &::=&
\{ \MIDATA~\vec(\byte), \MIMAX~\u32^? \} \\
\{ \MIDATA~\vec(\byte), \MIMAX~\u32^?, \MISHARE~\share \} \\
\end{array}
The length of the vector always is a multiple of the WebAssembly *page size*, which is defined to be the constant :math:`65536` -- abbreviated :math:`64\,\F{Ki}`.
Expand Down
9 changes: 7 additions & 2 deletions document/core/syntax/types.rst
Original file line number Diff line number Diff line change
Expand Up @@ -105,11 +105,12 @@ Limits
If no maximum is given, the respective storage can grow to any size.


.. index:: ! memory type, limits, page size, memory
.. index:: ! memory type, limits, page size, memory, share
pair: abstract syntax; memory type
pair: memory; type
pair: memory; limits
.. _syntax-memtype:
.. _syntax-share:

Memory Types
~~~~~~~~~~~~
Expand All @@ -119,11 +120,15 @@ Memory Types
.. math::
\begin{array}{llll}
\production{memory type} & \memtype &::=&
\limits \\
\limits~\share \\
\production{share} & \share &::=&
\MSHARED ~|~
\MUNSHARED \\
\end{array}
The limits constrain the minimum and optionally the maximum size of a memory.
The limits are given in units of :ref:`page size <page-size>`.
The memory type also determines whether this memory is shared.


.. index:: ! table type, ! element type, limits, table, element
Expand Down
3 changes: 2 additions & 1 deletion document/core/text/types.rst
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,8 @@ Memory Types
.. math::
\begin{array}{llclll@{\qquad\qquad}l}
\production{memory type} & \Tmemtype &::=&
\X{lim}{:}\Tlimits &\Rightarrow& \X{lim} \\
\X{lim}{:}\Tlimits &\Rightarrow& \X{lim}~\MUNSHARED \\ &&|&
\text{(}~\text{shared}~~\X{lim}{:}\Tlimits~~\text{)} &\Rightarrow& \X{lim}~\MSHARED \\
\end{array}
Expand Down
4 changes: 4 additions & 0 deletions document/core/util/math.def
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,8 @@
.. |ETMEM| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{mem}}
.. |ETGLOBAL| mathdef:: \xref{syntax/types}{syntax-externtype}{\K{global}}

.. |MSHARED| mathdef:: \xref{syntax/types}{syntax-memtype}{\K{shared}}
.. |MUNSHARED| mathdef:: \xref{syntax/types}{syntax-memtype}{\K{unshared}}

.. Types, non-terminals

Expand All @@ -148,6 +150,7 @@
.. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}}

.. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}}
.. |share| mathdef:: \xref{syntax/types}{syntax-share}{\X{share}}
.. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}}

.. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}}
Expand Down Expand Up @@ -750,6 +753,7 @@

.. |MIDATA| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{data}}
.. |MIMAX| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{max}}
.. |MISHARE| mathdef:: \xref{exec/runtime}{syntax-meminst}{\K{share}}

.. |GIVALUE| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{value}}
.. |GIMUT| mathdef:: \xref{exec/runtime}{syntax-globalinst}{\K{mut}}
Expand Down
6 changes: 3 additions & 3 deletions document/core/valid/types.rst
Original file line number Diff line number Diff line change
Expand Up @@ -88,8 +88,8 @@ Table Types
Memory Types
~~~~~~~~~~~~

:math:`\limits`
...............
:math:`\limits~\share`
......................

* The limits :math:`\limits` must be :ref:`valid <valid-limits>`.

Expand All @@ -99,7 +99,7 @@ Memory Types
\frac{
\vdashlimits \limits \ok
}{
\vdashmemtype \limits \ok
\vdashmemtype \limits~\share \ok
}
Expand Down
6 changes: 3 additions & 3 deletions proposals/threads/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -541,14 +541,14 @@ the linear memory or table is shared:

```
limits ::= {min u32, max u32?, share}
share ::= notshared | shared
share ::= unshared | shared
```

Its [encoding][limits encoding] is as follows:

```
limits ::= 0x00 n:u32 => {min n, max e, notshared}
0x01 n:u32 m:u32 => {min n, max m, notshared}
limits ::= 0x00 n:u32 => {min n, max e, unshared}
0x01 n:u32 m:u32 => {min n, max m, unshared}
0x03 n:u32 m:u32 => {min n, max m, shared}
```

Expand Down

0 comments on commit 8539394

Please sign in to comment.