Skip to content

Commit

Permalink
[spec] Use optional data instance, not data address (WebAssembly#93)
Browse files Browse the repository at this point in the history 
data.drop must update the store, not the frame. There may be multiple
copies of the frame, so any updates will only update once. We can make
sure that all copies are updated by using an indirection through data
addresses and updating the store instead.

See discussion in PR WebAssembly#92.
  • Loading branch information
@binji
binji authored Jun 8, 2019
1 parent 0ee9e67 commit 80aea4a
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 30 deletions.
69 changes: 43 additions & 26 deletions document/core/exec/instructions.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -704,29 +704,31 @@ Memory Instructions

5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[\X{ma}]`.

6. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
6. Assert: due to :ref:`validation <valid-data.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.

7. Let :math:`\X{da}^?` be the optional :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.
7. Let :math:`\X{da}` be the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.

8. If :math:`\X{da}^? = \epsilon`, then:
8. Assert: due to :ref:`validation <valid-data.init>`, :math:`S.\SDATA[\X{da}]` exists.

a. Trap.
9. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.

10. If :math:`\X{data}^? = \epsilon`, then:

9. Let :math:`\X{data}` be the :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[\X{da}]`.
a. Trap.

10. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
11. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

11. Pop the value :math:`\I32.\CONST~n` from the stack.
12. Pop the value :math:`\I32.\CONST~n` from the stack.

12. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
13. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

13. Pop the value :math:`\I32.\CONST~s` from the stack.
14. Pop the value :math:`\I32.\CONST~s` from the stack.

14. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
15. Assert: due to :ref:`validation <valid-memory.init>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.

15. Pop the value :math:`\I32.\CONST~d` from the stack.
16. Pop the value :math:`\I32.\CONST~d` from the stack.

16. If :math:`n` is :math:`0`, then:
17. If :math:`n` is :math:`0`, then:

a. If :math:`d` is larger than the length of :math:`\X{mem}.\MIDATA`, then:

Expand All @@ -736,7 +738,7 @@ Memory Instructions

i. Trap.

17. Else:
18. Else:

a. Push the value :math:`\I32.\CONST~d` to the stack.

Expand All @@ -755,6 +757,7 @@ Memory Instructions
h. Execute the instruction :math:`\MEMORYINIT~x`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~(n+1))~(\MEMORYINIT~x) &\stepto& S; F;
Expand All @@ -765,18 +768,17 @@ Memory Instructions
\end{array} \\
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIDATAS[x] \ne \epsilon \\
\wedge & b = \SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT[s]) \\
(\iff & s < |S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT| \\
\wedge & b = S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT[s]) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\I32.\CONST~d)~(\I32.\CONST~(s)~(\I32.\CONST~0)~(\MEMORYINIT~x) &\stepto& S; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & F.\AMODULE.\MIDATAS[x] \ne \epsilon \\
\wedge & d \leq |\SMEMS[F.\AMODULE.\MIMEMS[0]]| \\
\wedge & s \leq |\SDATA[F.\AMODULE.\MIDATAS[x]]|) \\
(\iff & d \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
\wedge & s \leq |S.\SDATA[F.\AMODULE.\MIDATAS[x]].\DIINIT|) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
Expand All @@ -794,22 +796,37 @@ Memory Instructions

1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.

2. Assert: due to :ref:`validation <valid-memory.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.
2. Assert: due to :ref:`validation <valid-data.init>`, :math:`F.\AMODULE.\MIDATAS[x]` exists.

3. Let :math:`a` be the :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.

3. Let :math:`a^?` be the optional :ref:`data address <syntax-dataaddr>` :math:`F.\AMODULE.\MIDATAS[x]`.
4. Assert: due to :ref:`validation <valid-data.init>`, :math:`S.\SDATA[a]` exists.

4. If :math:`a^? = \epsilon`, then:
5. Let :math:`\X{data}^?` be the optional :ref:`data instance <syntax-datainst>` :math:`S.\SDATA[a]`.

6. If :math:`\X{data}^? = \epsilon`, then:

a. Trap.

5. Replace :math:`F.\AMODULE.\MIDATAS[x]` with :math:`\epsilon`.
7. Replace :math:`S.\SDATA[a]` with :math:`\epsilon`.

.. math::
~\\[-1ex]
\begin{array}{l}
\begin{array}{lcl@{\qquad}l}
F; (\DATADROP~x) &\stepto& F'; \epsilon
& (\iff F' = F \with \AMODULE.\MIDATAS[x] = \epsilon) \\
F; (\DATADROP~x) &\stepto& F; \TRAP
& (\otherwise) \\
S; F; (\DATADROP~x) &\stepto& S'; F; \epsilon
\end{array}
\\ \qquad
\begin{array}[t]{@{}r@{~}l@{}}
(\iff & S.\SDATA[F.\AMODULE.\MIDATAS[x]] \ne \epsilon \\
\wedge & S' = S \with \SDATA[F.\AMODULE.\MIDATAS[x]] = \epsilon) \\
\end{array}
\\[1ex]
\begin{array}{lcl@{\qquad}l}
S; F; (\DATADROP~x) &\stepto& S; F; \TRAP
\end{array}
\\ \qquad
(\otherwise)
\end{array}
Expand Down
11 changes: 7 additions & 4 deletions document/core/exec/runtime.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,9 @@ Store
The *store* represents all global state that can be manipulated by WebAssembly programs.
It consists of the runtime representation of all *instances* of :ref:`functions <syntax-funcinst>`, :ref:`tables <syntax-tableinst>`, :ref:`memories <syntax-meminst>`, and :ref:`globals <syntax-globalinst>`, :ref:`element segments <syntax-eleminst>`, and :ref:`data segments <syntax-datainst>` that have been :ref:`allocated <alloc>` during the life time of the abstract machine. [#gc]_

Element and data segments can be dropped by the owning module, in which case the respective instances are replaced with :math:`\epsilon`.
It is an invariant of the semantics that no element or data instance is :ref:`addressed <syntax-addr>` from anywhere else but the owning module instances.

Syntactically, the store is defined as a :ref:`record <notation-record>` listing the existing instances of each category:

.. math::
Expand All @@ -72,8 +75,8 @@ Syntactically, the store is defined as a :ref:`record <notation-record>` listing
\STABLES & \tableinst^\ast, \\
\SMEMS & \meminst^\ast, \\
\SGLOBALS & \globalinst^\ast, \\
\SELEM & \eleminst^\ast, \\
\SDATA & \datainst^\ast ~\} \\
\SELEM & (\eleminst^?)^\ast, \\
\SDATA & (\datainst^?)^\ast ~\} \\
\end{array}
\end{array}
Expand Down Expand Up @@ -170,8 +173,8 @@ and collects runtime representations of all entities that are imported, defined,
\MITABLES & \tableaddr^\ast, \\
\MIMEMS & \memaddr^\ast, \\
\MIGLOBALS & \globaladdr^\ast, \\
\MIELEMS & (\elemaddr^?)^\ast, \\
\MIDATAS & (\dataaddr^?)^\ast, \\
\MIELEMS & \elemaddr^\ast, \\
\MIDATAS & \dataaddr^\ast, \\
\MIEXPORTS & \exportinst^\ast ~\} \\
\end{array}
\end{array}
Expand Down

0 comments on commit 80aea4a

Please sign in to comment.