Skip to content

Commit 1f50dba

Browse files
ioannadioannad
authored
WIP: Memory model aux defs (#209)
* Preliminary addition of auxiliary definitions in the relaxed memory model section. - TODO: use the new macros elsewhere in the text. * Added macro for trace * Found loose b.
1 parent e19c1f4 commit 1f50dba

3 files changed

Lines changed: 75 additions & 22 deletions

File tree

‎document/core/exec/relaxed.rst‎

Lines changed: 58 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,9 @@ A trace is a coinductive set of :ref:`events <syntax-evt>`. A trace is considere
5555

5656
.. math::
5757
\frac{
58-
\config \stepto^{\evt} \config' \qquad \vdash \config' : \X{tr} \qquad \timeevt(\evt) \notin \timeevt^\ast(\X{tr})
58+
\config \stepto^{\evt} \config' \qquad \vdash \config' : \trace \qquad \timeevt(\evt) \notin \timeevt^\ast(\trace)
5959
}{
60-
\vdash \config : \evt~\X{tr}
60+
\vdash \config : \evt~\trace
6161
}
6262
6363
When a WebAssembly program is executed, all behaviours observed during that execution must correspond to a single :ref:`consistent <relaxed-consistent>` pre-execution of that execution's starting :ref:`configuration <syntax-config>`.
@@ -70,57 +70,94 @@ Consistency
7070

7171
.. todo:: define auxiliary functions (either here or in Runtime Structure)
7272

73+
.. math::
74+
\begin{array}{lcl}
75+
\ordaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
76+
\ordaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \ord \\
77+
\ordaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \SEQCST \\
78+
&&\\
79+
\locaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
80+
\locaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \loc \\
81+
\locaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & \loc \\
82+
&&\\
83+
\sizeaux(\ARD_{\ord}~\loc~\byte^n~\NOTEARS^?) & = & n \\
84+
\sizeaux(\AWR_{\ord}~\loc~\byte^n~\NOTEARS^?) & = & n \\
85+
\sizeaux(\ARMW~\loc~{\byte_1}^n~{\byte_2}^n) & = & n \\
86+
&&\\
87+
\readaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
88+
\readaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \epsilon \\
89+
\readaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_1}^\ast \\
90+
&&\\
91+
\writeaux(\ARD_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \epsilon \\
92+
\writeaux(\AWR_{\ord}~\loc~\byte^\ast~\NOTEARS^?) & = & \byte^\ast \\
93+
\writeaux(\ARMW~\loc~{\byte_1}^\ast~{\byte_2}^\ast) & = & {\byte_2}^\ast \\
94+
&&\\
95+
\addraux(\act) & = & \addraux(\regionaux(\act) \\
96+
\addraux(\loc) & = & \addraux(\regionaux(\reg) \\
97+
\addraux(\addr.\fld) & = & \addr \\
98+
&&\\
99+
\regionaux(\act) & = & \regionaux(\locaux(\act) \\
100+
\regionaux(\reg) & = & \reg \\
101+
\regionaux(\reg[i]) & = & \reg \\
102+
&&\\
103+
\offsetaux(\act) & = & \offsetact(\locaux(\act)) \\
104+
\offsetaux(\reg) & = & 0 \\
105+
\offsetaux(\reg[i]) & = & i \\
106+
\end{array}
107+
108+
.. todo:: Add more auxiliary functions
109+
73110
.. todo:: add prose intuition
74111

75112
.. math::
76113
\frac{
77-
\forall \reg, \, \vdash_{\reg} \X{tr} \consistentwith
114+
\forall \reg, \, \vdash_{\reg} \trace \consistentwith
78115
}{
79-
\vdash \X{tr} \consistent
116+
\vdash \trace \consistent
80117
}
81118
82119
.. math::
83120
\frac{
84121
\begin{array}[b]{@{}l@{}}
85-
\forall \evt_R \in \readingact_{\reg}(\X{tr}), \exists \evt_W^\ast,
86-
\X{tr} \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\
87-
\forall \evt_I, \evt \in \X{tr}, \,
88-
\ordact_{\reg}(\evt_I) = \INIT \wedge
122+
\forall \evt_R \in \readingact_{\reg}(\trace), \exists \evt_W^\ast,
123+
\trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast \\
124+
\forall \evt_I, \evt \in \trace, \,
125+
\F{ord}_r(\evt_I) = \INIT \wedge
89126
\evt_I \neq \evt \wedge
90127
\overlapact(\evt_I, \evt) \Rightarrow \evt_I \prechb \evt
91128
\end{array}
92129
}{
93-
\vdash_{\reg} \X{tr} \consistentwith
130+
\vdash_{\reg} \trace \consistentwith
94131
}
95132
96133
.. math::
97134
\frac{
98135
\begin{array}[b]{@{}c@{}}
99136
\left|\evt_W^\ast\right| = |\readact_{\reg}(\evt_R)| \\
100137
\forall i < |\evt_W^\ast|,
101-
\X{tr} \vdash_{\reg}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
138+
\trace \vdash_{\reg}^i \evt_R \readsfrom \left(\evt_W^\ast[i]\right)
102139
\\
103140
\vdash_{\reg} \evt_R \notear \evt_W^\ast
104141
\end{array}
105142
}{
106-
\X{tr} \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast
143+
\trace \vdash_{\reg} \evt_R \readseachfrom \evt_W^\ast
107144
}
108145
109146
.. math::
110147
\frac{
111148
\begin{array}[b]{@{}l@{}}
112149
\evt_R \neq \evt_W \\
113-
\evt_W \in \writingact_{\reg}(\X{tr})
150+
\evt_W \in \writingact_{\reg}(\trace)
114151
\end{array}
115152
\qquad
116153
\begin{array}[b]{@{}r@{}}
117-
\X{tr} \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W \\
118-
\X{tr} \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
154+
\trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W \\
155+
\trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
119156
\end{array}
120157
\qquad
121-
\X{tr} \vdash_{\reg} \evt_R \sclastvisible \evt^\ast_W
158+
\trace \vdash_{\reg} \evt_R \sclastvisible \evt^\ast_W
122159
}{
123-
\X{tr} \vdash_{\reg}^i \evt_R \readsfrom \evt_W
160+
\trace \vdash_{\reg}^i \evt_R \readsfrom \evt_W
124161
}
125162
126163
.. math::
@@ -130,7 +167,7 @@ Consistency
130167
k = \offsetact_{\reg}(\evt_R) + i &=& \offsetact_{\reg}(\evt_W) + j
131168
\end{array}
132169
}{
133-
\X{tr} \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W
170+
\trace \vdash_{\reg}^{i,k} \evt_R \valueconsistent \evt_W
134171
}
135172
136173
.. math::
@@ -141,23 +178,23 @@ Consistency
141178
\end{array}
142179
\qquad
143180
\begin{array}[b]{@{}l@{}}
144-
\forall \evt'_W \in \writingact_{\reg}(\X{tr}),\\
181+
\forall \evt'_W \in \writingact_{\reg}(\trace),\\
145182
\quad \evt_W \prechb \evt'_W \prechb \evt_R \Rightarrow k \notin \rangeact_{\reg}(\evt'_W)
146183
\end{array}
147184
}{
148-
\X{tr} \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
185+
\trace \vdash_{\reg}^k \evt_R \hbconsistent \evt_W
149186
}
150187
151188
.. math::
152189
\frac{
153190
\begin{array}[b]{@{}l@{\qquad}l@{}}
154-
\forall \evt'_W \in \writingact_{\reg}(\X{tr}), \evt_W \prechb \evt_R \Rightarrow \\
191+
\forall \evt'_W \in \writingact_{\reg}(\trace), \evt_W \prechb \evt_R \Rightarrow \\
155192
\quad \evt_W \prectot \evt'_W \prectot \evt_R \wedge \syncact_{\reg}(\evt_W, \evt_R) \Rightarrow \neg \syncact_{\reg}(\evt'_W, \evt_R) \\
156193
\quad \evt_W \prechb \evt'_W \prectot \evt_R \Rightarrow \neg\syncact_{\reg}(\evt'_W, \evt_R) \\
157194
\quad \evt_W \prectot \evt'_W \prechb \evt_R \Rightarrow \neg\syncact_{\reg}(\evt_W, \evt'_W)
158195
\end{array}
159196
}{
160-
\X{tr} \vdash_{\reg} \evt_R \sclastvisible \evt_W
197+
\trace \vdash_{\reg} \evt_R \sclastvisible \evt_W
161198
}
162199
163200
.. math::

