Lines Matching refs:UL
20 * UL Unlock: a spin_unlock() event
28 * LKW and UL are write events; UL has Release ordering.
40 let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
55 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
61 empty ([LKW] ; po-loc ; [RU]) \ (po-loc ; [UL] ; po-loc) as nested-is-locked
67 * Put lock operations in their appropriate classes, but leave UL out of W
73 let Release = Release | UL
76 (* Match LKW events to their corresponding UL events *)
77 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
79 flag ~empty UL \ range(critical) as unmatched-unlock
86 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
114 * A given RU event e may read internally from the last po-previous UL,
115 * or it may read from a UL event in another thread or the initial write.
118 let possible-rf-ru e = (((UL * {e}) & po-loc) \
119 ([UL] ; po-loc ; [UL] ; po-loc)) |
120 (((UL | IW) * {e}) & loc & ext)
136 (* Generate all co relations, including LKW events but not UL *)
140 let W = W | UL
143 (* Merge UL events into co *)
149 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)