From 883419eccb90cac2cfee7b0ce215fa0ad55e2e21 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Wed, 13 Sep 2023 12:40:30 +0200 Subject: [PATCH 1/5] typesetting fixes - core/exec/instructions.rst: + (notify) Error in html: 'You can't use 'macro parameter character #' in math mode + (wait) too long right side of formal rules - core/exec/relaxed.rst (preliminary defs, nit picks): + add brackets due to ambiguous '=' signs in predicate definitions of overlapact, sameact, syncact + add linebreaks in some too long lines in rangeact, tearfreeact, \X{func}, syncact, + add brackets around 'otherwise' and '\iff ...', to match rest of spec + add several '~' to add missing space, after all '\iff' + add potentially forgotten '&&' before plain '\\'s - core/exec/relaxed.rst (consistency, nit picks): + add several '~' to add missing space, after predicates consistentwith, suspensionsconsistentwith, readsfrom, valueconsistentwith, hbconsistentwith, sclastvisible, notear, + removed potentially misplaced '\,' + removed and added some arrays to make the lines less long --- document/core/exec/instructions.rst | 10 +-- document/core/exec/relaxed.rst | 108 ++++++++++++++-------------- 2 files changed, 60 insertions(+), 58 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 3443e8e97..05160ce7a 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3435,7 +3435,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} - (\iff & \X{mem}.\MITYPE = \limits~\SHARED \\ord + (\iff & \X{mem}.\MITYPE = \limits~\SHARED \\ \wedge & \X{ea} + N/8 \leq n \\ \wedge & j \leq k \\ \wedge & \X{ea} \mod N/8 = 0) \\[1ex] @@ -3534,10 +3534,10 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \\ % ~\\ - \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg - &\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)}& - F; (\WAITX~a.\LDATA[\X{ea}]~k) + \begin{array}{rcl@{\qquad}l} + F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + \qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)}& + F; (\WAITX~a.\LDATA[\X{ea}]~k) & \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} diff --git a/document/core/exec/relaxed.rst b/document/core/exec/relaxed.rst index 16d98c243..ddf5c747e 100644 --- a/document/core/exec/relaxed.rst +++ b/document/core/exec/relaxed.rst @@ -22,40 +22,46 @@ Preliminary Definitions .. math:: \begin{array}{rcl} \timeevt(\act^\ast~\AT~\time_p~\time) & = & \time \\ - \\ + &&\\ \locact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\ \locact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\ \locact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \loc \\ - \\ + &&\\ \ordact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\ \ordact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\ \ordact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \SEQCST \\ - \\ - \overlapact(\act_1, \act_2) & = & \rangeact(\act_1) \cup \rangeact(\act_2) \neq \epsilon \\ - \sameact(\act_1, \act_2) & = & \rangeact(\act_1) = \rangeact(\act_2) \\ - \\ - \readingact(\act) & = & \readact(\act) \neq \epsilon \\ - \writingact(\act) & = & \writeact(\act) \neq \epsilon \\ - \\ + &&\\ + \overlapact(\act_1, \act_2) & = & (\rangeact(\act_1) \cup \rangeact(\act_2) \neq \epsilon) \\ + \sameact(\act_1, \act_2) & = & (\rangeact(\act_1) = \rangeact(\act_2)) \\ + &&\\ + \readingact(\act) & = & (\readact(\act) \neq \epsilon) \\ + \writingact(\act) & = & (\writeact(\act) \neq \epsilon) \\ + &&\\ \readact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\ \readact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\ - \readact(\act) & = & \epsilon \qquad \otherwise \\ + \readact(\act) & = & \epsilon \qquad (\otherwise) \\ &&\\ \writeact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\ \writeact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\ - \writeact(\act) & = & \epsilon \qquad \otherwise \\ + \writeact(\act) & = & \epsilon \qquad (\otherwise) \\ + &&\\ + \offsetact(\act) & = & \u32 \qquad (\iff~\locact(\act) = \reg[\u32]) \\ + &&\\ + \syncact(\act_1,\act_2) & = & (\sameact(\act_1,\act_2) \wedge \\ + && \qquad \ordact(\act_1) = \ordact(\act_2) = \SEQCST) \\ + \rangeact(\act) & = & [\u32 \ldots \u32 + n - 1] \\ + && (\iff~\locact(\act) = \reg[\u32] \wedge \\ + && \quad n = \F{max}(|\readact(\act)|,|\writeact(\act)|)) \\ &&\\ - \offsetact(\act) & = & \u32 \qquad \iff \locact(\act) = \reg[\u32] \ \\ - \\ - \syncact(\act_1,\act_2) & = & \sameact(\act_1,\act_2) \wedge \ordact(\act_1) = \ordact(\act_2) = \SEQCST \\ - \rangeact(\act) & = & [\u32 \ldots \u32 + n - 1] \qquad \iff \locact(\act) = \reg[\u32] \qquad n = \F{max}(|\readact(\act)|,|\writeact(\act)|) \\ - \\ - \tearfreeact(\ARD_{\ord}~\loc~\byte^\ast) & = & \bot \qquad \iff \ord = \UNORD \vee \ord = \INIT \\ - \tearfreeact(\AWR_{\ord}~\loc~\byte^\ast) & = & \bot \qquad \iff \ord = \UNORD \vee \ord = \INIT \\ - \tearfreeact(\act) & = & \top \qquad \otherwise \\ - \\ - \X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time) & = & \X{func}(\act) \qquad \iff \locact(\act) = \reg[\u32] \\ - \X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time, \act_3^\ast~\act'~\act_4^\ast~\AT~\time'_p~\time') & = & \X{func}(\act.\act') \qquad \iff \locact(\act) = \locact(\act') = \reg[\u32] \\ + \tearfreeact(\ARD_{\ord}~\loc~\byte^\ast) & = & \bot \qquad (\iff~\ord = \UNORD \vee \ord = \INIT) \\ + \tearfreeact(\AWR_{\ord}~\loc~\byte^\ast) & = & \bot \qquad (\iff~\ord = \UNORD \vee \ord = \INIT) \\ + \tearfreeact(\act) & = & \top \qquad (\otherwise) \\ + &&\\ + \X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time) & = & \X{func}(\act) \\ + && (\iff~\locact(\act) = \reg[\u32]) \\ + \X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time, \quad &&\\ + \qquad \act_3^\ast~\act'~\act_4^\ast~\AT~\time'_p~\time') & = & \X{func}(\act,\act') \\ + && (\iff~\locact(\act) = \locact(\act') = \reg[\u32]) \\ \end{array} .. todo:: add loc for wait/woken/timeout/notify @@ -96,24 +102,24 @@ Consistency .. math:: \frac{ - \forall \reg, \, \vdash_{\reg} \trace \consistentwith + \forall \reg,~ \vdash_{\reg} \trace~\consistentwith }{ - \vdash \trace \consistent + \vdash \trace~\consistent } .. math:: \frac{ \begin{array}[b]{@{}c@{}} - \vdash_{\reg} \trace \suspensionsconsistentwith \\ + \vdash_{\reg} \trace~\suspensionsconsistentwith \\ \forall \evt_R \in \readingact_{\reg}(\trace), \exists \evt_W^\ast, - \trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\ + \trace \vdash_{\reg} \evt_R~\readseachfrom~\evt_W^\ast \\ \forall \evt_I, \evt \in \trace, \, \ordact_{\reg}(\evt_I) = \INIT \wedge \evt_I \neq \evt \wedge \overlapact(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt \end{array} }{ - \vdash_{\reg} \trace \consistentwith + \vdash_{\reg} \trace~\consistentwith } .. math:: @@ -121,29 +127,25 @@ Consistency \begin{array}[b]{@{}c@{}} \left|\evt_W^\ast\right| = |\readact_{\reg}(\evt_R)| \\ \forall i < |\evt_W^\ast|, - \trace \vdash_{\reg}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right) + \trace \vdash_{\reg}^i \evt_R~\readsfrom~\left(\evt_W^\ast[i]\right) \\ - \vdash_{\reg} \evt_R \notear \evt_W^\ast + \vdash_{\reg} \evt_R~\notear~\evt_W^\ast \end{array} }{ - \trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast + \trace \vdash_{\reg} \evt_R~\readseachfrom~\evt_W^\ast } .. math:: \frac{ - \begin{array}[b]{@{}l@{}} - \evt_R \neq \evt_W \\ - \evt_W \in \writingact_{\reg}(\trace) - \end{array} - \qquad - \begin{array}[b]{@{}r@{}} - \trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W \\ - \trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W + \begin{array}[b]{@{}c} + \evt_R \neq \evt_W \\ + \evt_W \in \writingact_{\reg}(\trace) \\ + \trace \vdash_{\reg}^{i,k} \evt_R~\valueconsistent~\evt_W \\ + \trace \vdash_{\reg}^k \evt_R~\hbconsistent~\evt_W \\ + \trace \vdash_{\reg} \evt_R~\sclastvisible~\evt^\ast_W \end{array} - \qquad - \trace \vdash_{\reg} \evt_R \sclastvisible \evt^\ast_W }{ - \trace \vdash_{\reg}^i \evt_R \readsfrom \evt_W + \trace \vdash_{\reg}^i \evt_R~\readsfrom~\evt_W } .. math:: @@ -153,22 +155,18 @@ Consistency k = \offsetact_{\reg}(\evt_R) + i &=& \offsetact_{\reg}(\evt_W) + j \end{array} }{ - \trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W + \trace \vdash_{\reg}^{i,k} \evt_R~\valueconsistent~\evt_W } .. math:: \frac{ \begin{array}[b]{@{}c} \neg (\evt_R \prechb \evt_W) \\ - \syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R - \end{array} - \qquad - \begin{array}[b]{@{}l@{}} - \forall \evt'_W \in \writingact_{\reg}(\trace),\\ - \quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W) + \syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R \\ + \forall \evt'_W \in \writingact_{\reg}(\trace), \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W) \end{array} }{ - \trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W + \trace \vdash_{\reg}^k \evt_R~\hbconsistent~\evt_W } .. math:: @@ -180,23 +178,27 @@ Consistency \quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\syncact_{\reg}(\evt_W, \evt'_W) \end{array} }{ - \trace \vdash_{\reg} \evt_R \sclastvisible \evt_W + \trace \vdash_{\reg} \evt_R~\sclastvisible~\evt_W } .. math:: \frac{ - \tearfreeact_{\reg}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\reg}(\evt_R, \evt_W) \wedge \tearfreeact_{\reg}(\evt_W)\}| \leq 1 + \begin{array}[b]{l@{}} + \tearfreeact_{\reg}(\evt_R) \Rightarrow \\ + \quad |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\reg}(\evt_R, \evt_W) \wedge \tearfreeact_{\reg}(\evt_W)\}| \leq 1 + \end{array} }{ - \vdash_{\reg} \evt_R \notear \evt_W^\ast + \vdash_{\reg} \evt_R~\notear~\evt_W^\ast } .. math:: \frac{ TODO }{ - \vdash_{\reg} \trace \suspensionsconsistentwith + \vdash_{\reg} \trace~\suspensionsconsistentwith } + .. todo:: pull out the trace events which denote wait/wake actions as a timestamped list, check queue behaviour From c40e969222eed36f544656989ad41957408d7242 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 15 Sep 2023 11:32:47 +0200 Subject: [PATCH 2/5] changed '\normalbaselineskip' to 'ex' In relaxed.rst (traces): was creating the error 'Bracket argument to \\ must be a dimension' It looks less good in the pdf than in the html though. --- document/core/exec/relaxed.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/relaxed.rst b/document/core/exec/relaxed.rst index ddf5c747e..0493f74a4 100644 --- a/document/core/exec/relaxed.rst +++ b/document/core/exec/relaxed.rst @@ -84,9 +84,9 @@ A trace is a coinductive set of :ref:`events `. A trace is considere .. math:: \begin{array}{c} - \config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace) \\[0.2\normalbaselineskip] - \hline \\[-0.8\normalbaselineskip] - \hline \\[-0.8\normalbaselineskip] + \config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace) \\[0.2ex] + \hline \\[-0.8ex] + \hline \\[-0.8ex] \vdash \config : \evt~\trace \end{array} From 71d872205668cb3e3096fc61fc427590fa114e4c Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 15 Sep 2023 14:37:40 +0200 Subject: [PATCH 3/5] Add some space and clarifying parentheses. --- document/core/exec/instructions.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 05160ce7a..310c68866 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3423,7 +3423,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{mem}.\MITYPE = \limits~\UNSHARED \\ - \wedge & \X{ea} + N/8 > |\X{mem}.\MIDATA| \vee \X{ea} \mod N/8 \neq 0) \\ + \wedge & (\X{ea} + N/8 > |\X{mem}.\MIDATA| ~\vee~ \X{ea} \mod~N/8 \neq 0)) \\ \end{array} \\ % @@ -3449,7 +3449,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{mem}.\MITYPE = \limits~\SHARED \\ - \wedge & \X{ea} + N/8 > n \vee \X{ea} \mod N/8 \neq 0) \\ + \wedge & (\X{ea} + N/8 > n ~\vee~ \X{ea} \mod N/8 \neq 0)) \\ \end{array} \\ % @@ -3569,7 +3569,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\iff & \X{mem}.\MITYPE = \limits~\SHARED \\ - \wedge & (\X{ea} + N/8 > n \vee \X{ea} \mod N/8 \neq 0)) \\ + \wedge & (\X{ea} + N/8 > n ~\vee~ \X{ea} \mod N/8 \neq 0)) \\ \end{array} \\ % From c45b79238531092c9f12637e2866999694260e08 Mon Sep 17 00:00:00 2001 From: "Ioanna M. Dimitriou H" Date: Fri, 15 Sep 2023 14:38:29 +0200 Subject: [PATCH 4/5] Adding line breaks to lines that go off the right edge of the document. Tested in html and pdf. --- document/core/exec/instructions.rst | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 310c68866..88da410aa 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3429,9 +3429,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m % ~\\ \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg - &\stepto^{(\ARD~a.\LLEN~n)~(\ANOTIFY~a.\LDATA[\X{ea}]~j~k)}& - F; (\I32.\CONST~j) + F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg && \\ + \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ANOTIFY~a.\LDATA[\X{ea}]~j~k)} + \quad F; (\I32.\CONST~j) && \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3523,9 +3523,8 @@ The rules are identical to :ref:`non-atomic stores `, except that :m .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg - &\stepto& - F; \TRAP + F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg && \\ + \qquad\qquad \stepto \quad F; \TRAP && \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3534,10 +3533,10 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \\ % ~\\ - \begin{array}{rcl@{\qquad}l} + \begin{array}{lcl@{\qquad}l} F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ - \qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)}& - F; (\WAITX~a.\LDATA[\X{ea}]~k) & + \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)} + \quad F; (\WAITX~a.\LDATA[\X{ea}]~k) && \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3549,9 +3548,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg - &\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)}& - F; (\I32.\CONST~1) + F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)} + \quad F; (\I32.\CONST~1) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3562,9 +3561,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg - &\stepto^{(\ARD~a.\LLEN~n)}& - F; \TRAP + F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)} + \quad F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} From 11377ad529b14aa0a65606122609dc3ac40f861a Mon Sep 17 00:00:00 2001 From: ioa Date: Sun, 17 Sep 2023 16:04:19 +0300 Subject: [PATCH 5/5] Add missing store to rules for notify, waitN, and rmw.cmpxchg The store is involved in these reductions as well, as it appears in the reduction steps of all other memory instructions which refer to a meminst (all memory instruction reductions except for wait' and fence). --- document/core/exec/instructions.rst | 38 ++++++++++++++--------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 88da410aa..9e7fdc3d0 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -3296,7 +3296,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg) &\stepto^{(\ARD~a.\LLEN~n)~(\ARMW~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)}& - F; (t.\CONST~c) + S; F; (t.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3312,7 +3312,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg) &\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast)}& - F; (t.\CONST~c) + S; F; (t.\CONST~c) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3327,7 +3327,7 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \begin{array}{lcl@{\qquad}l} S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg) &\stepto^{(\ARD~a.\LLEN~n)}& - F; \TRAP + S; F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3404,9 +3404,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg + S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg &\stepto& - F; (\I32.\CONST~0) + S; F; (\I32.\CONST~0) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3416,9 +3416,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg + S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg &\stepto& - F; \TRAP + S; F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3429,9 +3429,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m % ~\\ \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg && \\ + S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg && \\ \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ANOTIFY~a.\LDATA[\X{ea}]~j~k)} - \quad F; (\I32.\CONST~j) && + \quad S; F; (\I32.\CONST~j) && \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3442,9 +3442,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg + S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg &\stepto^{(\ARD~a.\LLEN~n)}& - F; \TRAP + S; F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3523,8 +3523,8 @@ The rules are identical to :ref:`non-atomic stores `, except that :m .. math:: \begin{array}{l} \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg && \\ - \qquad\qquad \stepto \quad F; \TRAP && + S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg && \\ + \qquad\qquad \stepto \quad S; F; \TRAP && \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3534,9 +3534,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m % ~\\ \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)} - \quad F; (\WAITX~a.\LDATA[\X{ea}]~k) && \\ + \quad S; F; (\WAITX~a.\LDATA[\X{ea}]~k) && \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3548,9 +3548,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)} - \quad F; (\I32.\CONST~1) + \quad S; F; (\I32.\CONST~1) \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} @@ -3561,9 +3561,9 @@ The rules are identical to :ref:`non-atomic stores `, except that :m \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} - F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ + S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\ \qquad\qquad \stepto^{(\ARD~a.\LLEN~n)} - \quad F; \TRAP + \quad S; F; \TRAP \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}}