stdlib (*************************) (* Herd standard library *) (*************************) (* Empty set of events *) let emptyset = domain 0 (* Backward compatibility *) let partition = classes-loc let tag2instrs = tag2events (* Aliases *) let PoD = B let BR = PoD (* Basic relations *) let po-loc = po & loc let rfe = rf & ext let rfi = rf & int (* co0 *) let co0 = loc & ((IW * (W\IW)) | ((W\FW) * FW)) (* Id relation on set *) let toid(s) = [s] (* Turn a fence set into a fence relation *) let fencerel(B) = (po & (_ * B)) ; po (* Control+cfence *) let ctrlcfence(ctrl,CFENCE) = (ctrl & (_ * CFENCE)) ; po (* Make the difference between load-reserve/store conditional and amo insructions *) let lxsx = rmw \ amo (* Backward compatibility *) let inv-field = try inv-domain with 0 (* Some utilities (cpp11) *) let imply (A, B) = ~A | B (* nodetour eliminates the triangle: *) (* .--R2--> c --R3--. *) (* / v *) (* a --------R1-------> b *) let nodetour (R1, R2, R3) = R1 \ ( R2; R3 ) let singlestep (R) = nodetour(R, R, R) procedure subseteq(A, B) = empty (A \ B) end procedure inclusion(r1, r2) = empty r1 \ r2 end procedure total(r,E) = let rt = (r | r^-1) call inclusion((E*E),rt) end (*Union of domain and range*) let udr r = domain r | range r (***************) (* Set library *) (***************) (* Apply function f to each member of a set or relation *) let map f = let rec do_map S = match S with || {} -> {} || e ++ S -> f e ++ do_map S end in do_map let LKW = try LKW with emptyset