begin aux function specs

Author: conrad-watt

document/core/exec/relaxed.rst

@@ -6,8 +6,41 @@
 Relaxed Memory Model
 --------------------
 
-.. todo:: intro, cite [#cite-oopsla2019]_
-.. todo:: link this section with operational semantics
+The execution of a WebAssembly program gives rise to a :ref:`trace <relaxed-trace>` of events. WebAssembly's relaxed memory model constrains the observable behaviours of the program's execution by defining a :ref:`consistency <relaxed-consistent>` condition on the trace of events.
+
+.. note::
+   A relaxed memory model is necessary to describe the behaviour of programs exhibiting *shared memory concurrency*.
+   WebAssembly's relaxed memory model is heavily based on those of C/C++11 and JavaScript.
+   The relaxed memory model decribed here is derived from the following article: [#cite-oopsla2019]_.
+
+
+.. _relaxed-aux:
+
+Preliminary Definitions
+~~~~~~~~~~~~~~~~~~~~~~~
+
+.. math::
+   \begin{array}{lcl}
+   \timeevt \ldots     & = & \ldots \\
+   \\
+   \readingact \ldots  & = & \ldots \\
+   \ordact \ldots      & = & \ldots \\
+   \overlapact \ldots  & = & \ldots \\
+   \\
+   \readact \ldots     & = & \ldots \\
+   \\
+   \writingact \ldots  & = & \ldots \\
+   \\
+   \writeact \ldots    & = & \ldots \\
+   \offsetact \ldots   & = & \ldots \\
+   \\
+   \syncact \ldots     & = & \ldots \\
+   \rangeact \ldots    & = & \ldots \\
+   \\
+   \tearfreeact \ldots & = & \ldots \\
+   \end{array}
+
+.. todo:: need to refactor len+data in actions
 
 
 .. _relaxed-trace:
@@ -21,7 +54,7 @@ A trace is a coinductive set of :ref:`events <syntax-evt>`. A trace is considere
 
 .. math::
    \frac{
-     \config \stepto^{\evt} \config' \qquad \vdash \config' : \X{tr} \qquad \F{time}(\evt) \notin \F{time}(\X{tr})
+     \config \stepto^{\evt} \config' \qquad \vdash \config' : \X{tr} \qquad \timeevt(\evt) \notin \timeevt^\ast(\X{tr})
    }{
      \vdash \config : \evt~\X{tr}
    }
@@ -40,97 +73,97 @@ Consistency
 
 .. math::
    \frac{
-     \forall r, \, \vdash_r \X{tr} \consistentwith
+     \forall \loc, \, \vdash_{\loc} \X{tr} \consistentwith
    }{
      \vdash \X{tr} \consistent
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
-       \forall \evt_R \in \F{reading}_r(\X{tr}), \exists \evt_W^\ast,
-         \X{tr} \vdash_r \evt_R \readseachfrom \evt_W^\ast \\
+       \forall \evt_R \in \readingact_{\loc}(\X{tr}), \exists \evt_W^\ast,
+         \X{tr} \vdash_{\loc} \evt_R \readseachfrom \evt_W^\ast \\
        \forall \evt_I, \evt \in \X{tr}, \,
-         \F{ord}_r(\evt_I) = \INIT \wedge
+         \ordact_{\loc}(\evt_I) = \INIT \wedge
          \evt_I \neq \evt \wedge
-         \F{overlap}_r(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt
+         \overlapact(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt
      \end{array}
    }{
-     \vdash_r \X{tr} \consistentwith
+     \vdash_{\loc} \X{tr} \consistentwith
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}c@{}}
-       \left|\evt_W^\ast\right| = |\F{read}_r(\evt_R)| \\
+       \left|\evt_W^\ast\right| = |\readact_{\loc}(\evt_R)| \\
        \forall i < |\evt_W^\ast|,
-         \X{tr} \vdash_r^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
+         \X{tr} \vdash_{\loc}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
        \\
-       \vdash_r \evt_R \notear \evt_W^\ast
+       \vdash_{\loc} \evt_R \notear \evt_W^\ast
      \end{array}
    }{
-     \X{tr} \vdash_r \evt_R \readseachfrom \evt_W^\ast
+     \X{tr} \vdash_{\loc} \evt_R \readseachfrom \evt_W^\ast
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{}}
        \evt_R \neq \evt_W \\
-       \evt_W \in \F{writing}_r(\X{tr})
+       \evt_W \in \writingact_{\loc}(\X{tr})
      \end{array}
      \qquad
      \begin{array}[b]{@{}r@{}}
-       \X{tr} \vdash_r^{i,k} \evt_R \valueconsistent \evt_W \\
-       \X{tr} \vdash_r^k \evt_R \hbconsistent \evt_W
+       \X{tr} \vdash_{\loc}^{i,k} \evt_R \valueconsistent \evt_W \\
+       \X{tr} \vdash_{\loc}^k \evt_R \hbconsistent \evt_W
      \end{array}
      \qquad
-     \X{tr} \vdash_r \evt_R \sclastvisible \evt^\ast_W
+     \X{tr} \vdash_{\loc} \evt_R \sclastvisible \evt^\ast_W
    }{
-     \X{tr} \vdash_r^i \evt_R \readsfrom \evt_W
+     \X{tr} \vdash_{\loc}^i \evt_R \readsfrom \evt_W
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}r@{~}c@{~}l@{}}
-       \F{read}_r(\evt_R)[i] &=& \F{write}_r(\evt_W)[j] \\
-       k = \F{offset}_r(\evt_R) + i &=& \F{offset}_r(\evt_W) + j
+       \readact_{\loc}(\evt_R)[i] &=& \writeact_{\loc}(\evt_W)[j] \\
+       k = \offsetact_{\loc}(\evt_R) + i &=& \offsetact_{\loc}(\evt_W) + j
      \end{array}
   }{
-     \X{tr} \vdash_r^{i,k} \evt_R \valueconsistent \evt_W
+     \X{tr} \vdash_{\loc}^{i,k} \evt_R \valueconsistent \evt_W
   }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}c}
        \neg (\evt_R \prechb \evt_W) \\
