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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
include "ncos.cat"
(* Utilities *)
let roots(r) = domain(r) \ range(r)
let succs (e,r) = range ([e];r)
let mapset2rel f =
let rec map_rec xs = match xs with
|| {} -> 0
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
let mapset2set f =
let rec map_rec xs = match xs with
|| {} -> {}
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
(* Basic definitions *)
let poDorW = [PoD|W];po;[PoD|W]
let nextDorW = poDorW \ (poDorW;poDorW)
let DpoDorW = [PoD];poDorW
(* Add pair dw for w in ws
More precisely:
addD d (ws,dw) = dw U {(d,w) | w in ws}
*)
let addD d =
let rec do_rec ws = match ws with
|| {} -> fun k -> k
|| w ++ ws ->
let kws = do_rec ws in
fun k -> (d,w) ++ kws k
end in do_rec
(*
Set combination: union of equiv-related sets
*)
let addifequiv (equiv,ws0) = mapset2set (fun w -> succs (w,equiv) & ws0)
let combine (equiv,ws1,ws2) =
addifequiv (equiv,ws1) ws2 | addifequiv (equiv,ws2) ws1
(* Tree scan: returns ws,dw, where ws is the set of writes always performed at
this level and dw is the relation from PoD to writes always performed *)
let rec case_disjunction (equiv,e) = match { e } & PoD with
|| {} -> (* e is not a PoD, hence is a write *)
let (ws,dw) = write_acc (equiv, (succs (e,nextDorW))) in
(e ++ ws,dw)
|| d ++ es -> (* e is a PoD *)
let (ws,dw) = keep_equiv_writes (equiv, (succs (d,nextDorW))) in
(ws,addD d ws dw)
end
and write_acc (equiv,es) = match es with
|| {} -> ({},0)
|| e ++ es ->
let (ws_e,dw_e) = case_disjunction (equiv, e)
and (ws_es,dw_es) = write_acc (equiv, es) in
(ws_e|ws_es, dw_e|dw_es)
end
(* Warning, base case is on singleton *)
and keep_equiv_writes (equiv,es) = match es with
|| {} -> ({},0) (* No successors, ie no W po-after, special case *)
|| e ++ es ->
match es with
|| {} -> case_disjunction(equiv,e) (* Singleton = base case *)
|| f ++ fs ->
let (ws_e,dw_e) = case_disjunction(equiv,e)
and (ws_es,dw_es) = keep_equiv_writes(equiv,es) in
(combine (equiv,ws_e,ws_es), dw_e|dw_es)
end
end
(* Final call *)
let zyva equiv =
mapset2rel
(fun r -> let (ws,dw) = case_disjunction(equiv,r) in dw)
let intrinsic = (iico_data | iico_ctrl)+
let udr r = domain r | range r
let generated-by-stxr = udr(same-instr;[range(rmw)])
let rf-reg-restrict =
let NW = ~generated-by-stxr in
[NW];rf-reg
let dd = (rf-reg | intrinsic)+
#let dd-restrict = (rf-reg-restrict | intrinsic)+
let to-PoD = [R]; dd; [PoD]
let pre-ctrl = to-PoD; po; [W]
let Dmins = roots(DpoDorW)
let Dm=Dmins*Dmins
let always-exec equiv =
let DW = zyva equiv Dmins in
to-PoD; DW
let ctrlequiv equiv = pre-ctrl \ (always-exec equiv)
|
