tools/memory-model/lock.cat

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
64 let R = R | LKR | LF | RU
65 let W = W | LKW
67 let Release = Release | UL
68 let Acquire = Acquire | LKR
71 let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
76 let UNMATCHED-LKW = LKW \ domain(critical)
80 let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
83 let all-possible-rfe-lf =
89 	let possible-rfe-lf r =
90 		let pair-to-relation p = p ++ 0
97 let rf-lf = rfe-lf | rfi-lf
106 let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
109 let all-possible-rfe-ru =
110 	let possible-rfe-ru r =
111 		let pair-to-relation p = p ++ 0
117 let rf-ru = rfe-ru | rfi-ru
120 let rf = rf | rf-lf | rf-ru
123 let co0 = co0 | ([IW] ; loc ; [LKW]) |
126 let W = W | UL
127 let M = R | W
130 let co = (co | critical | (critical^-1 ; co))+
131 let coe = co & ext
132 let coi = co & int
135 let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
136 let rfe = rf & ext
137 let rfi = rf & int
139 let fr = rf^-1 ; co
140 let fre = fr & ext
141 let fri = fr & int