-       \F{sync}_r(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R
+       \syncact_{\loc}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R
      \end{array}
     \qquad
     \begin{array}[b]{@{}l@{}}
-      \forall \evt'_W \in \F{writing}_r(\X{tr}),\\
-      \quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \F{range}_r(\evt'_W)
+      \forall \evt'_W \in \writingact_{\loc}(\X{tr}),\\
+      \quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\loc}(\evt'_W)
     \end{array}
    }{
-    \X{tr} \vdash_r^k \evt_R \hbconsistent \evt_W
+    \X{tr} \vdash_{\loc}^k \evt_R \hbconsistent \evt_W
    }
 
 .. math::
    \frac{
      \begin{array}[b]{@{}l@{\qquad}l@{}}
-       \forall \evt'_W \in \F{writing}_r(\X{tr}), \evt_W \prechb \evt_R \Rightarrow \\
-       \quad \evt_W \prectot \evt'_W \prectot \evt_R \wedge \F{sync}_r(\evt_W, \evt_R) \Rightarrow \neg \F{sync}_r(\evt'_W, \evt_R) \\
-       \quad \evt_W \prechb \evt'_W \prectot \evt_R  \Rightarrow \neg\F{sync}_r(\evt'_W, \evt_R) \\
-       \quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\F{sync}_r(\evt_W, \evt'_W)
+       \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)
      \end{array}
    }{
-     \X{tr} \vdash_r \evt_R \sclastvisible \evt_W
+     \X{tr} \vdash_{\loc} \evt_R \sclastvisible \evt_W
    }
 
 .. math::
    \frac{
-     \F{tearfree}_r(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \F{same}_r(\evt_R, \evt_W) \wedge \F{tearfree}_r(\evt_W)\}| \leq 1
+     \tearfreeact_{\loc}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \F{same}_r(\evt_R, \evt_W) \wedge \tearfreeact_{\loc}(\evt_W)\}| \leq 1
    }{
-     \vdash_r \evt_R \notear \evt_W^\ast
+     \vdash_{\loc} \evt_R \notear \evt_W^\ast
    }
 
 

document/core/exec/runtime.rst

@@ -193,6 +193,7 @@ even where this identity is not observable from within WebAssembly code itself
 .. index:: ! time stamp, ! happens-before, thread, event
 .. _syntax-time:
 .. _relaxed-prechb:
