Skip to content

Commit 5243912

Browse files
author
Shale Xiong
committed
[gen] Add more rmw to match memory access.
1 parent 508a0de commit 5243912

1 file changed

Lines changed: 72 additions & 2 deletions

File tree

‎gen/libdir/forbidden.conf‎

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,7 @@
7171

7272
#let lwfs = [Exp & M | Imp & Tag & R]; (po & same-loc); [Exp & W]
7373
-safe Pos*W
74+
-safe [Pos*R Amo.Swp] [Pos*R Amo.Cas] [Pos*R Amo.StAdd] [Pos*R Amo.LdAdd] [Pos*R LxSx]
7475

7576
### Data and address dependance
7677
# let data = [Exp & R]; (basic-dep; [DATA]; iico_data+; [Exp & W]) & ~same-instance
@@ -90,15 +91,35 @@
9091
-safe [DpCtrldW ExpObs]
9192
# `DpCtrlsW` is stronger than `Pos*W`.
9293
#-safe DpCtrlsW
94+
-safe [DpCtrldR Amo.Cas] [DpCtrldR Amo.Swp] [DpCtrldR Amo.StAdd] [DpCtrldR Amo.LdAdd] [DpCtrldR LxSx]
95+
#`[DpCtrlsR rmw]` is stronger than `Pos*W`.
96+
#-safe [DpCtrlsR Amo.Cas] [DpCtrlsR Amo.Swp] [DpCtrlsR LxSx]
9397

9498
# let dob = addr; [Exp & M]; po; [Exp & W | HU]
9599
-safe [DpAddr Pod*W] [DpAddrd* Pos*W]
96100
# `[DpAddrs* Pos*W]` are stronger than `Pos*W` as the former are a read followed by a write to the same location.
97101
#-safe [DpAddrs* Pos*W]
102+
-safe [DpAddr*R Amo.Swp PodWW]
103+
-safe [DpAddr*R Amo.Cas PodWW]
104+
-safe [DpAddr*R Amo.StAdd PodWW]
105+
-safe [DpAddr*R Amo.LdAdd PodWW]
106+
-safe [DpAddr*R LxSx PodWW]
107+
# `[DpAddrdR rmw PosWW]` can be combined by `diy` as `[DpAddrdR rmw]` and `PosWW`
108+
-safe [DpAddrd* Po**R Amo.Swp] [DpAddrs* Pod*R Amo.Swp]
109+
-safe [DpAddrd* Po**R Amo.Cas] [DpAddrs* Pod*R Amo.Cas]
110+
-safe [DpAddrd* Po**R Amo.StAdd] [DpAddrs* Pod*R Amo.StAdd]
111+
-safe [DpAddrd* Po**R Amo.LdAdd] [DpAddrs* Pod*R Amo.LdAdd]
112+
-safe [DpAddrd* Po**R LxSx] [DpAddrs* Pod*R LxSx]
113+
# `[DpAddrs* Pos*R rmw]` is stronger than `Pos*W`.
98114

99115
# let dob = addr; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
100116
# let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
101117
-safe [DpAddr*W PosWR]
118+
-safe [DpAddrdR Amo.Swp PosWR] [DpAddrsR Amo.Swp PosWR]
119+
-safe [DpAddrdR Amo.Cas PosWR] [DpAddrsR Amo.Cas PosWR]
120+
-safe [DpAddrdR Amo.StAdd PosWR] [DpAddrsR Amo.StAdd PosWR]
121+
-safe [DpAddrdR Amo.LdAdd PosWR] [DpAddrsR Amo.LdAdd PosWR]
122+
-safe [DpAddrdR LxSx PosWR] [DpAddrsR LxSx PosWR]
102123

