Lines Matching full:rcu
64 let gp = po ; [Sync-rcu | Sync-srcu] ; po?
69 let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
71 Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
121 (* RCU *)
129 * In the definition of rcu-fence below, the po term at the left-hand side
131 * out. They have been moved into the definitions of rcu-link and rb.
134 let rcu-gp = [Sync-rcu] (* Compare with gp *)
136 let rcu-rscsi = rcu-rscs^-1
141 * one but two non-rf relations, but only in conjunction with an RCU
144 let rcu-link = po? ; hb* ; pb* ; prop ; po
147 * Any sequence containing at least as many grace periods as RCU read-side
148 * critical sections (joined by rcu-link) induces order like a generalized
154 let rec rcu-order = rcu-gp | srcu-gp |
155 (rcu-gp ; rcu-link ; rcu-rscsi) |
156 ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
157 (rcu-rscsi ; rcu-link ; rcu-gp) |
158 ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
159 (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) |
160 ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) |
161 (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) |
162 ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) |
163 (rcu-order ; rcu-link ; rcu-order)
164 let rcu-fence = po ; rcu-order ; po?
165 let fence = fence | rcu-fence
166 let strong-fence = strong-fence | rcu-fence
169 let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
171 irreflexive rb as rcu
174 * The happens-before, propagation, and rcu constraints are all