Lines Matching refs:UL
23 * UL Unlock: a spin_unlock() event
31 * LKW and UL are write events; UL has Release ordering.
43 let ALL-LOCKS = LKR | LKW | UL | LF | RU
58 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
64 * Put lock operations in their appropriate classes, but leave UL out of W
70 let Release = Release | UL
73 (* Match LKW events to their corresponding UL events *)
74 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
76 flag ~empty UL \ range(critical) as unmatched-unlock
83 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
108 (* rfi for RU events: an RU may read from the last po-previous UL *)
109 let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
111 (* rfe for RU events: an RU may read from an external UL or the initial write *)
115 in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
125 (* Generate all co relations, including LKW events but not UL *)
129 let W = W | UL
132 (* Merge UL events into co *)
138 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)