103124
# let dob = data; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
104125
# let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
@@ -125,18 +146,33 @@
125146
#-safe [DpAddr** ISB**W]
126147
# `[DpAddrdW ISBsWR]` is stronger than `[DpAddrdW PosWR]`.
127148
#-safe [DpAddrdW ISBsWR]
149+
-safe [DpAddr*R Amo.Swp ISBdWR ExpObs]
150+
-safe [DpAddr*R Amo.Cas ISBdWR ExpObs]
151+
-safe [DpAddr*R Amo.StAdd ISBdWR ExpObs]
152+
-safe [DpAddr*R Amo.LdAdd ISBdWR ExpObs]
153+
-safe [DpAddr*R LxSx ISBdWR ExpObs]
154+
# `[DpAddr*R rmw ISBsWR]` is stronger than `[DpAddr*R rmw PosWR]`
155+
#-safe [DpAddrdR Amo.Swp ISBsWR] [DpAddrsR Amo.Swp ISBsWR]
156+
#-safe [DpAddrdR Amo.Cas ISBsWR] [DpAddrsR Amo.Cas ISBsWR]
157+
#-safe [DpAddrdR LxSx ISBsWR] [DpAddrsR LxSx ISBsWR]
128158

129159
# let IFB-ob = [Exp & R]; pick-addr-dep; [Exp & M]; po; [IFB]; po
130160
-safe [DpAddrCsel ISB**R ExpObs]
131161
# `[DpAddrCsels* ISBs*W]` are stronger than `Pos*W` as the former are a read followed by a write to the same location.
132162
#-safe [DpAddrCsels* ISBs*W]
133163
# `[DpAddrCsel** ISB**W]` is stronger than `[DpAddr** Po**W]`
134164
#-safe [DpAddrCsel** ISB**W]
165+
-safe [DpAddrCsel*R Amo.Swp ISB*WR ExpObs]
166+
-safe [DpAddrCsel*R Amo.Cas ISB*WR ExpObs]
167+
-safe [DpAddrCsel*R Amo.StAdd ISB*WR ExpObs]
168+
-safe [DpAddrCsel*R Amo.LdAdd ISB*WR ExpObs]
169+
-safe [DpAddrCsel*R LxSx ISB*WR ExpObs]
135170

136171
# let pob = pick-addr-dep; [Exp & W | HU | TLBI | DC.CVAU | IC]
137172
-safe DpAddrCseldW
138173
# `DpAddrCselsW` is stronger than `Pos*W`.
139174
#-safe DpAddrCselsW
175+
-safe [DpAddrCseldR Amo.Swp] [DpAddrCseldR Amo.Cas] [DpAddrCseldR Amo.StAdd] [DpAddrCseldR Amo.LdAdd] [DpAddrCseldR LxSx]
140176

141177
# let pob = pick-data-dep
142178
-safe DpDataCseldW
@@ -147,11 +183,39 @@
147183
-safe DpCtrlCseldW
148184
# `DpCtrlCselsW` is stronger than `Pos*W`.
149185
#-safe DpCtrlCselsW
186+
-safe [DpCtrlCseldR Amo.Swp] [DpCtrlCseldR Amo.Cas] [DpCtrlCseldR Amo.StAdd] [DpCtrlCseldR Amo.LdAdd] [DpCtrlCseldR LxSx]
150187

