[spec] Use optional data instance, not data address (WebAssembly#93)

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.

Author: binji

document/core/exec/instructions.rst

@@ -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:
 
@@ -736,7 +738,7 @@ Memory Instructions
 
        i. Trap.
 
-17. Else:
+18. Else:
 
     a. Push the value :math:`\I32.\CONST~d` to the stack.
 
@@ -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;
@@ -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}
@@ -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}
 
 

document/core/exec/runtime.rst

@@ -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::
@@ -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}
 
@@ -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}