diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index e5342259c9..7effb80c5e 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -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} @@ -90,14 +92,20 @@ Limits Memory Types ~~~~~~~~~~~~ -:ref:`Memory types ` are encoded with their :ref:`limits `. +:ref:`Memory types ` are encoded with their :ref:`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 @@ -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} diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 3548a4dd18..128700a366 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -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 ` :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 ` :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 ` :math:`\ETMEM~(\{\LMIN~n, \LMAX~m^?\})`. +* Then :math:`\EVMEM~a` is valid with :ref:`external type ` :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 } @@ -321,11 +321,11 @@ New instances of :ref:`functions `, :ref:`tables ` to allocate. -2. Let :math:`\{\LMIN~n, \LMAX~m^?\}` be the structure of :ref:`memory type ` :math:`\memtype`. +2. Let :math:`\{\LMIN~n, \LMAX~m^?\}~s` be the structure of :ref:`memory type ` :math:`\memtype`. 3. Let :math:`a` be the first free :ref:`memory address ` in :math:`S`. -4. Let :math:`\meminst` be the :ref:`memory instance ` :math:`\{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^? \}` that contains :math:`n` pages of zeroed :ref:`bytes `. +4. Let :math:`\meminst` be the :ref:`memory instance ` :math:`\{ \MIDATA~(\hex{00})^{n \cdot 64\,\F{Ki}}, \MIMAX~m^?, \MISHARE~s\}` that contains :math:`n` pages of zeroed :ref:`bytes `. 5. Append :math:`\meminst` to the |SMEMS| of :math:`S`. @@ -335,9 +335,9 @@ New instances of :ref:`functions `, :ref:`tables `. -It holds a vector of :ref:`bytes ` and an optional maximum size, if one was specified at the definition site of the memory. +It holds a vector of :ref:`bytes ` 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}`. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 57da119cc7..dd7152c00f 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -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 ~~~~~~~~~~~~ @@ -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 `. +The memory type also determines whether this memory is shared. .. index:: ! table type, ! element type, limits, table, element diff --git a/document/core/text/types.rst b/document/core/text/types.rst index de5ed5f308..b381cefc82 100644 --- a/document/core/text/types.rst +++ b/document/core/text/types.rst @@ -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} diff --git a/document/core/util/math.def b/document/core/util/math.def index 3f672fb1e2..05b3252219 100644 --- a/document/core/util/math.def +++ b/document/core/util/math.def @@ -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 @@ -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}} @@ -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}} diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 8fbff90fca..4da9188a68 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -88,8 +88,8 @@ Table Types Memory Types ~~~~~~~~~~~~ -:math:`\limits` -............... +:math:`\limits~\share` +...................... * The limits :math:`\limits` must be :ref:`valid `. @@ -99,7 +99,7 @@ Memory Types \frac{ \vdashlimits \limits \ok }{ - \vdashmemtype \limits \ok + \vdashmemtype \limits~\share \ok } diff --git a/proposals/threads/Overview.md b/proposals/threads/Overview.md index 24a60bdca4..f4175908a3 100644 --- a/proposals/threads/Overview.md +++ b/proposals/threads/Overview.md @@ -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} ```