151188
# let pob = pick-addr-dep; [Exp & M]; po; [Exp & W | HU]
152189
-safe [DpAddrCsel Pod*W] [DpAddrCseld* Pos*W]
153190
# `[DpAddrCsels* Pos*W]` are stronger than `Pos*W` as the former are a read followed by a write to the same location.
154191
#-safe [DpAddrCsels* Pos*W]
192+
-safe [DpAddrCsel*R Amo.Swp Po*WW]
193+
-safe [DpAddrCsel*R Amo.Cas Po*WW]
194+
-safe [DpAddrCsel*R Amo.StAdd Po*WW]
195+
-safe [DpAddrCsel*R Amo.LdAdd Po*WW]
196+
-safe [DpAddrCsel*R LxSx Po*WW]
197+
#
198+
-safe [DpAddrCseld* Po**R Amo.Swp] [DpAddrCsels* Pod*R Amo.Swp]
199+
-safe [DpAddrCseld* Po**R Amo.Cas] [DpAddrCsels* Pod*R Amo.Cas]
200+
-safe [DpAddrCseld* Po**R Amo.StAdd] [DpAddrCsels* Pod*R Amo.StAdd]
201+
-safe [DpAddrCseld* Po**R Amo.LdAdd] [DpAddrCsels* Pod*R Amo.LdAdd]
202+
-safe [DpAddrCseld* Po**R LxSx] [DpAddrCsels* Pod*R LxSx]
203+
# `[DpAddrCsels* Pos*R rmw]` is stronger than `Pos*W`.
204+
-safe [DpAddrCseldR Amo.Swp Po*WR Amo.Swp] [DpAddrCseldR Amo.Swp Po*WR Amo.Cas] [DpAddrCseldR Amo.Swp Po*WR Amo.StAdd] [DpAddrCseldR Amo.Swp Po*WR Amo.LdAdd] [DpAddrCseldR Amo.Swp Po*WR LxSx]
205+
-safe [DpAddrCselsR Amo.Swp PodWR Amo.Swp] [DpAddrCselsR Amo.Swp PodWR Amo.Cas] [DpAddrCselsR Amo.Swp PodWR Amo.StAdd] [DpAddrCselsR Amo.Swp PodWR Amo.LdAdd] [DpAddrCselsR Amo.Swp PodWR LxSx]
206+
#
207+
-safe [DpAddrCseldR Amo.Cas Po*WR Amo.Swp] [DpAddrCseldR Amo.Cas Po*WR Amo.Cas] [DpAddrCseldR Amo.Cas Po*WR Amo.StAdd] [DpAddrCseldR Amo.Cas Po*WR Amo.LdAdd] [DpAddrCseldR Amo.Cas Po*WR LxSx]
208+
-safe [DpAddrCselsR Amo.Cas PodWR Amo.Swp] [DpAddrCselsR Amo.Cas PodWR Amo.Cas] [DpAddrCselsR Amo.Cas PodWR Amo.StAdd] [DpAddrCselsR Amo.Cas PodWR Amo.LdAdd] [DpAddrCselsR Amo.Cas PodWR LxSx]
209+
#
210+
-safe [DpAddrCseldR Amo.StAdd Po*WR Amo.Swp] [DpAddrCseldR Amo.StAdd Po*WR Amo.Cas] [DpAddrCseldR Amo.StAdd Po*WR Amo.StAdd] [DpAddrCseldR Amo.StAdd Po*WR Amo.LdAdd] [DpAddrCseldR Amo.StAdd Po*WR LxSx]
211+
-safe [DpAddrCselsR Amo.StAdd PodWR Amo.Swp] [DpAddrCselsR Amo.StAdd PodWR Amo.Cas] [DpAddrCselsR Amo.StAdd PodWR Amo.StAdd] [DpAddrCselsR Amo.StAdd PodWR Amo.LdAdd] [DpAddrCselsR Amo.StAdd PodWR LxSx]
212+
#
213+
-safe [DpAddrCseldR Amo.LdAdd Po*WR Amo.Swp] [DpAddrCseldR Amo.LdAdd Po*WR Amo.Cas] [DpAddrCseldR Amo.LdAdd Po*WR Amo.StAdd] [DpAddrCseldR Amo.LdAdd Po*WR Amo.LdAdd] [DpAddrCseldR Amo.LdAdd Po*WR LxSx]
214+
-safe [DpAddrCselsR Amo.LdAdd PodWR Amo.Swp] [DpAddrCselsR Amo.LdAdd PodWR Amo.Cas] [DpAddrCselsR Amo.LdAdd PodWR Amo.StAdd] [DpAddrCselsR Amo.LdAdd PodWR Amo.LdAdd] [DpAddrCselsR Amo.LdAdd PodWR LxSx]
215+
#
216+
-safe [DpAddrCseldR LxSx Po*WR Amo.Swp] [DpAddrCseldR LxSx Po*WR Amo.Cas] [DpAddrCseldR LxSx Po*WR Amo.StAdd] [DpAddrCseldR LxSx Po*WR Amo.LdAdd] [DpAddrCseldR LxSx Po*WR LxSx]
217+
-safe [DpAddrCselsR LxSx PodWR Amo.Swp] [DpAddrCselsR LxSx PodWR Amo.Cas] [DpAddrCselsR LxSx PodWR Amo.StAdd] [DpAddrCselsR LxSx PodWR Amo.LdAdd] [DpAddrCselsR LxSx PodWR LxSx]
218+
# `[DpAddrCselsR rmw PosWR rmw]` is stronger than `Pos*W`
155219

