Skip to content

Commit 631684c

Browse files
ioannadioannad
authored
Typesetting adjustments (#213)
* 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 * 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. * Add some space and clarifying parentheses. * Adding line breaks to lines that go off the right edge of the document. Tested in html and pdf. * 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).
1 parent 8deee83 commit 631684c

2 files changed

Lines changed: 85 additions & 84 deletions

File tree

‎document/core/exec/instructions.rst‎

Lines changed: 27 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -3296,7 +3296,7 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
32963296
\begin{array}{lcl@{\qquad}l}
32973297
S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg)
32983298
&\stepto^{(\ARD~a.\LLEN~n)~(\ARMW~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast~b_{\F{w}}^\ast)}&
3299-
F; (t.\CONST~c)
3299+
S; F; (t.\CONST~c)
33003300
\end{array}
33013301
\\ \qquad
33023302
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3312,7 +3312,7 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
33123312
\begin{array}{lcl@{\qquad}l}
33133313
S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg)
33143314
&\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b_{\F{r}}^\ast)}&
3315-
F; (t.\CONST~c)
3315+
S; F; (t.\CONST~c)
33163316
\end{array}
33173317
\\ \qquad
33183318
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3327,7 +3327,7 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
33273327
\begin{array}{lcl@{\qquad}l}
33283328
S; F; (\I32.\CONST~i)~(t.\CONST~c_2)~(t.\CONST~c_3)~(t.\ATOMICRMW({N}\K{\_u})^?.\ATCMPXCHG~\memarg)
33293329
&\stepto^{(\ARD~a.\LLEN~n)}&
3330-
F; \TRAP
3330+
S; F; \TRAP
33313331
\end{array}
33323332
\\ \qquad
33333333
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3404,9 +3404,9 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
34043404
.. math::
34053405
\begin{array}{l}
34063406
\begin{array}{lcl@{\qquad}l}
3407-
F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
3407+
S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
34083408
&\stepto&
3409-
F; (\I32.\CONST~0)
3409+
S; F; (\I32.\CONST~0)
34103410
\end{array}
34113411
\\ \qquad
34123412
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3416,40 +3416,40 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
34163416
\end{array}
34173417
\\[1ex]
34183418
\begin{array}{lcl@{\qquad}l}
3419-
F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
3419+
S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
34203420
&\stepto&
3421-
F; \TRAP
3421+
S; F; \TRAP
34223422
\end{array}
34233423
\\ \qquad
34243424
\begin{array}[t]{@{}r@{~}l@{}}
34253425
(\iff & \X{mem}.\MITYPE = \limits~\UNSHARED \\
3426-
\wedge & \X{ea} + N/8 > |\X{mem}.\MIDATA| \vee \X{ea} \mod N/8 \neq 0) \\
3426+
\wedge & (\X{ea} + N/8 > |\X{mem}.\MIDATA| ~\vee~ \X{ea} \mod~N/8 \neq 0)) \\
34273427
\end{array}
34283428
\\
34293429
%
34303430
~\\
34313431
\begin{array}{lcl@{\qquad}l}
3432-
F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
3433-
&\stepto^{(\ARD~a.\LLEN~n)~(\ANOTIFY~a.\LDATA[\X{ea}]~j~k)}&
3434-
F; (\I32.\CONST~j)
3432+
S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg && \\
3433+
\qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ANOTIFY~a.\LDATA[\X{ea}]~j~k)}
3434+
\quad S; F; (\I32.\CONST~j) &&
34353435
\end{array}
34363436
\\ \qquad
34373437
\begin{array}[t]{@{}r@{~}l@{}}
3438-
(\iff & \X{mem}.\MITYPE = \limits~\SHARED \\ord
3438+
(\iff & \X{mem}.\MITYPE = \limits~\SHARED \\
34393439
\wedge & \X{ea} + N/8 \leq n \\
34403440
\wedge & j \leq k \\
34413441
\wedge & \X{ea} \mod N/8 = 0) \\[1ex]
34423442
\end{array}
34433443
\\[1ex]
34443444
\begin{array}{lcl@{\qquad}l}
3445-
F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
3445+
S; F; (\I32.\CONST~i)~(\I32.\CONST~k)~\MEMORYATOMICNOTIFY~\memarg
34463446
&\stepto^{(\ARD~a.\LLEN~n)}&
3447-
F; \TRAP
3447+
S; F; \TRAP
34483448
\end{array}
34493449
\\ \qquad
34503450
\begin{array}[t]{@{}r@{~}l@{}}
34513451
(\iff & \X{mem}.\MITYPE = \limits~\SHARED \\
3452-
\wedge & \X{ea} + N/8 > n \vee \X{ea} \mod N/8 \neq 0) \\
3452+
\wedge & (\X{ea} + N/8 > n ~\vee~ \X{ea} \mod N/8 \neq 0)) \\
34533453
\end{array}
34543454
\\
34553455
%
@@ -3523,9 +3523,8 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
35233523
.. math::
35243524
\begin{array}{l}
35253525
\begin{array}{lcl@{\qquad}l}
3526-
F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg
3527-
&\stepto&
3528-
F; \TRAP
3526+
S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg && \\
3527+
\qquad\qquad \stepto \quad S; F; \TRAP &&
35293528
\end{array}
35303529
\\ \qquad
35313530
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3535,9 +3534,9 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
35353534
%
35363535
~\\
35373536
\begin{array}{lcl@{\qquad}l}
3538-
F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg
3539-
&\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)}&
3540-
F; (\WAITX~a.\LDATA[\X{ea}]~k)
3537+
S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\
3538+
\qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)~(\AWAIT~a.\LDATA[\X{ea}]~t)}
3539+
\quad S; F; (\WAITX~a.\LDATA[\X{ea}]~k) && \\
35413540
\end{array}
35423541
\\ \qquad
35433542
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3549,9 +3548,9 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
35493548
\end{array}
35503549
\\[1ex]
35513550
\begin{array}{lcl@{\qquad}l}
3552-
F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg
3553-
&\stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)}&
3554-
F; (\I32.\CONST~1)
3551+
S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\
3552+
\qquad\qquad \stepto^{(\ARD~a.\LLEN~n)~(\ARD_{\SEQCST}~a.\LDATA[\X{ea}]~b^\ast)}
3553+
\quad S; F; (\I32.\CONST~1)
35553554
\end{array}
35563555
\\ \qquad
35573556
\begin{array}[t]{@{}r@{~}l@{}}
@@ -3562,14 +3561,14 @@ The rules are identical to :ref:`non-atomic stores <exec-store>`, except that :m
35623561
\end{array}
35633562
\\[1ex]
35643563
\begin{array}{lcl@{\qquad}l}
3565-
F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg
3566-
&\stepto^{(\ARD~a.\LLEN~n)}&
3567-
F; \TRAP
3564+
S; F; (\I32.\CONST~i)~(\iN.\CONST~c)~(\I64.\CONST~k)~\MEMORYATOMICWAIT{N}~\memarg &&\\
3565+
\qquad\qquad \stepto^{(\ARD~a.\LLEN~n)}
3566+
\quad S; F; \TRAP
35683567
\end{array}
35693568
\\ \qquad
35703569
\begin{array}[t]{@{}r@{~}l@{}}
35713570
(\iff & \X{mem}.\MITYPE = \limits~\SHARED \\
3572-
\wedge & (\X{ea} + N/8 > n \vee \X{ea} \mod N/8 \neq 0)) \\
3571+
\wedge & (\X{ea} + N/8 > n ~\vee~ \X{ea} \mod N/8 \neq 0)) \\
35733572
\end{array}
35743573
\\
35753574
%

