移去rt

hc

2023-12-08 01573e231f18eb2d99162747186f59511f56b64d

 kernel/tools/memory-model/linux-kernel.cat
..
..
@@ -24,21 +24,30 @@
24
24
 (* Basic relations *)
25
25
 (*******************)
26
26
 
27
+(* Release Acquire *)
28
+let acq-po = [Acquire] ; po ; [M]
29
+let po-rel = [M] ; po ; [Release]
30
+let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
31
+
27
32
 (* Fences *)
28
-let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
33
+let R4rmb = R \ Noreturn	(* Reads for which rmb works *)
34
+let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
29
35
 let wmb = [W] ; fencerel(Wmb) ; [W]
30
36
 let mb = ([M] ; fencerel(Mb) ; [M]) |
31
37
 	([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
32
38
 	([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
33
-	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
34
-let gp = po ; [Sync-rcu] ; po?
35
-
39
+	([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
40
+	([M] ; po ; [UL] ; (co | po) ; [LKW] ;
41
+		fencerel(After-unlock-lock) ; [M])
42
+let gp = po ; [Sync-rcu | Sync-srcu] ; po?
36
43
 let strong-fence = mb | gp
37
44
 
38
-(* Release Acquire *)
39
-let acq-po = [Acquire] ; po ; [M]
40
-let po-rel = [M] ; po ; [Release]
41
-let rfi-rel-acq = [Release] ; rfi ; [Acquire]
45
+let nonrw-fence = strong-fence | po-rel | acq-po
46
+let fence = nonrw-fence | wmb | rmb
47
+let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
48
+		Before-atomic | After-atomic | Acquire | Release |
49
+		Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
50
+	(po ; [Release]) | ([Acquire] ; po)
42
51
 
43
52
 (**********************************)
44
53
 (* Fundamental coherence ordering *)
..
..
@@ -59,21 +68,22 @@
59
68
 let dep = addr | data
60
69
 let rwdep = (dep | ctrl) ; [W]
61
70
 let overwrite = co | fr
62
-let to-w = rwdep | (overwrite & int)
63
-let to-r = addr | (dep ; rfi) | rfi-rel-acq
64
-let fence = strong-fence | wmb | po-rel | rmb | acq-po
65
-let ppo = to-r | to-w | fence
71
+let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
72
+let to-r = addr | (dep ; [Marked] ; rfi)
73
+let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
66
74
 
67
75
 (* Propagation: Ordering from release operations and strong fences. *)
68
-let A-cumul(r) = rfe? ; r
69
-let cumul-fence = A-cumul(strong-fence | po-rel) | wmb
70
-let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
76
+let A-cumul(r) = (rfe ; [Marked])? ; r
77
+let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb |
78
+	po-unlock-rf-lock-po) ; [Marked]
79
+let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ;
80
+	[Marked] ; rfe? ; [Marked]
71
81
 
72
82
 (*
73
83
  * Happens Before: Ordering from the passage of time.
74
84
  * No fences needed here for prop because relation confined to one process.
75
85
  *)
76
-let hb = ppo | rfe | ((prop \ id) & int)
86
+let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked]
77
87
 acyclic hb as happens-before
78
88
 
79
89
 (****************************************)
..
..
@@ -81,7 +91,7 @@
81
91
 (****************************************)
82
92
 
83
93
 (* Propagation: Each non-rf link needs a strong fence. *)
84
-let pb = prop ; strong-fence ; hb*
94
+let pb = prop ; strong-fence ; hb* ; [Marked]
85
95
 acyclic pb as propagation
86
96
 
87
97
 (*******)
..
..
@@ -89,32 +99,51 @@
89
99
 (*******)
90
100
 
91
101
 (*
92
- * Effect of read-side critical section proceeds from the rcu_read_lock()
93
- * onward on the one hand and from the rcu_read_unlock() backwards on the
94
- * other hand.
102
+ * Effects of read-side critical sections proceed from the rcu_read_unlock()
103
+ * or srcu_read_unlock() backwards on the one hand, and from the
104
+ * rcu_read_lock() or srcu_read_lock() forwards on the other hand.
105
+ *
106
+ * In the definition of rcu-fence below, the po term at the left-hand side
107
+ * of each disjunct and the po? term at the right-hand end have been factored
108
+ * out.  They have been moved into the definitions of rcu-link and rb.
109
+ * This was necessary in order to apply the "& loc" tests correctly.
95
110
  *)
96
-let rscs = po ; crit^-1 ; po?
111
+let rcu-gp = [Sync-rcu]		(* Compare with gp *)
112
+let srcu-gp = [Sync-srcu]
113
+let rcu-rscsi = rcu-rscs^-1
114
+let srcu-rscsi = srcu-rscs^-1
97
115
 
98
116
 (*
99
117
  * The synchronize_rcu() strong fence is special in that it can order not
100
118
  * one but two non-rf relations, but only in conjunction with an RCU
101
119
  * read-side critical section.
102
120
  *)
103
-let rcu-link = hb* ; pb* ; prop
121
+let rcu-link = po? ; hb* ; pb* ; prop ; po
104
122
 
105
123
 (*
106
124
  * Any sequence containing at least as many grace periods as RCU read-side
107
- * critical sections (joined by rcu-link) acts as a generalized strong fence.
125
+ * critical sections (joined by rcu-link) induces order like a generalized
126
+ * inter-CPU strong fence.
127
+ * Likewise for SRCU grace periods and read-side critical sections, provided
128
+ * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same
129
+ * struct srcu_struct location.
108
130
  *)
109
-let rec rcu-fence = gp |
110
-	(gp ; rcu-link ; rscs) |
111
-	(rscs ; rcu-link ; gp) |
112
-	(gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) |
113
-	(rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) |
114
-	(rcu-fence ; rcu-link ; rcu-fence)
131
+let rec rcu-order = rcu-gp | srcu-gp |
132
+	(rcu-gp ; rcu-link ; rcu-rscsi) |
133
+	((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
134
+	(rcu-rscsi ; rcu-link ; rcu-gp) |
135
+	((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
136
+	(rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) |
137
+	((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) |
138
+	(rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) |
139
+	((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) |
140
+	(rcu-order ; rcu-link ; rcu-order)
141
+let rcu-fence = po ; rcu-order ; po?
142
+let fence = fence | rcu-fence
143
+let strong-fence = strong-fence | rcu-fence
115
144
 
116
145
 (* rb orders instructions just as pb does *)
117
-let rb = prop ; rcu-fence ; hb* ; pb*
146
+let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
118
147
 
119
148
 irreflexive rb as rcu
120
149
 
..
..
@@ -126,3 +155,49 @@
126
155
  * let xb = hb | pb | rb
127
156
  * acyclic xb as executes-before
128
157
  *)
158
+
159
+(*********************************)
160
+(* Plain accesses and data races *)
161
+(*********************************)
162
+
163
+(* Warn about plain writes and marked accesses in the same region *)
164
+let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) |
165
+	([Marked] ; (po-loc \ barrier) ; [Plain & W])
166
+flag ~empty mixed-accesses as mixed-accesses
167
+
168
+(* Executes-before and visibility *)
169
+let xbstar = (hb | pb | rb)*
170
+let vis = cumul-fence* ; rfe? ; [Marked] ;
171
+	((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
172
+
173
+(* Boundaries for lifetimes of plain accesses *)
174
+let w-pre-bounded = [Marked] ; (addr | fence)?
175
+let r-pre-bounded = [Marked] ; (addr | nonrw-fence |
176
+	([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))?
177
+let w-post-bounded = fence? ; [Marked]
178
+let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ;
179
+	[Marked]
180
+
181
+(* Visibility and executes-before for plain accesses *)
182
+let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) |
183
+	(w-post-bounded ; vis ; w-pre-bounded)
184
+let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) |
185
+	(w-post-bounded ; vis ; r-pre-bounded)
186
+let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded)
187
+
188
+(* Potential races *)
189
+let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain))
190
+
191
+(* Coherence requirements for plain accesses *)
192
+let wr-incoh = pre-race & rf & rw-xbstar^-1
193
+let rw-incoh = pre-race & fr & wr-vis^-1
194
+let ww-incoh = pre-race & co & ww-vis^-1
195
+empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence
196
+
197
+(* Actual races *)
198
+let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis)
199
+let ww-race = (pre-race & co) \ ww-nonrace
200
+let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1
201
+let rw-race = (pre-race & fr) \ rw-xbstar
202
+
203
+flag ~empty (ww-race | wr-race | rw-race) as data-race