From 3dbf3c61f9c10ef40b508a83ae9bdf8617374d4a Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 25 Jul 2016 18:24:59 -0700 Subject: [PATCH 1/4] start dataflow analysis --- _oasis | 4 +- _tags | 13 ++++++- lib/Frenetic_Fdd.ml | 68 +++++++++++++++++---------------- lib/Frenetic_Fdd.mli | 3 ++ lib/Frenetic_NetKAT_Compiler.ml | 18 +++++++++ lib/META | 4 +- setup.ml | 9 +++-- 7 files changed, 79 insertions(+), 40 deletions(-) diff --git a/_oasis b/_oasis index fbb7e913d..09c747478 100644 --- a/_oasis +++ b/_oasis @@ -40,7 +40,9 @@ Library frenetic tcpip, ulex, yojson, - threads + threads, +# http://gallium.inria.fr/~fpottier/fix/ + fix Modules: Frenetic_Hashcons, Frenetic_Bits, diff --git a/_tags b/_tags index 296288fdb..79f355a54 100644 --- a/_tags +++ b/_tags @@ -1,5 +1,5 @@ # OASIS_START -# DO NOT EDIT (digest: 2f510444f9f8afdf56c9ef3cae00c123) +# DO NOT EDIT (digest: c6512c1020d86e25d9fca42583cfc498) # Ignore VCS directories, you can use the same kind of rule outside # OASIS_START/STOP if you want to exclude directories that contains # useless stuff for the build process @@ -22,6 +22,7 @@ true: annot, bin_annot : package(camlp4.lib) : package(core) : package(cstruct) +: package(fix) : package(ocamlgraph) : package(ppx_deriving.enum) : package(ppx_deriving.eq) @@ -43,6 +44,7 @@ true: annot, bin_annot : package(core) : package(cstruct) : package(cstruct.async) +: package(fix) : package(mparser) : package(mparser.re) : package(ocamlgraph) @@ -68,6 +70,7 @@ true: annot, bin_annot "frenetic/frenetic.native": package(core) "frenetic/frenetic.native": package(cstruct) "frenetic/frenetic.native": package(cstruct.async) +"frenetic/frenetic.native": package(fix) "frenetic/frenetic.native": package(mparser) "frenetic/frenetic.native": package(mparser.re) "frenetic/frenetic.native": package(ocamlgraph) @@ -94,6 +97,7 @@ true: annot, bin_annot "frenetic/openflow.native": package(core) "frenetic/openflow.native": package(cstruct) "frenetic/openflow.native": package(cstruct.async) +"frenetic/openflow.native": package(fix) "frenetic/openflow.native": package(mparser) "frenetic/openflow.native": package(mparser.re) "frenetic/openflow.native": package(ocamlgraph) @@ -119,6 +123,7 @@ true: annot, bin_annot : package(core) : package(cstruct) : package(cstruct.async) +: package(fix) : package(mparser) : package(mparser.re) : package(ocamlgraph) @@ -142,6 +147,7 @@ true: annot, bin_annot : package(camlp4.quotations.o) : package(core) : package(cstruct) +: package(fix) : package(ipaddr) : package(ocamlgraph) : package(ppx_deriving.enum) @@ -161,6 +167,7 @@ true: annot, bin_annot : package(camlp4.lib) : package(core) : package(cstruct) +: package(fix) : package(ocamlgraph) : package(ppx_deriving.enum) : package(ppx_deriving.eq) @@ -183,6 +190,7 @@ true: annot, bin_annot "lib_test/Test.byte": package(core) "lib_test/Test.byte": package(cstruct) "lib_test/Test.byte": package(cstruct.async) +"lib_test/Test.byte": package(fix) "lib_test/Test.byte": package(mparser) "lib_test/Test.byte": package(mparser.re) "lib_test/Test.byte": package(ocamlgraph) @@ -210,6 +218,7 @@ true: annot, bin_annot : package(core) : package(cstruct) : package(cstruct.async) +: package(fix) : package(mparser) : package(mparser.re) : package(ocamlgraph) @@ -234,6 +243,7 @@ true: annot, bin_annot : package(camlp4.lib) : package(core) : package(cstruct) +: package(fix) : package(ocamlgraph) : package(ppx_deriving.enum) : package(ppx_deriving.eq) @@ -250,6 +260,7 @@ true: annot, bin_annot : package(camlp4.lib) : package(core) : package(cstruct) +: package(fix) : package(ocamlgraph) : package(ppx_deriving.enum) : package(ppx_deriving.eq) diff --git a/lib/Frenetic_Fdd.ml b/lib/Frenetic_Fdd.ml index 03f1769a9..e8090d016 100644 --- a/lib/Frenetic_Fdd.ml +++ b/lib/Frenetic_Fdd.ml @@ -7,29 +7,33 @@ module Field = struct (** The order of the constructors defines the default variable ordering and has a massive performance impact. Do not change unless you know what you are doing. *) - type t - = Switch - | Location - | VSwitch - | VPort - | Vlan - | VlanPcp - (* SJS: for simplicity, support only up to 5 meta fields for now *) - | Meta0 - | Meta1 - | Meta2 - | Meta3 - | Meta4 - | EthType - | IPProto - | EthSrc - | EthDst - | IP4Src - | IP4Dst - | TCPSrcPort - | TCPDstPort - | VFabric - [@@deriving sexp, enumerate, enum] + module T = struct + type t + = Switch + | Location + | VSwitch + | VPort + | Vlan + | VlanPcp + (* SJS: for simplicity, support only up to 5 meta fields for now *) + | Meta0 + | Meta1 + | Meta2 + | Meta3 + | Meta4 + | EthType + | IPProto + | EthSrc + | EthDst + | IP4Src + | IP4Dst + | TCPSrcPort + | TCPDstPort + | VFabric + [@@deriving sexp, enumerate, enum, compare] + end + include Comparable.Make(T) + include T type field = t let num_fields = max + 1 @@ -43,7 +47,7 @@ module Field = struct sexp_of_t t |> Sexp.to_string let is_valid_order (lst : t list) : bool = - Set.Poly.(equal (of_list lst) (of_list all)) + Set.(equal (of_list lst) (of_list all)) let order = Array.init num_fields ~f:ident @@ -76,8 +80,8 @@ module Field = struct module Env : ENV = struct - type t = { - alist : (string * (field * (Frenetic_NetKAT.meta_init * bool))) list; + type t = { + alist : (string * (field * (Frenetic_NetKAT.meta_init * bool))) list; depth : int } @@ -159,12 +163,12 @@ module Field = struct | Mod _ -> k (1, lst) | Filter a -> k (1, (env, a) :: lst) | Seq (p, q) -> - f_seq' p lst env (fun (m, lst) -> + f_seq' p lst env (fun (m, lst) -> f_seq' q lst env (fun (n, lst) -> k (m * n, lst))) | Union _ -> k (f_union pol env, lst) - | Let (id, init, mut, p) -> - let env = Env.add env id init mut in + | Let (id, init, mut, p) -> + let env = Env.add env id init mut in f_seq' p lst env k | Star p -> k (f_union p env, lst) | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst) @@ -177,12 +181,12 @@ module Field = struct | Mod _ -> (1, lst) | Filter a -> (1, (env, a) :: lst) | Union (p, q) -> - f_union' p lst env (fun (m, lst) -> + f_union' p lst env (fun (m, lst) -> f_union' q lst env (fun (n, lst) -> k (m + n, lst))) | Seq _ -> k (f_seq pol env, lst) - | Let (id, init, mut, p) -> - let env = Env.add env id init mut in + | Let (id, init, mut, p) -> + let env = Env.add env id init mut in k (f_seq p env, lst) | Star p -> f_union' p lst env k | Link (sw,pt,_,_) -> k (1, (env, Test (Switch sw)) :: (env, Test (Location (Physical pt))) :: lst) diff --git a/lib/Frenetic_Fdd.mli b/lib/Frenetic_Fdd.mli index adf7abfd6..4e4473544 100644 --- a/lib/Frenetic_Fdd.mli +++ b/lib/Frenetic_Fdd.mli @@ -57,6 +57,9 @@ module Field : sig type field = t include Frenetic_Vlr.HashCmp with type t := t + module Set : Set.S with type Elt.t = t + module Map : Map.S with type Key.t = t + module Env : sig type t val empty : t diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml index 18f196a75..fe752b53a 100644 --- a/lib/Frenetic_NetKAT_Compiler.ml +++ b/lib/Frenetic_NetKAT_Compiler.ml @@ -801,6 +801,24 @@ module NetKAT_Automaton = struct let fdd = FDD.seq guard (FDD.union e d) in FDD.union acc fdd) + (* META fields *) + module Property : Fix.PROPERTY = struct + type property = Field.Set.t (* set of meta fields that a state depends on *) + let bottom = Field.(Set.of_list all) (* SJS *) + let equal = Field.Set.equal + let is_maximal = Field.Set.is_empty + end + + module Map : Fix.IMPERATIVE_MAPS = struct + include Int.Table + let create () = create () + let add key data tbl = set ~key ~data tbl + let find key tbl = find_exn tbl key + let iter f tbl = iteri ~f:(fun ~key ~data -> f key data) tbl + end + + module Analysis = Fix.Make(Map)(Property) + (* SJS: horrible hack *) let to_dot (automaton : t) = let states = Tbl.map automaton.states ~f:(fun (e,d) -> FDD.union e d) in diff --git a/lib/META b/lib/META index 51be07853..bf7a0230d 100644 --- a/lib/META +++ b/lib/META @@ -1,9 +1,9 @@ # OASIS_START -# DO NOT EDIT (digest: 2aed45dcfbabaef0cfd87efd10e22d19) +# DO NOT EDIT (digest: a56da596bf8054bafaefe81351a3001b) version = "4.0.0" description = "The Frenetic Compiler and Runtime System" requires = -"base64 camlp4.lib camlp4.extend camlp4 core cstruct ocamlgraph ppx_jane ppx_deriving.eq ppx_deriving.enum str tcpip ulex yojson threads" +"base64 camlp4.lib camlp4.extend camlp4 core cstruct ocamlgraph ppx_jane ppx_deriving.eq ppx_deriving.enum str tcpip ulex yojson threads fix" archive(byte) = "frenetic.cma" archive(byte, plugin) = "frenetic.cma" archive(native) = "frenetic.cmxa" diff --git a/setup.ml b/setup.ml index e747400c5..105da5762 100644 --- a/setup.ml +++ b/setup.ml @@ -1,7 +1,7 @@ (* setup.ml generated for the first time by OASIS v0.4.6 *) (* OASIS_START *) -(* DO NOT EDIT (digest: 2199ee8c8591b8a10a103774b1d0d7e9) *) +(* DO NOT EDIT (digest: a42271e2708c028450c74c6a073ce916) *) (* Regenerated by OASIS v0.4.6 Visit http://oasis.forge.ocamlcore.org for more information and @@ -7015,7 +7015,8 @@ let setup_t = FindlibPackage ("tcpip", None); FindlibPackage ("ulex", None); FindlibPackage ("yojson", None); - FindlibPackage ("threads", None) + FindlibPackage ("threads", None); + FindlibPackage ("fix", None) ]; bs_build_tools = [ExternalTool "ocamlbuild"; ExternalTool "ocamldoc"]; @@ -7413,7 +7414,7 @@ let setup_t = }; oasis_fn = Some "_oasis"; oasis_version = "0.4.6"; - oasis_digest = Some "\146\226'z\196]} ~\231\007\211\238;\193j"; + oasis_digest = Some "2R\202\192\136\139\209\245\r!\015\219\011c\135-"; oasis_exec = None; oasis_setup_args = []; setup_update = false @@ -7421,6 +7422,6 @@ let setup_t = let setup () = BaseSetup.setup setup_t;; -# 7425 "setup.ml" +# 7426 "setup.ml" (* OASIS_STOP *) let () = setup ();; From f9e2e3eb9edb9632568bda699e4ecfc5a6e9e80d Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 25 Jul 2016 21:35:58 -0700 Subject: [PATCH 2/4] data flow analysis: meta fields dependencies --- lib/Frenetic_NetKAT_Compiler.ml | 45 ++++++++++++++++++++++++++++++--- 1 file changed, 41 insertions(+), 4 deletions(-) diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml index fe752b53a..138f07427 100644 --- a/lib/Frenetic_NetKAT_Compiler.ml +++ b/lib/Frenetic_NetKAT_Compiler.ml @@ -802,23 +802,60 @@ module NetKAT_Automaton = struct FDD.union acc fdd) (* META fields *) - module Property : Fix.PROPERTY = struct + module Property (* : Fix.PROPERTY *) = struct type property = Field.Set.t (* set of meta fields that a state depends on *) - let bottom = Field.(Set.of_list all) (* SJS *) + let bottom = Field.(all |> List.filter ~f:is_meta |> Set.of_list) let equal = Field.Set.equal let is_maximal = Field.Set.is_empty end - module Map : Fix.IMPERATIVE_MAPS = struct + module Map (* : Fix.IMPERATIVE_MAPS *) = struct include Int.Table let create () = create () let add key data tbl = set ~key ~data tbl let find key tbl = find_exn tbl key - let iter f tbl = iteri ~f:(fun ~key ~data -> f key data) tbl + let iter f tbl = iteri tbl ~f:(fun ~key ~data -> f key data) end module Analysis = Fix.Make(Map)(Property) + let gen fdd = + FDD.fold + (fun _ -> Field.Set.empty) + (fun (f,_) x y -> + let s = Set.union x y in + if Field.is_meta f then Set.add s f else s) + fdd + + let eq (automaton : t) : Analysis.equations = fun (state : int) -> + let (e,d) = Tbl.find_exn automaton.states state in + let gen = Set.union (gen e) (gen d) in + let conts = + let open Action in + FDD.fold + (fun par -> Par.fold par ~init:Int.Map.empty ~f:(fun acc seq -> + let key = Value.to_int_exn (Seq.find_exn seq K) in + let data = List.filter_map (Seq.keys seq) ~f:(function + | K -> None + | F f -> if Field.is_meta f then Some f else None) + |> Field.Set.of_list + in + Int.Map.add ~key ~data acc)) + (fun _ -> Int.Map.merge ~f:(fun ~key v -> Some (match v with + | `Left v | `Right v -> v + | `Both (v1,v2) -> Set.inter v1 v2))) + d + |> Int.Map.to_alist + in + fun deps -> + (* kill-gen analysis: gen ∪ (⋃ᵢ inᵢ - killᵢ) *) + List.map conts ~f:(fun (k,kill) -> Field.Set.diff (deps k) kill) + |> List.cons gen + |> Field.Set.union_list + + let meta_deps (automaton : t) = Analysis.lfp (eq automaton) + + (* SJS: horrible hack *) let to_dot (automaton : t) = let states = Tbl.map automaton.states ~f:(fun (e,d) -> FDD.union e d) in From ec51d560cc8ab3d7e57cdf681014b5082d7fe379 Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 25 Jul 2016 23:07:26 -0700 Subject: [PATCH 3/4] take a crack at global meta field erasure --- lib/Frenetic_NetKAT_Compiler.ml | 48 ++++++++++++++++++++++++++++++++- 1 file changed, 47 insertions(+), 1 deletion(-) diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml index 138f07427..6ddcd69a0 100644 --- a/lib/Frenetic_NetKAT_Compiler.ml +++ b/lib/Frenetic_NetKAT_Compiler.ml @@ -853,7 +853,52 @@ module NetKAT_Automaton = struct |> List.cons gen |> Field.Set.union_list - let meta_deps (automaton : t) = Analysis.lfp (eq automaton) + module Cache = Hashable.Make(struct + type env = Value.t Field.Map.t [@@deriving sexp, compare] + type t = int * env [@@deriving sexp, compare] + let hash (state, env) = + (state, Field.Map.to_alist env) |> Hashtbl.hash + end) + + let erase_meta_fields (automaton : t) : t = + let meta_deps = Analysis.lfp (eq automaton) in + let cache = Cache.Table.create () in + let new_auto = create_t () in + + let rec go (state : int) (meta_env : Value.t Field.Map.t) = + let deps = meta_deps state in + let meta_env = Field.Map.filter meta_env ~f:(fun ~key ~data -> Set.mem deps key) in + match Cache.Table.find cache (state, meta_env) with + | Some s -> s + | None -> + let s = mk_state_t new_auto in + Cache.Table.add_exn cache ~key:(state, meta_env) ~data:s; + add_to_t_with_id new_auto (go' (Tbl.find_exn automaton.states state) meta_env) s; + s + and go' (e,d) (meta_env : Value.t Field.Map.t) = + let e = FDD.restrict (Field.Map.to_alist meta_env) e in + let d = + Field.Map.to_alist meta_env + |> List.map ~f:(fun (f,v) -> (Action.F f, v)) + |> Seq.of_alist_exn + |> Par.singleton + |> (fun a -> FDD.seq (FDD.const a) d) + |> FDD.map_r (fun par -> Par.fold par ~init:Par.empty ~f:(fun par seq -> + let env = + Seq.to_hvs seq + |> List.filter ~f:(fun (f,v) -> Field.is_meta f) + |> Field.Map.of_alist_exn + in + let seq = Seq.update seq Action.K ~f:(function + | None -> assert false + | Some k -> Value.of_int (go (Value.to_int_exn k) env)) + in + Par.add par seq)) + in + (e,d) + in + new_auto.source <- go automaton.source Field.Map.empty; + new_auto (* SJS: horrible hack *) @@ -920,6 +965,7 @@ end let compile_global ?(options=default_compiler_options) (pol : Frenetic_NetKAT.policy) : FDD.t = prepare_compilation ~options pol; NetKAT_Automaton.of_policy pol + |> NetKAT_Automaton.erase_meta_fields |> NetKAT_Automaton.to_local ~pc:Field.Vlan From 4613f2b6d743e616f67f479aaccc03bb73fff374 Mon Sep 17 00:00:00 2001 From: Steffen Smolka Date: Mon, 25 Jul 2016 23:21:32 -0700 Subject: [PATCH 4/4] first global example --- examples/meta-fields/global/meta-global1.kat | 2 ++ lib/Frenetic_NetKAT_Compiler.ml | 3 +++ 2 files changed, 5 insertions(+) create mode 100644 examples/meta-fields/global/meta-global1.kat diff --git a/examples/meta-fields/global/meta-global1.kat b/examples/meta-fields/global/meta-global1.kat new file mode 100644 index 000000000..60746c04b --- /dev/null +++ b/examples/meta-fields/global/meta-global1.kat @@ -0,0 +1,2 @@ +let meta := 1 in +if meta = 1 then 1@1=>2@2 else 1@1=>3@3 diff --git a/lib/Frenetic_NetKAT_Compiler.ml b/lib/Frenetic_NetKAT_Compiler.ml index 6ddcd69a0..fbce67061 100644 --- a/lib/Frenetic_NetKAT_Compiler.ml +++ b/lib/Frenetic_NetKAT_Compiler.ml @@ -535,6 +535,9 @@ module Pol = struct |> mk_filter in mk_big_seq [filter_loc s1 p1; Dup; post_link ] + | Let (metaid, Const v, _, p) -> + Seq (Mod (Meta (metaid, v)), of_pol ing p) + | Let _ -> failwith "not implemented" | VLink _ -> assert false (* SJS / JNF *) end