1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
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
|
