From d5218ff91c3ef684cf00a5bda85b7d1af85fdb39 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 27 Apr 2011 08:50:34 +0200 Subject: [PATCH] Causality check for linear types --- compiler/heptagon/analysis/causal.ml | 54 ++++++++++++++++--------- compiler/heptagon/analysis/causality.ml | 11 +++-- 2 files changed, 42 insertions(+), 23 deletions(-) diff --git a/compiler/heptagon/analysis/causal.ml b/compiler/heptagon/analysis/causal.ml index 598cd9f..6fa1cd1 100644 --- a/compiler/heptagon/analysis/causal.ml +++ b/compiler/heptagon/analysis/causal.ml @@ -36,6 +36,7 @@ type sc = | Ctuple of sc list | Cwrite of ident | Cread of ident + | Clinread of ident | Clastread of ident | Cempty @@ -43,6 +44,7 @@ type sc = type ac = | Awrite of ident | Aread of ident + | Alinread of ident | Alastread of ident | Aseq of ac * ac | Aand of ac * ac @@ -71,6 +73,7 @@ let output_ac ff ac = fprintf ff "@[%a@]" (print_list_r (print 1) "(" "," ")") acs | Awrite(m) -> fprintf ff "%s" (name m) | Aread(m) -> fprintf ff "^%s" (name m) + | Alinread(m) -> fprintf ff "*%s" (name m) | Alastread(m) -> fprintf ff "last %s" (name m) in fprintf ff "@[%a@]@?" (print 0) ac @@ -131,6 +134,7 @@ and norm = function | Ctuple l -> ctuple (List.map norm l) | Cwrite(n) -> Aac(Awrite(n)) | Cread(n) -> Aac(Aread(n)) + | Clinread(n) -> Aac(Alinread(n)) | Clastread(n) -> Aac(Alastread(n)) | _ -> Aempty @@ -139,39 +143,48 @@ let build ac = (* associate a graph node for each name declaration *) let nametograph n g n_to_graph = Env.add n g n_to_graph in - let rec associate_node g n_to_graph = function + let rec associate_node g (n_to_graph, lin_map) = function | Awrite(n) -> - nametograph n g n_to_graph + nametograph n g n_to_graph, lin_map + | Alinread(n) -> + n_to_graph, nametograph n g lin_map | Atuple l -> - List.fold_left (associate_node g) n_to_graph l + List.fold_left (associate_node g) (n_to_graph, lin_map) l | _ -> - n_to_graph + n_to_graph, lin_map in (* first build the association [n -> node] *) (* for every defined variable *) - let rec initialize ac n_to_graph = + let rec initialize ac n_to_graph lin_map = match ac with | Aand(ac1, ac2) -> - let n_to_graph = initialize ac1 n_to_graph in - initialize ac2 n_to_graph + let n_to_graph, lin_map = initialize ac1 n_to_graph lin_map in + initialize ac2 n_to_graph lin_map | Aseq(ac1, ac2) -> - let n_to_graph = initialize ac1 n_to_graph in - initialize ac2 n_to_graph + let n_to_graph, lin_map = initialize ac1 n_to_graph lin_map in + initialize ac2 n_to_graph lin_map | _ -> let g = make ac in - associate_node g n_to_graph ac + associate_node g (n_to_graph, lin_map) ac in - let make_graph ac n_to_graph = + let make_graph ac n_to_graph lin_map = let attach node n = try let g = Env.find n n_to_graph in add_depends node g with | Not_found -> () in + let attach_lin node n = + try + let g = Env.find n lin_map in add_depends g node + with + | Not_found -> () in + let rec add_dependence g = function - | Aread(n) -> attach g n + | Aread(n) -> attach g n; attach_lin g n + | Alinread(n) -> let g = Env.find n lin_map in attach g n | _ -> () in @@ -187,12 +200,12 @@ let build ac = in match ac with | Awrite n -> Env.find n n_to_graph + | Alinread n -> Env.find n lin_map | Atuple l -> - begin try - node_for_tuple l - with Not_found - _ -> make ac - end + (try + node_for_tuple l + with Not_found + _ -> make ac) | _ -> make ac in @@ -211,7 +224,8 @@ let build ac = 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] + | 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 @@ -230,8 +244,8 @@ let build ac = let top_list, bot_list = make_graph ac in graph top_list bot_list in - let n_to_graph = initialize ac Env.empty in - let g = make_graph ac n_to_graph in + let n_to_graph, lin_map = initialize ac Env.empty Env.empty in + let g = make_graph ac n_to_graph lin_map in g (* the main entry. *) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 58ea744..fa94912 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -15,6 +15,7 @@ open Idents open Heptagon open Location open Sgraph +open Linearity open Causal let cempty = Cempty @@ -53,6 +54,7 @@ let rec cseqlist l = | c1 :: l -> cseq c1 (cseqlist l) let read x = Cread(x) +let linread x = Clinread(x) let lastread x = Clastread(x) let cwrite x = Cwrite(x) @@ -62,7 +64,7 @@ let rec pre = function | Cand(c1, c2) -> Cand(pre c1, pre c2) | Ctuple l -> Ctuple (List.map pre l) | Cseq(c1, c2) -> Cseq(pre c1, pre c2) - | Cread _ -> Cempty + | Cread _ | Clinread _ -> Cempty | (Cwrite _ | Clastread _ | Cempty) as c -> c (* projection and restriction *) @@ -82,7 +84,7 @@ let clear env c = let c2 = clearec c2 in cseq c1 c2 | Ctuple l -> Ctuple (List.map clearec l) - | Cwrite(id) | Cread(id) | Clastread(id) -> + | Cwrite(id) | Cread(id) | Clinread(id) | Clastread(id) -> if IdentSet.mem id env then Cempty else c | Cempty -> c in clearec c @@ -95,7 +97,10 @@ let build dec = let rec typing e = match e.e_desc with | Econst _ -> cempty - | Evar(x) -> read x + | Evar(x) -> + (match e.e_linearity with + | Lat _ -> linread x + | _ -> read x) | Elast(x) -> lastread x | Epre (_, e) -> pre (typing e) | Efby (e1, e2) ->