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
55 empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
61  * Put lock operations in their appropriate classes, but leave UL out of W
67 let Release = Release | UL
70 (* Match LKW events to their corresponding UL events *)
71 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
73 flag ~empty UL \ range(critical) as unmatched-unlock
80 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
105 (* rfi for RU events: an RU may read from the last po-previous UL *)
106 let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
108 (* rfe for RU events: an RU may read from an external UL or the initial write *)
112 		in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
122 (* Generate all co relations, including LKW events but not UL *)
126 let W = W | UL
129 (* Merge UL events into co *)
135 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)