156220
### Fence
157221

@@ -165,11 +229,15 @@
165229
-safe [DMB.LDdR* ExpObs] [DMB.LDsRR ExpObs]
166230
# `DMB.LDsRW` is stronger than `Pos*W`.
167231
#-safe DMB.LDsRW
232+
-safe [Amo.Swp DMB.LDdW*] [Amo.Cas DMB.LDdW*] [Amo.LdAdd DMB.LDdW*] [LxSx DMB.LDdW*]
233+
-safe [Amo.Swp DMB.LDsWR] [Amo.Cas DMB.LDsWR] [Amo.LdAdd DMB.LDsWR] [LxSx DMB.LDsWR]
234+
# `[DMB.LD*R* rmw]` can be combined by `diy`
168235

169236
# let bob = [Exp & W]; po; [dmb.st]; po; [Exp & W | MMU & FAULT]
170237
-safe DMB.STdWW
171238
# `DMB.STsWW` is stronger than `Pos*W`.
172239
#-safe DMB.STsWW
240+
-safe [DMB.STdWR Amo.Swp] [DMB.STdWR Amo.Cas] [DMB.STdWR Amo.StAdd] [DMB.STdWR Amo.LdAdd] [DMB.STdWR LxSx]
173241

174242
# let DSB-ob = [M | DC.CVAU | IC]; po; [dsb.full]; po; [~(Imp & TTD & M | Imp & Instr & R)]
175243
# DSB.ISH*** DSB.OSH*** in `-moreedges` in `diy7`; these two edges also satisfy `dsb.full`
@@ -181,6 +249,8 @@
181249
-safe [DSB.LDdR* ExpObs] [DSB.LDsRR ExpObs]
182250
# `DSB.LDsRW` is stronger than `Pos*W`.
183251
#-safe DSB.LDsRW
252+
-safe [Amo.Swp DSB.LDdW*] [Amo.Cas DSB.LDdW*] [Amo.LdAdd DSB.LDdW*] [LxSx DSB.LDdW*]
253+
-safe [Amo.Swp DSB.LDsWR] [Amo.Cas DSB.LDsWR] [Amo.LdAdd DSB.LDsWR] [LxSx DSB.LDsWR]
184254

185255
# let DSB-ob = [Exp & W]; po; [dsb.st]; po; [~(Imp & TTD & M | Imp & Instr & R)]
186256
-safe [DSB.STdW* ExpObs] [DSB.STsWR ExpObs]
@@ -190,6 +260,7 @@
190260
### Acquire-Release load and store
191261
# let bob = [L]; po; [A]
192262
-safe [L Po*WR A]
263+
# `[(rmw) L Po*WR A (rmw)]` can be combined by `diy`
193264

194265
### Atomic operation
195266
# Amo.Swp
@@ -204,7 +275,6 @@
204275
-safe [A PodR* ExpObs] [A PosRR ExpObs] [Q PodR* ExpObs] [Q PosRR ExpObs]
205276
# `[A|Q PosRW]` is stronger than `PosRW`
206277
#-safe [A PosRW] [Q PosRW]
207-
208278
# An acquire atomic operation followed by a memory access also matches above
209279
-safe [A Amo.Swp PodW* ExpObs] [A Amo.Swp PosWR ExpObs]
210280
-safe [A Amo.Cas PodW* ExpObs] [A Amo.Cas PosWR ExpObs]
@@ -226,7 +296,7 @@
226296
-safe [ExpObs Pod*R Amo.LdAdd L]
227297
-safe [ExpObs Pod*R LxSx L]
228298
# `[Pos*R rmw L]` is stronger than `Pos*W`
229-
#-safe [Pos*R Amo.Swp L] [Pos*R Amo.Cas L] [Pos*R LxSx L]
299+
#-safe [Pos*R Amo.Swp L] [Pos*R Amo.Cas L] [Pos*R LxSx L]
230300

231301
# let aob = [Exp & M]; rmw; [Exp & M]
232302
-safe LxSx Amo.Swp Amo.Cas

0 commit comments

Comments
 (0)