1 // SPDX-License-Identifier: GPL-2.0+ 1 // SPDX-License-Identifier: GPL-2.0+
2 (* 2 (*
3 * Copyright (C) 2015 Jade Alglave <j.alglave@u 3 * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>,
4 * Copyright (C) 2016 Luc Maranget <luc.marange 4 * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
5 * Copyright (C) 2017 Alan Stern <stern@rowland 5 * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>,
6 * Andrea Parri <parri.andre 6 * Andrea Parri <parri.andrea@gmail.com>
7 * 7 *
8 * An earlier version of this file appeared in 8 * An earlier version of this file appeared in the companion webpage for
9 * "Frightening small children and disconcerti 9 * "Frightening small children and disconcerting grown-ups: Concurrency
10 * in the Linux kernel" by Alglave, Maranget, 10 * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern,
11 * which appeared in ASPLOS 2018. 11 * which appeared in ASPLOS 2018.
12 *) 12 *)
13 13
14 "Linux-kernel memory consistency model" 14 "Linux-kernel memory consistency model"
15 15
16 (* 16 (*
17 * File "lock.cat" handles locks and is experi 17 * File "lock.cat" handles locks and is experimental.
18 * It can be replaced by include "cos.cat" for 18 * It can be replaced by include "cos.cat" for tests that do not use locks.
19 *) 19 *)
20 20
21 include "lock.cat" 21 include "lock.cat"
22 22
23 (*******************) 23 (*******************)
24 (* Basic relations *) 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-lock-po = po ; [UL] ; (po|rf) ; <<
31 <<
32 (* Fences *) 27 (* Fences *)
33 let R4rmb = R \ Noreturn (* Reads for w !! 28 let rmb = [R \ Noreturn] ; fencerel(Rmb) ; [R \ Noreturn]
34 let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] <<
35 let wmb = [W] ; fencerel(Wmb) ; [W] 29 let wmb = [W] ; fencerel(Wmb) ; [W]
36 let mb = ([M] ; fencerel(Mb) ; [M]) | 30 let mb = ([M] ; fencerel(Mb) ; [M]) |
37 ([M] ; fencerel(Before-atomic) ; [RMW] 31 ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
38 ([M] ; po? ; [RMW] ; fencerel(After-at 32 ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
39 ([M] ; po? ; [LKW] ; fencerel(After-sp !! 33 ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
40 (* !! 34 let gp = po ; [Sync-rcu] ; po?
41 * Note: The po-unlock-lock-po relation only p !! 35
42 * successor, perhaps giving the impression th <<
43 * smp_mb__after_unlock_lock() fence only affe <<
44 * However, in a longer sequence of lock hando <<
45 * A-cumulative release fences of lock-release <<
46 * propagate to one of the involved CPUs befor <<
47 * the next CPU will also propagate to the fin <<
48 * to the CPU that executes the fence. Theref <<
49 * also affected by the fence. <<
50 *) <<
51 ([M] ; po-unlock-lock-po ; <<
52 [After-unlock-lock] ; po ; [M] <<
53 ([M] ; po? ; [Srcu-unlock] ; fencerel( <<
54 let gp = po ; [Sync-rcu | Sync-srcu] ; po? <<
55 let strong-fence = mb | gp 36 let strong-fence = mb | gp
56 37
57 let nonrw-fence = strong-fence | po-rel | acq- !! 38 (* Release Acquire *)
58 let fence = nonrw-fence | wmb | rmb !! 39 let acq-po = [Acquire] ; po ; [M]
59 let barrier = fencerel(Barrier | Rmb | Wmb | M !! 40 let po-rel = [M] ; po ; [Release]
60 Before-atomic | After-atomic | !! 41 let po-unlock-rf-lock-po = po ; [UL] ; rf ; [LKR] ; po
61 Rcu-lock | Rcu-unlock | Srcu-l <<
62 (po ; [Release]) | ([Acquire] ; po) <<
63 42
64 (**********************************) 43 (**********************************)
65 (* Fundamental coherence ordering *) 44 (* Fundamental coherence ordering *)
66 (**********************************) 45 (**********************************)
67 46
68 (* Sequential Consistency Per Variable *) 47 (* Sequential Consistency Per Variable *)
69 let com = rf | co | fr 48 let com = rf | co | fr
70 acyclic po-loc | com as coherence 49 acyclic po-loc | com as coherence
71 50
72 (* Atomic Read-Modify-Write *) 51 (* Atomic Read-Modify-Write *)
73 empty rmw & (fre ; coe) as atomic 52 empty rmw & (fre ; coe) as atomic
74 53
75 (**********************************) 54 (**********************************)
76 (* Instruction execution ordering *) 55 (* Instruction execution ordering *)
77 (**********************************) 56 (**********************************)
78 57
79 (* Preserved Program Order *) 58 (* Preserved Program Order *)
80 let dep = addr | data 59 let dep = addr | data
81 let rwdep = (dep | ctrl) ; [W] 60 let rwdep = (dep | ctrl) ; [W]
82 let overwrite = co | fr 61 let overwrite = co | fr
83 let to-w = rwdep | (overwrite & int) | (addr ; !! 62 let to-w = rwdep | (overwrite & int)
84 let to-r = (addr ; [R]) | (dep ; [Marked] ; rf !! 63 let to-r = addr | (dep ; rfi)
85 let ppo = to-r | to-w | (fence & int) | (po-un !! 64 let fence = strong-fence | wmb | po-rel | rmb | acq-po
>> 65 let ppo = to-r | to-w | fence | (po-unlock-rf-lock-po & int)
86 66
87 (* Propagation: Ordering from release operatio 67 (* Propagation: Ordering from release operations and strong fences. *)
88 let A-cumul(r) = (rfe ; [Marked])? ; r !! 68 let A-cumul(r) = rfe? ; r
89 let rmw-sequence = (rf ; rmw)* !! 69 let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | po-unlock-rf-lock-po
90 let cumul-fence = [Marked] ; (A-cumul(strong-f !! 70 let prop = (overwrite & ext)? ; cumul-fence* ; rfe?
91 po-unlock-lock-po) ; [Marked] ; rmw-se <<
92 let prop = [Marked] ; (overwrite & ext)? ; cum <<
93 [Marked] ; rfe? ; [Marked] <<
94 71
95 (* 72 (*
96 * Happens Before: Ordering from the passage o 73 * Happens Before: Ordering from the passage of time.
97 * No fences needed here for prop because rela 74 * No fences needed here for prop because relation confined to one process.
98 *) 75 *)
99 let hb = [Marked] ; (ppo | rfe | ((prop \ id) !! 76 let hb = ppo | rfe | ((prop \ id) & int)
100 acyclic hb as happens-before 77 acyclic hb as happens-before
101 78
102 (****************************************) 79 (****************************************)
103 (* Write and fence propagation ordering *) 80 (* Write and fence propagation ordering *)
104 (****************************************) 81 (****************************************)
105 82
106 (* Propagation: Each non-rf link needs a stron 83 (* Propagation: Each non-rf link needs a strong fence. *)
107 let pb = prop ; strong-fence ; hb* ; [Marked] !! 84 let pb = prop ; strong-fence ; hb*
108 acyclic pb as propagation 85 acyclic pb as propagation
109 86
110 (*******) 87 (*******)
111 (* RCU *) 88 (* RCU *)
112 (*******) 89 (*******)
113 90
114 (* 91 (*
115 * Effects of read-side critical sections proc !! 92 * Effect of read-side critical section proceeds from the rcu_read_lock()
116 * or srcu_read_unlock() backwards on the one !! 93 * onward on the one hand and from the rcu_read_unlock() backwards on the
117 * rcu_read_lock() or srcu_read_lock() forward !! 94 * other hand.
118 * <<
119 * In the definition of rcu-fence below, the p <<
120 * of each disjunct and the po? term at the ri <<
121 * out. They have been moved into the definit <<
122 * This was necessary in order to apply the "& <<
123 *) 95 *)
124 let rcu-gp = [Sync-rcu] (* Compare wit !! 96 let rscs = po ; crit^-1 ; po?
125 let srcu-gp = [Sync-srcu] <<
126 let rcu-rscsi = rcu-rscs^-1 <<
127 let srcu-rscsi = srcu-rscs^-1 <<
128 97
129 (* 98 (*
130 * The synchronize_rcu() strong fence is speci 99 * The synchronize_rcu() strong fence is special in that it can order not
131 * one but two non-rf relations, but only in c 100 * one but two non-rf relations, but only in conjunction with an RCU
132 * read-side critical section. 101 * read-side critical section.
133 *) 102 *)
134 let rcu-link = po? ; hb* ; pb* ; prop ; po !! 103 let rcu-link = hb* ; pb* ; prop
135 104
136 (* 105 (*
137 * Any sequence containing at least as many gr 106 * Any sequence containing at least as many grace periods as RCU read-side
138 * critical sections (joined by rcu-link) indu !! 107 * critical sections (joined by rcu-link) acts as a generalized strong fence.
139 * inter-CPU strong fence. <<
140 * Likewise for SRCU grace periods and read-si <<
141 * the synchronize_srcu() and srcu_read_[un]lo <<
142 * struct srcu_struct location. <<
143 *) 108 *)
144 let rec rcu-order = rcu-gp | srcu-gp | !! 109 let rec rcu-fence = gp |
145 (rcu-gp ; rcu-link ; rcu-rscsi) | !! 110 (gp ; rcu-link ; rscs) |
146 ((srcu-gp ; rcu-link ; srcu-rscsi) & l !! 111 (rscs ; rcu-link ; gp) |
147 (rcu-rscsi ; rcu-link ; rcu-gp) | !! 112 (gp ; rcu-link ; rcu-fence ; rcu-link ; rscs) |
148 ((srcu-rscsi ; rcu-link ; srcu-gp) & l !! 113 (rscs ; rcu-link ; rcu-fence ; rcu-link ; gp) |
149 (rcu-gp ; rcu-link ; rcu-order ; rcu-l !! 114 (rcu-fence ; rcu-link ; rcu-fence)
150 ((srcu-gp ; rcu-link ; rcu-order ; rcu <<
151 (rcu-rscsi ; rcu-link ; rcu-order ; rc <<
152 ((srcu-rscsi ; rcu-link ; rcu-order ; <<
153 (rcu-order ; rcu-link ; rcu-order) <<
154 let rcu-fence = po ; rcu-order ; po? <<
155 let fence = fence | rcu-fence <<
156 let strong-fence = strong-fence | rcu-fence <<
157 115
158 (* rb orders instructions just as pb does *) 116 (* rb orders instructions just as pb does *)
159 let rb = prop ; rcu-fence ; hb* ; pb* ; [Marke !! 117 let rb = prop ; rcu-fence ; hb* ; pb*
160 118
161 irreflexive rb as rcu 119 irreflexive rb as rcu
162 120
163 (* 121 (*
164 * The happens-before, propagation, and rcu co 122 * The happens-before, propagation, and rcu constraints are all
165 * expressions of temporal ordering. They cou 123 * expressions of temporal ordering. They could be replaced by
166 * a single constraint on an "executes-before" 124 * a single constraint on an "executes-before" relation, xb:
167 * 125 *
168 * let xb = hb | pb | rb 126 * let xb = hb | pb | rb
169 * acyclic xb as executes-before 127 * acyclic xb as executes-before
170 *) 128 *)
171 <<
172 (*********************************) <<
173 (* Plain accesses and data races *) <<
174 (*********************************) <<
175 <<
176 (* Warn about plain writes and marked accesses <<
177 let mixed-accesses = ([Plain & W] ; (po-loc \ <<
178 ([Marked] ; (po-loc \ barrier) ; [Plai <<
179 flag ~empty mixed-accesses as mixed-accesses <<
180 <<
181 (* Executes-before and visibility *) <<
182 let xbstar = (hb | pb | rb)* <<
183 let vis = cumul-fence* ; rfe? ; [Marked] ; <<
184 ((strong-fence ; [Marked] ; xbstar) | <<
185 <<
186 (* Boundaries for lifetimes of plain accesses <<
187 let w-pre-bounded = [Marked] ; (addr | fence)? <<
188 let r-pre-bounded = [Marked] ; (addr | nonrw-f <<
189 ([R4rmb] ; fencerel(Rmb) ; [~Noreturn] <<
190 let w-post-bounded = fence? ; [Marked] ; rmw-s <<
191 let r-post-bounded = (nonrw-fence | ([~Noretur <<
192 [Marked] <<
193 <<
194 (* Visibility and executes-before for plain ac <<
195 let ww-vis = fence | (strong-fence ; xbstar ; <<
196 (w-post-bounded ; vis ; w-pre-bounded) <<
197 let wr-vis = fence | (strong-fence ; xbstar ; <<
198 (w-post-bounded ; vis ; r-pre-bounded) <<
199 let rw-xbstar = fence | (r-post-bounded ; xbst <<
200 <<
201 (* Potential races *) <<
202 let pre-race = ext & ((Plain * M) | ((M \ IW) <<
203 <<
204 (* Coherence requirements for plain accesses * <<
205 let wr-incoh = pre-race & rf & rw-xbstar^-1 <<
206 let rw-incoh = pre-race & fr & wr-vis^-1 <<
207 let ww-incoh = pre-race & co & ww-vis^-1 <<
208 empty (wr-incoh | rw-incoh | ww-incoh) as plai <<
209 <<
210 (* Actual races *) <<
211 let ww-nonrace = ww-vis & ((Marked * W) | rw-x <<
212 let ww-race = (pre-race & co) \ ww-nonrace <<
213 let wr-race = (pre-race & (co? ; rf)) \ wr-vis <<
214 let rw-race = (pre-race & fr) \ rw-xbstar <<
215 <<
216 flag ~empty (ww-race | wr-race | rw-race) as d <<
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.