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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2011-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(* Edge variations on plain/atomic/reserve *)
module type S = sig
type edge
val varatom_one : edge list -> edge list list
val varatom_es : edge list list -> edge list list
end
module type Fold = sig
type atom
val fold : (atom option -> 'a -> 'a) -> 'a -> 'a
end
module Make(E:Edge.S) (F:Fold with type atom = E.atom) : S
with type edge = E.edge = struct
type edge = E.edge
open E
(* Notice, var_src si applied second, hence RMW check *)
let can_set_src e a = match e.E.edge with
| E.Rmw _ -> E.compare_atomo e.E.a2 a = 0
| _ -> true
let var_src e es = match e.E.a1 with
| None ->
F.fold
(fun ao k ->
if can_set_src e ao then
({ e with a1=ao }::es)::k
else k)
[]
| Some _ -> [e::es]
let var_tgt e es = match e.E.a2 with
| None ->
F.fold
(fun ao k -> ({ e with a2=ao }::es)::k)
[]
| Some _ -> [e::es]
let var_edge e1 e2 es = match e1.E.a2,e2.E.a1 with
| None,None ->
F.fold
(fun ao k ->
if can_set_src e2 ao then
({ e1 with a2 = ao}::{ e2 with a1 = ao}::es)::k
else k)
[]
| _,_ -> [e1::e2::es]
(*
let var_both e = match e.E.edge with
| E.Rmw -> begin match e.E.a1,e.E.a2 with
| None,None -> (* RMW have identical atomic specs for source and targets *)
F.fold
(fun ao k -> { e with a1=ao; a2=ao; }::k)
[]
| _,_ -> [e]
end
| _ -> begin match e.E.a1,e.E.a2 with
| None,None ->
F.fold
(fun ao1 k ->
F.fold
(fun ao2 k -> { e with a1=ao1; a2=ao2; }::k)
k)
[]
| None,Some _ ->
F.fold
(fun ao1 k -> { e with a1=ao1;}::k)
[]
| Some _,None ->
F.fold
(fun ao2 k -> { e with a2=ao2;}::k)
[]
| Some _,Some _ -> [e]
end
*)
(* Variation of composite relaxation candidate *)
let as_cons = function
| e::es -> e,es
| [] -> assert false
let rec varatom_inside = function
| [] -> assert false
| [e] -> var_tgt e []
| e1::(_::_ as ess) ->
let ess = varatom_inside ess in
List.fold_right
(fun es k ->
let e2,rem = as_cons es in
var_edge e1 e2 rem@k)
ess []
let varatom_ones es k = match es with
| [] -> k
| _ ->
let ess = varatom_inside es in
List.fold_right
(fun es k ->
let e,es = as_cons es in
var_src e es@k)
ess k
let varatom_one es = varatom_ones es []
let varatom_es es = List.fold_right varatom_ones es []
end
|