‎document/core/exec/relaxed.rst‎

Lines changed: 58 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -22,40 +22,46 @@ Preliminary Definitions
2222
.. math::
2323
\begin{array}{rcl}
2424
\timeevt(\act^\ast~\AT~\time_p~\time) & = & \time \\
25-
\\
25+
&&\\
2626
\locact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
2727
\locact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
2828
\locact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \loc \\
29-
\\
29+
&&\\
3030
\ordact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
3131
\ordact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
3232
\ordact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \SEQCST \\
33-
\\
34-
\overlapact(\act_1, \act_2) & = & \rangeact(\act_1) \cup \rangeact(\act_2) \neq \epsilon \\
35-
\sameact(\act_1, \act_2) & = & \rangeact(\act_1) = \rangeact(\act_2) \\
36-
\\
37-
\readingact(\act) & = & \readact(\act) \neq \epsilon \\
38-
\writingact(\act) & = & \writeact(\act) \neq \epsilon \\
39-
\\
33+
&&\\
34+
\overlapact(\act_1, \act_2) & = & (\rangeact(\act_1) \cup \rangeact(\act_2) \neq \epsilon) \\
35+
\sameact(\act_1, \act_2) & = & (\rangeact(\act_1) = \rangeact(\act_2)) \\
36+
&&\\
37+
\readingact(\act) & = & (\readact(\act) \neq \epsilon) \\
38+
\writingact(\act) & = & (\writeact(\act) \neq \epsilon) \\
39+
&&\\
4040
\readact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
4141
\readact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\
42-
\readact(\act) & = & \epsilon \qquad \otherwise \\
42+
\readact(\act) & = & \epsilon \qquad (\otherwise) \\
4343
&&\\
4444
\writeact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
4545
\writeact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\
46-
\writeact(\act) & = & \epsilon \qquad \otherwise \\
46+
\writeact(\act) & = & \epsilon \qquad (\otherwise) \\
47+
&&\\
48+
\offsetact(\act) & = & \u32 \qquad (\iff~\locact(\act) = \reg[\u32]) \\
49+
&&\\
50+
\syncact(\act_1,\act_2) & = & (\sameact(\act_1,\act_2) \wedge \\
51+
&& \qquad \ordact(\act_1) = \ordact(\act_2) = \SEQCST) \\
52+
\rangeact(\act) & = & [\u32 \ldots \u32 + n - 1] \\
53+
&& (\iff~\locact(\act) = \reg[\u32] \wedge \\
54+
&& \quad n = \F{max}(|\readact(\act)|,|\writeact(\act)|)) \\
4755
&&\\
48-
\offsetact(\act) & = & \u32 \qquad \iff \locact(\act) = \reg[\u32] \ \\
49-
\\
50-
\syncact(\act_1,\act_2) & = & \sameact(\act_1,\act_2) \wedge \ordact(\act_1) = \ordact(\act_2) = \SEQCST \\
51-
\rangeact(\act) & = & [\u32 \ldots \u32 + n - 1] \qquad \iff \locact(\act) = \reg[\u32] \qquad n = \F{max}(|\readact(\act)|,|\writeact(\act)|) \\
52-
\\
53-
\tearfreeact(\ARD_{\ord}~\loc~\byte^\ast) & = & \bot \qquad \iff \ord = \UNORD \vee \ord = \INIT \\
54-
\tearfreeact(\AWR_{\ord}~\loc~\byte^\ast) & = & \bot \qquad \iff \ord = \UNORD \vee \ord = \INIT \\
55-
\tearfreeact(\act) & = & \top \qquad \otherwise \\
56-
\\
57-
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time) & = & \X{func}(\act) \qquad \iff \locact(\act) = \reg[\u32] \\
58-
\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] \\
56+
\tearfreeact(\ARD_{\ord}~\loc~\byte^\ast) & = & \bot \qquad (\iff~\ord = \UNORD \vee \ord = \INIT) \\
57+
\tearfreeact(\AWR_{\ord}~\loc~\byte^\ast) & = & \bot \qquad (\iff~\ord = \UNORD \vee \ord = \INIT) \\
58+
\tearfreeact(\act) & = & \top \qquad (\otherwise) \\
59+
&&\\
60+
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time) & = & \X{func}(\act) \\
61+
&& (\iff~\locact(\act) = \reg[\u32]) \\
62+
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time_p~\time, \quad &&\\
63+
\qquad \act_3^\ast~\act'~\act_4^\ast~\AT~\time'_p~\time') & = & \X{func}(\act,\act') \\
64+
&& (\iff~\locact(\act) = \locact(\act') = \reg[\u32]) \\
5965
\end{array}
6066
6167
.. todo:: add loc for wait/woken/timeout/notify
@@ -78,9 +84,9 @@ A trace is a coinductive set of :ref:`events <syntax-evt>`. A trace is considere
7884

7985
.. math::
8086
\begin{array}{c}
81-
\config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace) \\[0.2\normalbaselineskip]
82-
\hline \\[-0.8\normalbaselineskip]
83-
\hline \\[-0.8\normalbaselineskip]
87+
\config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace) \\[0.2ex]
88+
\hline \\[-0.8ex]
89+
\hline \\[-0.8ex]
8490
\vdash \config : \evt~\trace
8591
\end{array}
8692
@@ -96,54 +102,50 @@ Consistency
96102