‎document/core/exec/runtime.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -706,7 +706,7 @@ Each event is annotated with a :ref:`time stamp <syntax-time>` that uniquely ide
706706
\LDATA \\
707707
\production{(store value)} & \storeval &::=&
708708
\val ~|~
709-
b^\ast \\
709+
\byte^\ast \\
710710
\end{array}
711711
712712
.. todo:: ensure identity of wait + wake operations is preserved

‎document/core/util/macros.def‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1113,6 +1113,18 @@
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+
1127+
11161128
.. Events, meta functions
11171129
.. |tearing| mathdef:: \xref{exec/runtime}{syntax-ord}{\F{tearing}}
11181130

@@ -1150,6 +1162,10 @@
11501162
.. |prechb| mathdef:: \xref{exec/runtime}{relaxed-prechb}{\mathrel{\prec_{\K{hb}}}}
11511163
.. |prectot| mathdef:: \xref{exec/runtime}{relaxed-prectot}{\mathrel{\prec_{\K{tot}}}}
11521164

1165+
.. Relaxed Memory Model, non-terminals
1166+
1167+
.. |trace| mathdef:: \xref{exec/relaxed}{relaxed-trace}{\X{tr}}
1168+
11531169

11541170
.. Stack, terminals
11551171

0 commit comments

Comments
 (0)