Lines Matching full:rcu
54 let gp = po ; [Sync-rcu | Sync-srcu] ; po?
59 let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
61 Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
111 (* RCU *)
119 * In the definition of rcu-fence below, the po term at the left-hand side
121 * out. They have been moved into the definitions of rcu-link and rb.
124 let rcu-gp = [Sync-rcu] (* Compare with gp *)
126 let rcu-rscsi = rcu-rscs^-1
131 * one but two non-rf relations, but only in conjunction with an RCU
134 let rcu-link = po? ; hb* ; pb* ; prop ; po
137 * Any sequence containing at least as many grace periods as RCU read-side
138 * critical sections (joined by rcu-link) induces order like a generalized
144 let rec rcu-order = rcu-gp | srcu-gp |
145 (rcu-gp ; rcu-link ; rcu-rscsi) |
146 ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) |
147 (rcu-rscsi ; rcu-link ; rcu-gp) |
148 ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) |
149 (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) |
150 ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) |
151 (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) |
152 ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) |
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
159 let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
161 irreflexive rb as rcu
164 * The happens-before, propagation, and rcu constraints are all