more work on host function and action definitions

Author: conrad-watt

document/core/appendix/properties.rst

@@ -156,52 +156,17 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * The :ref:`function type <syntax-functype>` :math:`\functype` must be :ref:`valid <valid-functype>`.
 
-* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type <syntax-functype>` :math:`\functype`.
-
-* For every :ref:`valid <valid-store>` :ref:`store <syntax-store>` :math:`S_1` :ref:`extending <extend-store>` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values <syntax-val>` whose :ref:`types <valid-val>` coincide with :math:`t_1^\ast`:
-
-  * :ref:`Executing <exec-invoke-host>` :math:`\X{hf}` in store :math:`S_1` with arguments :math:`\val^\ast` has a non-empty set of possible outcomes.
-
-  * For every element :math:`R` of this set:
-
-    * Either :math:`R` must be :math:`\bot` (i.e., divergence).
-
-    * Or :math:`R` consists of a :ref:`valid <valid-store>` :ref:`store <syntax-store>` :math:`S_2` :ref:`extending <extend-store>` :math:`S_1` and a :ref:`result <syntax-result>` :math:`\result` whose :ref:`type <valid-result>` coincides with :math:`[t_2^\ast]`.
-
 * Then the function instance is valid with :ref:`function type <syntax-functype>` :math:`\functype`.
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
      \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\
      \end{array}
-     \quad
-     \begin{array}[b]{@{}l@{}}
-     \forall S_1, \val^\ast,~
-       {\vdashstore S_1 \ok} \wedge
-       {\vdashstoreextends S \extendsto S_1} \wedge
-       {S_1 \vdashresult \val^\ast : [t_1^\ast]}
-       \Longrightarrow {} \\ \qquad
-       \X{hf}(S_1; \val^\ast) \supset \emptyset \wedge {} \\ \qquad
-     \forall R \in \X{hf}(S_1; \val^\ast),~
-       R = \bot \vee {} \\ \qquad\qquad
-       \exists S_2, \result,~
-       {\vdashstore S_2 \ok} \wedge
-       {\vdashstoreextends S_1 \extendsto S_2} \wedge
-       {S_2 \vdashresult \result : [t_2^\ast]} \wedge
-       R = (S_2; \result)
-     \end{array}
    }{
      S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTCODE~\X{hf}\} : [t_1^\ast] \to [t_2^\ast]
    }
 
-.. note::
-   This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results.
-   The post-conditions match the ones in the :ref:`execution rule <exec-invoke-host>` for invoking host functions.
-
-   Any store under which the function is invoked is assumed to be an extension of the current store.
-   That way, the function itself is able to make sufficient assumptions about future stores.
-
 
 .. index:: table type, table instance, limits, function address
 .. _valid-tableinst:

document/core/exec/instructions.rst

@@ -4149,9 +4149,7 @@ During its execution, a host function call may do any of the following.
 - Terminate with a list of values that respects the host function's type annotation.
 - Terminate with a trap.
 
-.. todo:: better prose
-
-.. todo:: reconcile with old-style host function formulation
+.. todo:: better prose, evaluate alternative approach where host may directly emit shared memory events
 
 .. math::
    ~\\[-1ex]
@@ -4189,20 +4187,6 @@ During its execution, a host function call may do any of the following.
    \end{array}
    \end{array}
 
-.. todo:: reconcile with old-style host function formulation
-
-Here, :math:`\X{hf}(S; \val^n)` denotes the implementation-defined execution of host function :math:`\X{hf}` in current store :math:`S` with arguments :math:`\val^n`.
-It yields a set of possible outcomes, where each element is either a pair of a modified store :math:`S'` and a :ref:`result <syntax-result>`
-or the special value :math:`\bot` indicating divergence.
-A host function is non-deterministic if there is at least one argument for which the set of outcomes is not singular.
-
-For a WebAssembly implementation to be :ref:`sound <soundness>` in the presence of host functions,
-every :ref:`host function instance <syntax-funcinst>` must be :ref:`valid <valid-hostfuncinst>`,
-which means that it adheres to suitable pre- and post-conditions:
-under a :ref:`valid store <valid-store>` :math:`S`, and given arguments :math:`\val^n` matching the ascribed parameter types :math:`t_1^n`,
-executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store :math:`S'` that is an :ref:`extension <extend-store>` of :math:`S` and a result matching the ascribed return types :math:`t_2^m`.
-All these notions are made precise in the :ref:`Appendix <soundness>`.
-
 .. note::
    A host function can call back into WebAssembly by :ref:`invoking <exec-invocation>` a function :ref:`exported <syntax-export>` from a :ref:`module <syntax-module>`.
    However, the effects of any such call are subsumed by the non-deterministic behavior allowed for the host function.

