Fix for causality
Tuples should behave like ands for nodes that are not reads or writes of a single variable
This commit is contained in:
parent
04fcf5a826
commit
9105b54c1f
1 changed files with 27 additions and 16 deletions
|
@ -117,13 +117,13 @@ let rec cand nc1 nc2 =
|
|||
| nc1, Aor(nc2, nc22) -> Aor(cand nc1 nc2, cand nc1 nc22)
|
||||
| Aac(ac1), Aac(ac2) -> Aac(Aand(ac1, ac2))
|
||||
|
||||
let rec ctuple l =
|
||||
let conv = function
|
||||
let rec ctuple l =
|
||||
let rec conv = function
|
||||
| Cwrite(n) -> Awrite(n)
|
||||
| Cread(n) -> Aread(n)
|
||||
| Clastread(n) -> Alastread(n)
|
||||
| Ctuple(l) -> Atuple (ctuple l)
|
||||
| Cand _ -> Format.printf "Unexpected and\n"; assert false
|
||||
| Cand (c1, c2) -> Aand (conv c1, conv c2)
|
||||
| Cseq _ -> Format.printf "Unexpected seq\n"; assert false
|
||||
| Cor _ -> Format.printf "Unexpected or\n"; assert false
|
||||
| _ -> assert false
|
||||
|
@ -133,7 +133,7 @@ let rec ctuple l =
|
|||
| Cempty::l -> ctuple l
|
||||
| v::l -> (conv v)::(ctuple l)
|
||||
|
||||
let rec norm = function
|
||||
and norm = function
|
||||
| Cor(c1, c2) -> cor (norm c1) (norm c2)
|
||||
| Cand(c1, c2) -> cand (norm c1) (norm c2)
|
||||
| Cseq(c1, c2) -> cseq (norm c1) (norm c2)
|
||||
|
@ -214,18 +214,29 @@ let build ac =
|
|||
| Aseq(ac1, ac2) ->
|
||||
let top1, bot1 = make_graph ac1 in
|
||||
let top2, bot2 = make_graph ac2 in
|
||||
(* add extra dependences *)
|
||||
List.iter
|
||||
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
|
||||
top2;
|
||||
top1 @ top2, bot1 @ bot2
|
||||
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
||||
| Aread(n) -> let g = make ac in attach g n; [g], [g]
|
||||
| Atuple(l) ->
|
||||
let g = node_for_ac ac in
|
||||
List.iter (add_dependence g) l;
|
||||
[g], [g]
|
||||
| _ -> [], [] in
|
||||
(* add extra dependences *)
|
||||
List.iter
|
||||
(fun top -> List.iter (fun bot -> add_depends top bot) bot1)
|
||||
top2;
|
||||
top1 @ top2, bot1 @ bot2
|
||||
| Awrite(n) -> let g = Env.find n n_to_graph in [g], [g]
|
||||
| Aread(n) -> let g = make ac in attach g n; attach_lin g n; [g], [g]
|
||||
| Alinread(n) -> let g = Env.find n lin_map in attach g n; [g], [g]
|
||||
| Atuple(l) ->
|
||||
let make_graph_tuple ac =
|
||||
match ac with
|
||||
| Aand _ | Atuple _ -> make_graph ac
|
||||
| _ -> [], []
|
||||
in
|
||||
let g = node_for_ac ac in
|
||||
List.iter (add_dependence g) l;
|
||||
let top_l, bot_l = List.split (List.map make_graph_tuple l) in
|
||||
let top_l = List.flatten top_l in
|
||||
let bot_l = List.flatten bot_l in
|
||||
g::top_l, g::bot_l
|
||||
| _ -> [], []
|
||||
|
||||
in
|
||||
let top_list, bot_list = make_graph ac in
|
||||
graph top_list bot_list in
|
||||
|
||||
|
|
Loading…
Reference in a new issue