Lines Matching full:let

33 let RL = try RL with emptyset
34 let RU = try RU with emptyset
37 let LF = LF | RL
40 let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
44 let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
45 let rmw = rmw | lk-rmw
70 let R = R | LKR | LF | RU
71 let W = W | LKW
73 let Release = Release | UL
74 let Acquire = Acquire | LKR
77 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
82 let UNMATCHED-LKW = LKW \ domain(critical)
86 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
89 let pair-to-relation p = p ++ 0
96 let possible-rfe-noncrit-lf e = (LKW * {e}) & loc & ext
99 let all-possible-rfe-lf =
104 	let set-of-singleton-rfe-lf e =
111 let rf-lf = rfe-lf | rfi-lf
118 let possible-rf-ru e = (((UL * {e}) & po-loc) \
123 let all-possible-rf-ru =
125 	let set-of-singleton-rf-ru e =
134 let rf = rf | rf-lf | rf-ru
137 let co0 = co0 | ([IW] ; loc ; [LKW]) |
140 let W = W | UL
141 let M = R | W
144 let co = (co | critical | (critical^-1 ; co))+
145 let coe = co & ext
146 let coi = co & int
149 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
150 let rfe = rf & ext
151 let rfi = rf & int
153 let fr = rf^-1 ; co
154 let fre = fr & ext
155 let fri = fr & int