document/core/exec/modules.rst

@@ -658,11 +658,15 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
 4. For each :ref:`external value <syntax-externval>` :math:`\externval_i` in :math:`\externval^n` and :ref:`external type <syntax-externtype>` :math:`\externtype'_i` in :math:`\externtype_{\F{im}}^n`, do:
 
-   a. If :math:`\externval_i` is not :ref:`valid <valid-externval>` with an :ref:`external type <syntax-externtype>` :math:`\externtype_i` in store :math:`S`, then:
+   a. If :math:`\externval_i` is :ref:`valid <valid-externval>` with an :ref:`external type <syntax-externtype>` :math:`\externtype_i` in store :math:`S`, then:
+
+      i. Assert: in checking the validity of :math:`\externval_i`, the :ref:`shared memory actions <syntax-act>` :math:`\X{act}_i^?` are performed.
+
+   b. Else:
 
       i. Fail.
 
-   b. If :math:`\externtype_i` does not :ref:`match <match-externtype>` :math:`\externtype'_i`, then:
+   c. If :math:`\externtype_i` does not :ref:`match <match-externtype>` :math:`\externtype'_i`, then:
 
       i. Fail.
 
@@ -698,11 +702,13 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
 11. Let :math:`\moduleinst` be a new module instance :ref:`allocated <alloc-module>` from :math:`\module` in store :math:`S` with imports :math:`\externval^n`, global initializer values :math:`\val^\ast`, and element segment contents :math:`(\reff^\ast)^\ast`, and let :math:`S'` be the extended store produced by module allocation.
 
-12. Let :math:`F` be the auxiliary :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`.
+12. Assert: in allocating :math:`\moduleinst`, the :ref:`shared memory actions <syntax-act>` :math:`\X{act_{\F{m}}}^\ast` are performed.
+
+13. Let :math:`F` be the auxiliary :ref:`frame <syntax-frame>` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`.
 
-13. Push the frame :math:`F` to the stack.
+14. Push the frame :math:`F` to the stack.
 
-14. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do:
+15. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EACTIVE~\{ \ETABLE~\tableidx_i, \EOFFSET~\X{einstr}^\ast_i~\END \}`, do:
 
     a. Let :math:`n` be the length of the vector :math:`\elem_i.\EINIT`.
 
@@ -716,11 +722,11 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
     f. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.
 
-15. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARATIVE`, do:
+16. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARATIVE`, do:
 
     a. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.
 
-16. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode <syntax-datamode>` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do:
+17. For each :ref:`data segment <syntax-data>` :math:`\data_i` in :math:`\module.\MDATAS` whose :ref:`mode <syntax-datamode>` is of the form :math:`\DACTIVE~\{ \DMEM~\memidx_i, \DOFFSET~\X{dinstr}^\ast_i~\END \}`, do:
 
     a. Assert: :math:`\memidx_i` is :math:`0`.
 
@@ -736,15 +742,15 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
 
     g. :ref:`Execute <exec-data.drop>` the instruction :math:`\DATADROP~i`.
 
-17. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:
+18. If the :ref:`start function <syntax-start>` :math:`\module.\MSTART` is not empty, then:
 
     a. Let :math:`\start` be the :ref:`start function <syntax-start>` :math:`\module.\MSTART`.
 
     b. :ref:`Execute <exec-call>` the instruction :math:`\CALL~\start.\SFUNC`.
 
-18. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
+19. Assert: due to :ref:`validation <valid-module>`, the frame :math:`F` is now on the top of the stack.
 
-19. Pop the frame :math:`F` from the stack.
+20. Pop the frame :math:`F` from the stack.
 
 
 .. math::
@@ -753,7 +759,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep
    \begin{array}{@{}rcll}
    \instantiate(S, \module, \externval^k) &=& S'; F;
      \begin{array}[t]{@{}l@{}}
-     (\PERFORM~(\X{act}^?)^k) \\
+     (\PERFORM~(\X{act}^?))^k \\
      (\PERFORM~\X{act_{\F{m}}}^\ast) \\
      \F{runelem}_0(\elem^n[0])~\dots~\F{runelem}_{n-1}(\elem^n[n-1]) \\
      \F{rundata}_0(\data^m[0])~\dots~\F{rundata}_{m-1}(\data^m[m-1]) \\

document/core/exec/relaxed.rst

@@ -40,11 +40,9 @@ Preliminary Definitions
    \tearfreeact \ldots & = & \ldots \\
    \sameact \ldots & = & \ldots \\
    \\
-   \X{func}_{\loc}(\evt) \ldots & = & \X{func}(\act) \ldots \\
+   \X{func}_{\reg}(\evt) \ldots & = & \X{func}(\act) \ldots \\
    \end{array}
 