97103
.. math::
98104
\frac{
99-
\forall \reg, \, \vdash_{\reg} \trace \consistentwith
105+
\forall \reg,~ \vdash_{\reg} \trace~\consistentwith
100106
}{
101-
\vdash \trace \consistent
107+
\vdash \trace~\consistent
102108
}
103109
104110
.. math::
105111
\frac{
106112
\begin{array}[b]{@{}c@{}}
107-
\vdash_{\reg} \trace \suspensionsconsistentwith \\
113+
\vdash_{\reg} \trace~\suspensionsconsistentwith \\
108114
\forall \evt_R \in \readingact_{\reg}(\trace), \exists \evt_W^\ast,
109-
\trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\
115+
\trace \vdash_{\reg} \evt_R~\readseachfrom~\evt_W^\ast \\
110116
\forall \evt_I, \evt \in \trace, \,
111117
\ordact_{\reg}(\evt_I) = \INIT \wedge
112118
\evt_I \neq \evt \wedge
113119
\overlapact(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt
114120
\end{array}
115121
}{
116-
\vdash_{\reg} \trace \consistentwith
122+
\vdash_{\reg} \trace~\consistentwith
117123
}
118124
119125
.. math::
120126
\frac{
121127
\begin{array}[b]{@{}c@{}}
122128
\left|\evt_W^\ast\right| = |\readact_{\reg}(\evt_R)| \\
123129
\forall i < |\evt_W^\ast|,
124-
\trace \vdash_{\reg}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
130+
\trace \vdash_{\reg}^i \evt_R~\readsfrom~\left(\evt_W^\ast[i]\right)
125131
\\
126-
\vdash_{\reg} \evt_R \notear \evt_W^\ast
132+
\vdash_{\reg} \evt_R~\notear~\evt_W^\ast
127133
\end{array}
128134
}{
129-
\trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast
135+
\trace \vdash_{\reg} \evt_R~\readseachfrom~\evt_W^\ast
130136
}
131137
132138
.. math::
133139
\frac{
134-
\begin{array}[b]{@{}l@{}}
135-
\evt_R \neq \evt_W \\
136-
\evt_W \in \writingact_{\reg}(\trace)
137-
\end{array}
138-
\qquad
139-
\begin{array}[b]{@{}r@{}}
140-
\trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W \\
141-
\trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
140+
\begin{array}[b]{@{}c}
141+
\evt_R \neq \evt_W \\
142+
\evt_W \in \writingact_{\reg}(\trace) \\
143+
\trace \vdash_{\reg}^{i,k} \evt_R~\valueconsistent~\evt_W \\
144+
\trace \vdash_{\reg}^k \evt_R~\hbconsistent~\evt_W \\
145+
\trace \vdash_{\reg} \evt_R~\sclastvisible~\evt^\ast_W
142146
\end{array}
143-
\qquad
144-
\trace \vdash_{\reg} \evt_R \sclastvisible \evt^\ast_W
145147
}{
146-
\trace \vdash_{\reg}^i \evt_R \readsfrom \evt_W
148+
\trace \vdash_{\reg}^i \evt_R~\readsfrom~\evt_W
147149
}
148150
149151
.. math::
@@ -153,22 +155,18 @@ Consistency
153155
k = \offsetact_{\reg}(\evt_R) + i &=& \offsetact_{\reg}(\evt_W) + j
154156
\end{array}
155157
}{
156-
\trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W
158+
\trace \vdash_{\reg}^{i,k} \evt_R~\valueconsistent~\evt_W
157159
}
158160
159161
.. math::
160162
\frac{
161163
\begin{array}[b]{@{}c}
162164
\neg (\evt_R \prechb \evt_W) \\
163-
\syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R
164-
\end{array}
165-
\qquad
166-
\begin{array}[b]{@{}l@{}}
167-
\forall \evt'_W \in \writingact_{\reg}(\trace),\\
168-
\quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W)
165+
\syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \evt_W \prechb \evt_R \\
166+
\forall \evt'_W \in \writingact_{\reg}(\trace), \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W)
169167
\end{array}
170168
}{
171-
\trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
169+
\trace \vdash_{\reg}^k \evt_R~\hbconsistent~\evt_W
172170
}
173171
174172
.. math::
@@ -180,23 +178,27 @@ Consistency
180178
\quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\syncact_{\reg}(\evt_W, \evt'_W)
181179
\end{array}
182180
}{
183-
\trace \vdash_{\reg} \evt_R \sclastvisible \evt_W
181+
\trace \vdash_{\reg} \evt_R~\sclastvisible~\evt_W
184182
}
185183
186184
.. math::
187185
\frac{
188-
\tearfreeact_{\reg}(\evt_R) \Rightarrow |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\reg}(\evt_R, \evt_W) \wedge \tearfreeact_{\reg}(\evt_W)\}| \leq 1
186+
\begin{array}[b]{l@{}}
187+
\tearfreeact_{\reg}(\evt_R) \Rightarrow \\
188+
\quad |\{\evt_W \in \evt_W^\ast ~|~ \sameact_{\reg}(\evt_R, \evt_W) \wedge \tearfreeact_{\reg}(\evt_W)\}| \leq 1
189+
\end{array}
189190
}{
190-
\vdash_{\reg} \evt_R \notear \evt_W^\ast
191+
\vdash_{\reg} \evt_R~\notear~\evt_W^\ast
191192
}
192193
193194
.. math::
194195
\frac{
195196
TODO
196197
}{
197-
\vdash_{\reg} \trace \suspensionsconsistentwith
198+
\vdash_{\reg} \trace~\suspensionsconsistentwith
198199
}
199200
201+
200202
.. todo:: pull out the trace events which denote wait/wake actions as a timestamped list, check queue behaviour
201203

202204

0 commit comments

Comments
 (0)