Portless NetKAT

_oasis

@@ -31,11 +31,15 @@ PreBuildCommand:
   cppo -n \
     ppx/PPX_NetKAT_Parser.cppo.mly \
     -o ppx/PPX_NetKAT_Parser.mly
+  cppo -n \
+    lib/Frenetic_NetKAT_Portless_Generated_Parser.cppo.mly \
+    -o lib/Frenetic_NetKAT_Portless_Generated_Parser.mly
   menhir --only-tokens ppx/PPX_NetKAT_Parser.mly \
     --base lib/Frenetic_NetKAT_Tokens
 PostBuildCommand:
   rm -f ppx/PPX_NetKAT_Parser.mly
   rm -f lib/Frenetic_NetKAT_Generated_Parser.mly
+  rm -f lib/Frenetic_NetKAT_Portless_Generated_Parser.mly
   # do not delete so ocamldoc is happy!
   # rm -f lib/Frenetic_NetKAT_Tokens*
 ImplementationPatterns:
@@ -62,11 +66,14 @@ Library frenetic
   InternalModules:
     LexBuffer,
     Frenetic_NetKAT_Lexer,
-    Frenetic_NetKAT_Generated_Parser
+    Frenetic_NetKAT_Generated_Parser,
+    Frenetic_NetKAT_Portless_Lexer,
+    Frenetic_NetKAT_Portless_Generated_Parser
   Modules:
     Frenetic_Hashcons,
     Frenetic_Bits,
     Frenetic_Fdd,
+    Frenetic_Portless_Fdd,
     Frenetic_OpenFlow0x04,
     Frenetic_GroupTable0x04,
     Frenetic_NetKAT,
@@ -80,6 +87,10 @@ Library frenetic
     Frenetic_NetKAT_Net,
     Frenetic_NetKAT_Pretty,
     Frenetic_NetKAT_Semantics,
+    Frenetic_NetKAT_Portless,
+    Frenetic_NetKAT_Portless_Compiler,
+    Frenetic_NetKAT_Portless_Optimize,
+    Frenetic_NetKAT_Portless_Parser,
     Frenetic_Network,
     Frenetic_OpenFlow,
     Frenetic_OpenFlow_Header,

frenetic/Topologies.ml

@@ -0,0 +1,70 @@
+open Core.Std
+open Frenetic_NetKAT_Portless
+
+let (--) i j =
+    let rec aux n acc =
+      if n < i then acc else aux (n-1) (n :: acc)
+    in aux j []
+
+let geo_sum a r n = a * ((1-(Int.pow r n))/(1-r))
+
+let i64 = Int64.of_int_exn
+
+let single host_count =
+  let children = 1 -- host_count in
+  let topo_down, _ = List.fold children ~init:([], 1)
+      ~f:(fun (acc, port) to_host ->
+          ((Switch(1L, i64 port), Host(i64 to_host)) :: acc), port + 1) in
+
+  let topo_up = List.map topo_down (fun (x, y) -> y, x) in
+  topo_up @ topo_down
+
+let minimal = single 2
+
+let linear switch_count =
+  let hosts = List.map (1 -- switch_count) (fun x -> (Switch(i64 x, i64 1), Host(i64 x))) in
+  let switches =
+    if switch_count > 1 then
+      (Switch(2L, 2L), Switch(1L, 2L)) :: List.map (2 -- (switch_count - 1)) (fun x -> (Switch(i64 (x + 1), i64 2), Switch(i64 x, i64 3)))
+    else
+      [] in
+
+  let topo_down = hosts @ switches in
+  let topo_up = List.map topo_down (fun (x, y) -> y, x) in
+  topo_up @ topo_down
+
+let tree depth fanout =
+  let rec add_hosts switch fanout position =
+    let children = (((position - 1) * fanout) + 1) -- (position * fanout) in
+    let switches, top_port = List.fold children ~init:([], 1)
+        ~f:(fun (acc, port) to_host ->
+            ((Switch(i64 switch, i64 port), Host(i64 to_host)) :: acc), port + 1)
+    in switches in
+
+  let rec add_switches switch fanout =
+    let children = (((switch - 1) * fanout) + 2) -- ((switch * fanout) + 1) in
+    let switches, top_port = List.fold children ~init:([], 1)
+        ~f:(fun (acc, port) to_sw ->
+            ((Switch(i64 switch, i64 port), Switch(i64 to_sw, i64 (fanout + 1))) :: acc), port + 1)
+    in switches in
+
+  let switch_numbers    = 1 -- (geo_sum 1 fanout (depth - 1)) in
+  let switch_with_hosts = List.zip_exn
+      (((geo_sum 1 fanout (depth - 1)) + 1) -- (geo_sum 1 fanout depth))
+      (1 -- (Int.pow fanout (depth - 1))) in
+  let sw_links = List.fold switch_numbers ~init:[] ~f:(fun acc sw -> add_switches sw fanout @ acc) in
+  let topo_down = List.fold switch_with_hosts ~init:sw_links ~f:(fun acc (sw, pos) -> add_hosts sw fanout pos @ acc) in
+  let topo_up = List.map topo_down (fun (x, y) -> y, x) in
+  topo_up @ topo_down
+
+type topo_name =
+  | Tree of int * int
+  | Linear of int
+  | Single of int
+  | Minimal
+
+let topo_from_name name = match name with
+  | Tree (x, y) -> tree x y
+  | Linear x -> linear x
+  | Single x -> single x
+  | Minimal -> minimal