-.. todo:: need to refactor len+data in actions
-
 
 .. _relaxed-trace:
 
@@ -76,97 +74,97 @@ Consistency
 
 .. math::
    \frac{
-     \forall \loc, \, \vdash_{\loc} \X{tr} \consistentwith
+     \forall \reg, \, \vdash_{\reg} \X{tr} \consistentwith
    }{
      \vdash \X{tr} \consistent
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
-       \forall \evt_R \in \readingact_{\loc}(\X{tr}), \exists \evt_W^\ast,
-         \X{tr} \vdash_{\loc} \evt_R \readseachfrom \evt_W^\ast \\
+       \forall \evt_R \in \readingact_{\reg}(\X{tr}), \exists \evt_W^\ast,
+         \X{tr} \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\
        \forall \evt_I, \evt \in \X{tr}, \,
-         \ordact_{\loc}(\evt_I) = \INIT \wedge
+         \ordact_{\reg}(\evt_I) = \INIT \wedge
          \evt_I \neq \evt \wedge
          \overlapact(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt
      \end{array}
    }{
-     \vdash_{\loc} \X{tr} \consistentwith
+     \vdash_{\reg} \X{tr} \consistentwith
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}c@{}}
-       \left|\evt_W^\ast\right| = |\readact_{\loc}(\evt_R)| \\
+       \left|\evt_W^\ast\right| = |\readact_{\reg}(\evt_R)| \\
        \forall i < |\evt_W^\ast|,
-         \X{tr} \vdash_{\loc}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
+         \X{tr} \vdash_{\reg}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
        \\
-       \vdash_{\loc} \evt_R \notear \evt_W^\ast
+       \vdash_{\reg} \evt_R \notear \evt_W^\ast
      \end{array}
    }{
-     \X{tr} \vdash_{\loc} \evt_R \readseachfrom \evt_W^\ast
+     \X{tr} \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
        \evt_R \neq \evt_W \\
-       \evt_W \in \writingact_{\loc}(\X{tr})
+       \evt_W \in \writingact_{\reg}(\X{tr})
      \end{array}
      \qquad
      \begin{array}[b]{@{}r@{}}
-       \X{tr} \vdash_{\loc}^{i,k} \evt_R \valueconsistent \evt_W \\
-       \X{tr} \vdash_{\loc}^k \evt_R \hbconsistent \evt_W
+       \X{tr} \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W \\
+       \X{tr} \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
      \end{array}
      \qquad
-     \X{tr} \vdash_{\loc} \evt_R \sclastvisible \evt^\ast_W
+     \X{tr} \vdash_{\reg} \evt_R \sclastvisible \evt^\ast_W
    }{
-     \X{tr} \vdash_{\loc}^i \evt_R \readsfrom \evt_W
+     \X{tr} \vdash_{\reg}^i \evt_R \readsfrom \evt_W
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}r@{~}c@{~}l@{}}
-       \readact_{\loc}(\evt_R)[i] &=& \writeact_{\loc}(\evt_W)[j] \\
-       k = \offsetact_{\loc}(\evt_R) + i &=& \offsetact_{\loc}(\evt_W) + j
+       \readact_{\reg}(\evt_R)[i] &=& \writeact_{\reg}(\evt_W)[j] \\
+       k = \offsetact_{\reg}(\evt_R) + i &=& \offsetact_{\reg}(\evt_W) + j
      \end{array}
   }{
-     \X{tr} \vdash_{\loc}^{i,k} \evt_R \valueconsistent \evt_W
+     \X{tr} \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W
   }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}c}
        \neg (\evt_R \prechb \evt_W) \\
-       \syncact_{\loc}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R
+       \syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R
      \end{array}
     \qquad
     \begin{array}[b]{@{}l@{}}