+.. _relaxed-prectot:
 
 Time Stamps
 ~~~~~~~~~~~
@@ -208,8 +209,12 @@ the semantics uses a notion of abstract *time stamps*.
 
 Each time stamp denotes a discrete point in time, and is drawn from an infinite set.
 The shape of time stamps is not specified or observable.
-However, time stamps form a partially ordered set:
-a time stamp :math:`\time_1` *happens before* :math:`\time_2`, written :math:`\time_1 \prechb \time_2`, if it is known to have occurred earlier in time.
+
+Time stamps are associated with a total order -- if a time stamp :math:`\time_1` is *totally ordered before* time stamp :math:`\time_2`, this is written as :math:`\time_1 \prectot \time_2`.
+
+Time stamps are also associated with a *happens before* partial order -- if a time stamp :math:`\time_1` *happens before* :math:`\time_2`, this is written as :math:`\time_1 \prechb \time_2`.
+
+During the execution of WebAssembly code, time stamped :ref:`events <syntax-evt>` may be emitted which are related by one or both of these orderings, thus constraining the code's observable behaviours according to WebAssembly's :ref:`relaxed memory model <relaxed>`.
 
 .. note:
 
@@ -218,9 +223,6 @@ a time stamp :math:`\time_1` *happens before* :math:`\time_2`, written :math:`\t
 
    The ordering is partial because some events have an unspecified relative order -- in particular, when they occur in separate threads without intervening synchronisation.
 
-.. _relaxed-prectot:
-.. todo:: define prectot here as well?
-
 
 .. _notation-attime:
 
@@ -729,8 +731,8 @@ Its form and meaning is outside the scope of this specification.
    An :ref:`embedder <embedder>` may define a custom set of host actions and respective ordering constraints to model other forms of interactions that are not expressible within WebAssembly, but whose ordering relative to WebAssembly events is relevant for the combined semantics.
 
 
-Convention
-..........
+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`.
 
@@ -745,6 +747,15 @@ The following auxiliary definition is used to classify whether an access will *t
 
 
 .. todo:: better description of tearing
+
+Relations between time stamps are lifted to relations between events.
+
+.. math::
+   \begin{array}{lclclcl}
+   \act_1^\ast~\AT~\time_1 & \prectot & \act_2^\ast~\AT~\time_2  &=& \time_1 & \prectot & \time_2 \\
+   \act_1^\ast~\AT~\time_1 & \prechb & \act_2^\ast~\AT~\time_2  &=& \time_1 & \prechb & \time_2 \\
+   \end{array}
+
 .. todo:: define notational shorthands over actions and events (or better put that in relaxed.rst?)
 
 

document/core/util/macros.def

@@ -1113,6 +1113,24 @@
 .. Events, meta functions
 .. |tearing| mathdef:: \xref{exec/runtime}{syntax-ord}{\F{tearing}}
 
+.. |timeevt| mathdef:: \xref{exec/runtime}{relaxed-aux}{\F{time}}
+
+.. |readingact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{reading}}
+.. |ordact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{ord}}
+.. |overlapact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{overlap}}
+
+.. |readact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{read}}
+
+.. |writingact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{writing}}
+
+.. |writeact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{write}}
+.. |offsetact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{offset}}
+
+.. |syncact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{sync}}
+.. |rangeact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{range}}
+
+.. |tearfreeact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{tearfree}}
+
 
 .. Relaxed Memory Model Judgements
 
@@ -1125,9 +1143,8 @@
 .. |hbconsistent| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{hb-consistent}}}
 .. |valueconsistent| mathdef:: \xref{exec/relaxed}{relaxed-consistent}{\mathrel{\mbox{value-consistent}}}
 
-.. |prechb| mathdef:: \xref{exec/relaxed}{relaxed-prechb}{\mathrel{\prec_{\K{hb}}}}
-.. |prectot| mathdef:: \xref{exec/relaxed}{relaxed-prectot}{\mathrel{\prec_{\K{tot}}}}
-
+.. |prechb| mathdef:: \xref{exec/runtime}{relaxed-prechb}{\mathrel{\prec_{\K{hb}}}}
+.. |prectot| mathdef:: \xref{exec/runtime}{relaxed-prectot}{\mathrel{\prec_{\K{tot}}}}
 
 
 .. Stack, terminals