Skip to content

Commit ca9550d

Browse files
committed
a little more
1 parent 99b2ff7 commit ca9550d

2 files changed

Lines changed: 5 additions & 1 deletion

File tree

document/core/exec/relaxed.rst

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@ Preliminary Definitions
3838
\rangeact \ldots & = & \ldots \\
3939
\\
4040
\tearfreeact \ldots & = & \ldots \\
41+
\sameact \ldots & = & \ldots \\
42+
\\
43+
\X{func}_{\loc}(\evt) \ldots & = & \X{func}(\act) \ldots \\
4144
\end{array}
4245
4346
.. todo:: need to refactor len+data in actions
@@ -161,7 +164,7 @@ Consistency
161164
162165
.. math::
163166
\frac{
164-
\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
167+
\tearfreeact_{\loc}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\loc}(\evt_R, \evt_W) \wedge \tearfreeact_{\loc}(\evt_W)\}| \leq 1
165168
}{
166169
\vdash_{\loc} \evt_R \notear \evt_W^\ast
167170
}

document/core/util/macros.def

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1130,6 +1130,7 @@
11301130
.. |rangeact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{range}}
11311131

11321132
.. |tearfreeact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{tearfree}}
1133+
.. |sameact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{same}}
11331134

11341135

11351136
.. Relaxed Memory Model Judgements

0 commit comments

Comments
 (0)