-      \forall \evt'_W \in \writingact_{\loc}(\X{tr}),\\
-      \quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\loc}(\evt'_W)
+      \forall \evt'_W \in \writingact_{\reg}(\X{tr}),\\
+      \quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W)
     \end{array}
    }{
-    \X{tr} \vdash_{\loc}^k \evt_R \hbconsistent \evt_W
+    \X{tr} \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{\qquad}l@{}}
-       \forall \evt'_W \in \writingact_{\loc}(\X{tr}), \evt_W \prechb \evt_R \Rightarrow \\
-       \quad \evt_W \prectot \evt'_W \prectot \evt_R \wedge \syncact_{\loc}(\evt_W, \evt_R) \Rightarrow \neg \syncact_{\loc}(\evt'_W, \evt_R) \\
-       \quad \evt_W \prechb \evt'_W \prectot \evt_R  \Rightarrow \neg\syncact_{\loc}(\evt'_W, \evt_R) \\
-       \quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\syncact_{\loc}(\evt_W, \evt'_W)
+       \forall \evt'_W \in \writingact_{\reg}(\X{tr}), \evt_W \prechb \evt_R \Rightarrow \\
+       \quad \evt_W \prectot \evt'_W \prectot \evt_R \wedge \syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \neg \syncact_{\reg}(\evt'_W, \evt_R) \\
+       \quad \evt_W \prechb \evt'_W \prectot \evt_R  \Rightarrow \neg\syncact_{\reg}(\evt'_W, \evt_R) \\
+       \quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\syncact_{\reg}(\evt_W, \evt'_W)
      \end{array}
    }{
-     \X{tr} \vdash_{\loc} \evt_R \sclastvisible \evt_W
+     \X{tr} \vdash_{\reg} \evt_R \sclastvisible \evt_W
    }
 
 .. math::
    \frac{
-     \tearfreeact_{\loc}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\loc}(\evt_R, \evt_W) \wedge \tearfreeact_{\loc}(\evt_W)\}| \leq 1
+     \tearfreeact_{\reg}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\reg}(\evt_R, \evt_W) \wedge \tearfreeact_{\reg}(\evt_W)\}| \leq 1
    }{
-     \vdash_{\loc} \evt_R \notear \evt_W^\ast
+     \vdash_{\reg} \evt_R \notear \evt_W^\ast
    }
 
 

document/core/exec/runtime.rst

@@ -666,6 +666,7 @@ This definition allows to index active labels surrounding a :ref:`branch <syntax
 .. _syntax-act:
 .. _syntax-ord:
 .. _syntax-loc:
+.. _syntax-reg:
 .. _syntax-fld:
 .. _syntax-storeval:
 
@@ -697,10 +698,12 @@ Each event is annotated with a :ref:`time stamp <syntax-time>` that uniquely ide
      \SEQCST ~|~
      \INIT \\
    \production{(location)} & \loc &::=&
+     \reg[\u32] \\
+   \production{(region)} & \reg &::=&
      \addr.\fld \\
    \production{(field)} & \fld &::=&
      \LLEN ~|~
-     \LDATA[\u32] \\
+     \LDATA \\
    \production{(store value)} & \storeval &::=&
      \val ~|~
      b^\ast \\
@@ -710,8 +713,7 @@ Each event is annotated with a :ref:`time stamp <syntax-time>` that uniquely ide
 .. todo:: remove spawn from events in a typed way?
 
 The access of *mutable* shared state is performed through the |ARD|, |AWR|, and |ARMW| actions.
-Each action accesses an abstract *location*, which consists of an :ref:`address <syntax-addr>` of a :ref:`shared <syntax-shared>` :ref:`memory <syntax-meminst>` instance and a symbolic *field* name in the respective object.
-This is either |LLEN| for the size or |LDATA| for the vector of bytes.
+Each action accesses an abstract *location*, which consists of an :ref:`address <syntax-addr>` of a :ref:`shared <syntax-shared>` :ref:`memory <syntax-meminst>` instance, a symbolic *field* name in the respective object (either |LLEN| for the size or |LDATA| for the vector of bytes), and an offset index into the field.
 
 In each case, read and write actions record the *store value* that has been read or written, which is either a regular :ref:`value <syntax-val>` or a sequence of :ref:`bytes <syntax-byte>`, depending on the location accessed.
 An |ARMW| event, performing an atomic read-modify-write access, records both the store values read (first) and written (second);
@@ -736,6 +738,8 @@ Conventions
 
 * The actions :math:`\ARD_{\ord}` and :math:`\AWR_{\ord}` are abbreviated to just :math:`\ARD` and :math:`\AWR` when :math:`\ord` is :math:`\UNORD`.
 
+* A location may syntactically elide its :math:`[\u32]` offset in the case that it is 0.
+
 The following auxiliary definition is used to classify whether an access will *tear*.
 
 .. math::

document/core/util/macros.def

@@ -1106,6 +1106,7 @@
 .. |hostact| mathdef:: \xref{exec/runtime}{syntax-act}{\X{hostact}}
 .. |ord| mathdef:: \xref{exec/runtime}{syntax-ord}{\X{ord}}
 .. |loc| mathdef:: \xref{exec/runtime}{syntax-loc}{\X{loc}}
+.. |reg| mathdef:: \xref{exec/runtime}{syntax-reg}{\X{reg}}
 .. |fld| mathdef:: \xref{exec/runtime}{syntax-fld}{\X{fld}}
 .. |storeval| mathdef:: \xref{exec/runtime}{syntax-storeval}{\X{storeval}}
 .. |notears| mathdef:: \xref{exec/runtime}{syntax-ord}{\X{notears}}