Skip to content

Commit db59f85

Browse files
conrad-wattconrad-watt
committed
unify aux functions
1 parent fd26764 commit db59f85

2 files changed

Lines changed: 49 additions & 86 deletions

File tree

‎document/core/exec/relaxed.rst‎

Lines changed: 44 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,50 @@ The execution of a WebAssembly program gives rise to a :ref:`trace <relaxed-trac
1919
Preliminary Definitions
2020
~~~~~~~~~~~~~~~~~~~~~~~
2121

22-
Bla bla
22+
.. math::
23+
\begin{array}{rcl}
24+
\timeevt(\act^\ast~\AT~\time) & = & \time \\
25+
\\
26+
\locact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
27+
\locact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
28+
\locact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \loc \\
29+
\\
30+
\ordact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
31+
\ordact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
32+
\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+
\\
40+
\readact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
41+
\readact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\
42+
\readact(\act) & = & \epsilon \qquad \otherwise \\
43+
&&\\
44+
\writeact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
45+
\writeact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\
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 \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) & = & \X{func}(\act) \qquad \iff \locact(\act) = \reg[\u32] \\
58+
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time, \act_3^\ast~\act'~\act_4^\ast~\AT~\time') & = & \X{func}(\act.\act') \qquad \iff \locact(\act) = \locact(\act') = \reg[\u32] \\
59+
\end{array}
60+
61+
.. todo:: Double check notears
62+
63+
.. todo:: Tidy up range
64+
65+
.. todo:: add prose intuition?
2366

2467

2568
.. _relaxed-trace:
@@ -46,78 +89,6 @@ When a WebAssembly program is executed, all behaviours observed during that exec
4689
Consistency
4790
~~~~~~~~~~~
4891

49-
.. todo:: define auxiliary functions (either here or in Runtime Structure)
50-
51-
.. math::
52-
\begin{array}{lcl}
53-
\ordaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
54-
\ordaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
55-
\ordaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \SEQCST \\
56-
&&\\
57-
\locaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
58-
\locaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
59-
\locaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \loc \\
60-
&&\\
61-
\sizeaux(\ARD_{\ord}~\loc~\byte^n~\NOTEARS^?) & = & n \\
62-
\sizeaux(\AWR_{\ord}~\loc~\byte^n~\NOTEARS^?) & = & n \\
63-
\sizeaux(\ARMW~\loc~{\byte_1}^n~{\byte_2}^n) & = & n \\
64-
&&\\
65-
\readaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
66-
\readaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\
67-
\readaux(\act) & = & \epsilon \qquad \otherwise \\
68-
&&\\
69-
\writeaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \epsilon \\
70-
\writeaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\
71-
\writeaux(\act) & = & \epsilon \qquad \otherwise \\
72-
&&\\
73-
\addraux(\act) & = & \addraux(\regionaux(\act) \\
74-
\addraux(\loc) & = & \addraux(\regionaux(\reg) \\
75-
\addraux(\addr.\fld) & = & \addr \\
76-
&&\\
77-
\regionaux(\act) & = & \regionaux(\locaux(\act) \\
78-
\regionaux(\reg) & = & \reg \\
79-
\regionaux(\reg[i]) & = & \reg \\
80-
&&\\
81-
\offsetaux(\act) & = & \offsetact(\locaux(\act)) \\
82-
\offsetaux(\reg) & = & 0 \\
83-
\offsetaux(\reg[i]) & = & i \\
84-
\end{array}
85-
86-
.. math::
87-
\begin{array}{rcl}
88-
\timeevt(\act^\ast~\AT~\time) & = & \time \\
89-
\\
90-
\ordact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
91-
\ordact(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
92-
\ordact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \SEQCST \\
93-
\\
94-
\overlapact(\act_1, \act_2) \ldots & = & \rangeact(\act_1) \cup \rangeact(\act_2) \neq \epsilon \\
95-
\sameact \ldots & = & \rangeact(\act_1) = \rangeact(\act_2) \\
96-
\\
97-
\readingact(\act) & = & \readact(\act) \neq \epsilon \\
98-
\writingact(\act) & = & \writeact(\act) \neq \epsilon \\
99-
\\
100-
\readact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
101-
\readact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\
102-
\readact(\act) & = & \epsilon \qquad \otherwise \\
103-
&&\\
104-
\writeact(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \epsilon \\
105-
\writeact(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\
106-
\writeact(\act) & = & \epsilon \qquad \otherwise \\
107-
&&\\
108-
\offsetact(\act) & = & \u32 \qquad \iff \locaux(\act) = \reg[\u32] \ \\
109-
\\
110-
\syncact \ldots & = & \ldots \\
111-
\rangeact \ldots & = & \ldots \\
112-
\\
113-
\tearfreeact \ldots & = & \ldots \\
114-
\\
115-
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time) & = & \X{func}(\act) \qquad \iff \locaux(\act) = \reg[\u32] \\
116-
\X{func}_{\reg}(\act_1^\ast~\act~\act_2^\ast~\AT~\time, \act_3^\ast~\act'~\act_4^\ast~\AT~\time') & = & \X{func}(\act.\act') \qquad \iff \locaux(\act) = \locaux(\act') = \reg[\u32] \\
117-
\end{array}
118-
119-
.. todo:: Add more auxiliary functions
120-
12192
.. todo:: add prose intuition
12293

12394
.. math::

‎document/core/util/macros.def‎

Lines changed: 5 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1113,22 +1113,13 @@
11131113
.. |storeval| mathdef:: \xref{exec/runtime}{syntax-storeval}{\X{storeval}}
11141114
.. |notears| mathdef:: \xref{exec/runtime}{syntax-ord}{\X{notears}}
11151115

1116-
.. Events, auxiliary functions
1117-
1118-
.. |ordaux| mathdef:: \xref{exec/relaxed}{exec-ordaux}{\F{ord}}
1119-
.. |locaux| mathdef:: \xref{exec/relaxed}{exec-locaux}{\F{loc}}
1120-
.. |sizeaux| mathdef:: \xref{exec/relaxed}{exec-sizeaux}{\F{size}}
1121-
.. |readaux| mathdef:: \xref{exec/relaxed}{exec-readaux}{\F{read}}
1122-
.. |writeaux| mathdef:: \xref{exec/relaxed}{exec-writeaux}{\F{write}}
1123-
.. |addraux| mathdef:: \xref{exec/relaxed}{exec-addraux}{\F{addr}}
1124-
.. |regionaux| mathdef:: \xref{exec/relaxed}{exec-regionaux}{\F{region}}
1125-
.. |offsetaux| mathdef:: \xref{exec/relaxed}{exec-offsetaux}{\F{offset}}
1126-
11271116

11281117
.. Events, meta functions
1129-
.. |tearing| mathdef:: \xref{exec/runtime}{syntax-ord}{\F{tearing}}
1118+
.. |tearing| mathdef:: \xref{exec/relaxed}{syntax-ord}{\F{tearing}}
11301119

1131-
.. |timeevt| mathdef:: \xref{exec/runtime}{relaxed-aux}{\F{time}}
1120+
.. |timeevt| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{time}}
1121+
1122+
.. |locact| mathdef:: \xref{exec/relaxed}{exec-locact}{\F{loc}}
11321123

11331124
.. |readingact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{reading}}
11341125
.. |ordact| mathdef:: \xref{exec/relaxed}{relaxed-aux}{\F{ord}}
@@ -1162,6 +1153,7 @@
11621153
.. |prechb| mathdef:: \xref{exec/runtime}{relaxed-prechb}{\mathrel{\prec_{\K{hb}}}}
11631154
.. |prectot| mathdef:: \xref{exec/runtime}{relaxed-prectot}{\mathrel{\prec_{\K{tot}}}}
11641155

1156+
11651157
.. Relaxed Memory Model, non-terminals
11661158

11671159
.. |trace| mathdef:: \xref{exec/relaxed}{relaxed-trace}{\X{tr}}

0 commit comments

Comments
 (0)