frenetic/frenetic.ml

@@ -42,6 +42,26 @@ let table_fields : Frenetic_NetKAT_Compiler.flow_layout Command.Spec.Arg_type.t
       List.map ~f:table_to_fields field_list_list
     )
 
+let topology_name : Topologies.topo_name Command.Spec.Arg_type.t =
+  let open Topologies in
+  let num_arg = ",\\([1-9][0-9]*\\)" in
+  let tree = Str.regexp ("tree" ^ num_arg ^ num_arg ^ "$") in
+  let linear = Str.regexp ("linear" ^ num_arg ^ "$") in
+  let single = Str.regexp ("single" ^ num_arg ^ "$") in
+  let minimal = Str.regexp "minimal$" in
+  Command.Spec.Arg_type.create
+    (function x ->
+      if Str.string_match tree x 0 then
+        Tree (Int.of_string (Str.matched_group 1 x), Int.of_string (Str.matched_group 2 x))
+      else if Str.string_match linear x 0 then
+        Linear (Int.of_string (Str.matched_group 1 x))
+      else if Str.string_match single x 0 then
+        Single (Int.of_string (Str.matched_group 1 x))
+      else if Str.string_match minimal x 0 then
+        Minimal
+      else
+        (eprintf "'%s' is not a legal topology name.  Choose 'tree,n,o', 'linear,n', 'single,n', 'minimal' \n" x;
+        exit 1))
 
 (*===========================================================================*)
 (* FLAGS                                                                     *)
@@ -77,6 +97,11 @@ module Flag = struct
   let topology_file =
     flag "--topology-file" (optional_with_default "topology.dot" file)
       ~doc:"File containing .dot topology of network. Defaults to \"topology.kat\"."
+
+  let topology_name =
+    flag "--topo" (required topology_name)
+      ~doc:"topology_name The name of the topology. Same as mn --topo value."
+
 end
 
 
@@ -145,6 +170,26 @@ let openflow13_fault_tolerant_controller : Command.t =
       run (Frenetic_OpenFlow0x04_Plugin.fault_tolerant_main
         openflow_port policy_file topology_file))
 
