Lines Matching full:rcu
42 let gp = po ; [Sync-rcu | Sync-srcu] ; po?
47 let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu |
49 Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) |
98 (* RCU *)
106 * In the definition of rcu-fence below, the po term at the left-hand side
108 * out. They have been moved into the definitions of rcu-link and rb.
111 let rcu-gp = [Sync-rcu] (* Compare with gp *)
113 let rcu-rscsi = rcu-rscs^-1
118 * one but two non-rf relations, but only in conjunction with an RCU
121 let rcu-link = po? ; hb* ; pb* ; prop ; po
124 * Any sequence containing at least as many grace periods as RCU read-side
125 * critical sections (joined by rcu-link) induces order like a generalized
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
146 let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked]
148 irreflexive rb as rcu
151 * The happens-before, propagation, and rcu constraints are all