+let start_controller : Command.t =
+  Command.basic
+    ~summary:"Starts a controller with specified topology and installed rules generated from portless policy."
+    Command.Spec.(empty
+                  +> Flag.openflow_port
+                  +> Flag.topology_name
+                  +> Flag.policy_file
+                  ++ default_spec)
+    (fun openflow_port topology_name policy_file ->
+       run (
+         let pol = Frenetic_NetKAT_Portless_Parser.pol_of_file policy_file in
+         let topo = Topologies.topo_from_name topology_name in
+
+         let module Controller = Frenetic_NetKAT_Controller.Make (Frenetic_OpenFlow0x01_Plugin) in
+         Controller.start openflow_port;
+         Async.Std.Deferred.don't_wait_for (Controller.update (Frenetic_NetKAT_Portless_Compiler.compile pol topo));
+         never_returns (Async.Std.Scheduler.go ());
+       )
+    )
+
 let main : Command.t =
   Command.group
     ~summary:"Invokes the specified Frenetic module."
@@ -153,7 +198,8 @@ let main : Command.t =
     ; ("http-controller", http_controller)
     ; ("openflow13", openflow13_controller)
     ; ("fault-tolerant", openflow13_fault_tolerant_controller)
-    ; ("dump", Dump.main)]
+    ; ("dump", Dump.main)
+    ; ("start-controller", start_controller)]
 
 let () =
   Frenetic_Util.pp_exceptions ();

lib/Frenetic_NetKAT_Portless.ml

@@ -0,0 +1,54 @@
+open Core.Std
+
+type header =
+  | EthSrc
+  | EthDst
+  | Vlan
+  | VlanPcp
+  | EthType
+  | IPProto
+  | IP4Src
+  | IP4Dst
+  | TCPSrcPort
+  | TCPDstPort
+  | From
+  | AbstractLoc
+[@@deriving sexp, compare]
+
+type pred =
+  | True
+  | False
+  | Test of header * int64 * int
+  | And of pred * pred
+  | Or of pred * pred
+  | Neg of pred
+[@@deriving sexp]
+
+type policy =
+  | Filter of pred
+  | Mod of header * int64 * int
+  | Union of policy * policy
+  | Seq of policy * policy
+  | Star of policy
+[@@deriving sexp]
+
+type link =
+  | Host of int64
+  | Switch of int64 * int64
+[@@deriving sexp]
+
+type topo = (link * link) list [@@deriving sexp]
+
+let is_loc_host id = Int64.equal (Int64.bit_and id 1L) 1L
+let is_loc_switch id = Int64.equal (Int64.bit_and id 1L) 0L
+
+let host_to_abs_loc id = Int64.(+) (Int64.shift_left id 1) 1L
+let switch_to_abs_loc id = Int64.shift_left id 1
+
+let link_to_abs_loc link = match link with
+  | Host id -> host_to_abs_loc id
+  | Switch (id, pt) -> switch_to_abs_loc id
+
+let default_mask = 64
+let id           = Filter True
+let drop         = Filter False

lib/Frenetic_NetKAT_Portless.mli

@@ -0,0 +1,52 @@
+open Core.Std
+
+type header =
+  | EthSrc
+  | EthDst
+  | Vlan
+  | VlanPcp
+  | EthType
+  | IPProto
+  | IP4Src
+  | IP4Dst
+  | TCPSrcPort
+  | TCPDstPort
+  | From
+  | AbstractLoc
+[@@deriving sexp, compare]
+
+type pred =
+  | True
+  | False
+  | Test of header * int64 * int
+  | And of pred * pred
+  | Or of pred * pred
+  | Neg of pred
+[@@deriving sexp]
+
+type policy =
+  | Filter of pred
+  | Mod of header * int64 * int
+  | Union of policy * policy
+  | Seq of policy * policy
+  | Star of policy
+[@@deriving sexp]
+
+type link =
+  | Host of int64
+  | Switch of int64 * int64
+[@@deriving sexp]
+
+val default_mask: int
+val id: policy
+val drop: policy
+
+type topo = (link * link) list [@@deriving sexp]
+
+val host_to_abs_loc: int64 -> int64
+val switch_to_abs_loc: int64 -> int64
+
+val is_loc_host: int64 -> bool
+val is_loc_switch: int64 -> bool
+
+val link_to_abs_loc: link -> int64