NetKAT Decision Procedure Based on Symbolic Automata (FDDs)

_oasis

@@ -80,6 +80,7 @@ Library frenetic
     Frenetic_NetKAT_Optimize,
     Frenetic_NetKAT_Json,
     Frenetic_NetKAT_Compiler,
+    Frenetic_NetKAT_Equivalence,
     Frenetic_NetKAT_FabricGen,
     Frenetic_NetKAT_Virtual_Compiler,
     Frenetic_NetKAT_Net,

examples/decision-procedure/README.md

@@ -0,0 +1,17 @@
+# Decision Procedure
+This directory contains (pairs of) NetKAT programs that can be checked for equivalence.
+
+## Requirements
+The frenetic executable must be installed:
+  * run `make && make reinstall` in the frenetic root directory
+
+## Run
+To decide program equivalence, run
+```bash
+frenetic dump decision <file1> <file2>
+```
+
+## Options
+Run `frenetic dump help decision` to see a list of all options. Currently, one flag is supported:
+  * --dump-auto: dump automata representations of the programs
+

examples/decision-procedure/drop.kat

@@ -0,0 +1 @@
+drop

examples/decision-procedure/equalities.txt

@@ -0,0 +1,86 @@
+(* RANDOM CRAP. *)
+(* ASSAGE. *)
+(port:=3; filter port=3) == (port:=3);;
+(filter port=3; filter switch=4) == (filter switch=4; filter port=3);;
+(port:=3; switch:=4) == (switch:=4; port:=3);;
+(port:=1; filter switch=2) == (filter switch=2; port:=1);;
+(dup; filter port=3) == (filter port=3; dup);;
+(filter port=3; port:=3) == (filter port=3);;
+(port:=3; port:=4 ) == (port:=4);;
+(filter port=3; filter port=4) == drop;;
+(filter port=3 + filter port != 3) == id;;
+(* FALSE!! *) (* (filter port != 3) <= filter port != 4;; *)
+(port:=3; port :=4; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=6; port:=5) == port:=5;;
+(port:=3; port :=4; port:=2; port:=1; port:=0; port:=6; port:=7; port:=5) == port:=5;;
+(port:=3; switch :=4; port:=2; switch:=1; port:=0; switch:=6; port:=7; port:=5) == port:=5; switch:=6;;
+(switch:=1; port:=0; switch:=6; port:=5) == port:=5; switch:=6;;
+port:=0; switch:=6; port:=5 == port:=5; switch:=6;;
+(* FALSE!! *) (* vlanId:=3; switch:=6; port:=5 <= vlanId:=4; port:=5; switch:=6;; *)
+(filter port=3 or vlanId=4) + drop == (filter port=3 or vlanId=4);;
+(filter port=3 or vlanId=4) + (filter port=3 or vlanId=4) == (filter port=3 or vlanId=4);;
+id; (filter port=3 or vlanId=4) == (filter port=3 or vlanId=4);;
+(filter port=3 or vlanId=4); id == (filter port=3 or vlanId=4);;
+(filter switch=2);(filter port=3 + filter vlanId=4) == (filter switch=2);(filter port=3) + (filter switch=2);(filter vlanId=4);;
+(filter port=3 + filter vlanId=4);(filter switch=2) == (filter port=3);(filter switch=2) + (filter vlanId=4);(filter switch=2);;
+(* FALSE!! *) (* filter port=3 <= filter port=4;; *)
+drop; (filter port=3 + filter vlanId=4) == drop;;
+(filter port=3 + filter vlanId=4); drop == drop;;
+id + (filter port=3 + filter vlanId=4); (filter port=3 + filter vlanId=4)* == (filter port=3 + filter vlanId=4)*;;
+
+(*  this is a trolltastic test.  it's true because both sides are equivalent *)
+(*  to the sum of all tests. *)
+(* (vlanId=5) + ((port=3 + vlanId=4); (port=3 + vlanId=4)* ) <= vlanId=5 + (port=3 + vlanId=4)* *)
+
+
+(* BOOLEAN ALGEBRA TIME! *)
+(filter port=4) + (filter port != 4) == id;;
+(filter port=4); (filter port != 4) == drop;;
+
+(* DUP-TACULAR! *)
+dup; filter port=5 == filter port=5; dup;;
+
+(* PACKET ALGEBRA *)
+port:=4; filter port=4 == port:=4;;
+filter port=4; port:=4 == filter port=4;;
+filter port=3; filter port=5 == drop;;
+
+
+(* from the other project *)
+(filter switch=0; (switch:=1))* <= id + switch:=1;;
+
+(port:=4; port:=3; filter port=3)* == id + port:=3;;
+
+(port:=4; port:=3; filter port=3) <= id + port:=3;;
+
+(port:=4; port:=3; filter port=3) ==  port:=3;;
+
+
+(* simple hops through the network *)
+
+filter(switch=0); switch:=1; dup; filter(switch=1); switch:=2; dup  ==  filter(switch=0); switch:=1; dup; switch:=2; dup;;
+
+filter(switch=0); switch:=1; dup; filter(switch=1) == filter(switch=0); switch:=1; dup;;
+
+(filter switch=3 + filter vlanId=4; vlanId:=4)*; (filter switch=4 + filter vlanId=5)* == (filter switch=3 + filter vlanId=4; vlanId:=4)*; (filter switch=4 + filter vlanId=5)*;;
+
+(filter port=3); (filter switch=4); (filter vlanId=2; vlanId:=3 + filter vlanId=3; vlanId:=2)*; (filter vport=1);
+(filter vswitch=4) <= filter port=0;;
+
+id + (filter port=1; switch:=2);(filter vlanId=3; drop) + (filter vlanId=3;drop) <= filter vlanId=3; drop;;
+
+(* FALSE !! *) (* id <= drop;; *)
+
+filter port=1; dup <= dup;;
+
+(* This eportploits non-canonicity of FDDs, naive implementation gets it wrong *)
+port:=1; switch:=2 == port:=1; switch:=2 + filter switch=2; port:=1;;
+
+filter port=0; switch:=0 + filter port=1; switch:=1 + filter port!=1; switch:=0
+  == filter port=1; switch:=1 + filter port!=1; switch:=0;;
+
+filter port=0; switch:=0 + filter port!=1; switch:=0
+  == filter port!=1; switch:=0

examples/decision-procedure/id.kat

@@ -0,0 +1 @@
+id

examples/decision-procedure/unrollable1.kat

@@ -0,0 +1,7 @@
+(* NetKAT automata have the strange property that they can sometimes be unrolled
+   into a loop-free automaton. This is an example for such an automaton.
+*)
+
+vlanId:=0;
+(dup; (filter vlanId=0; vlanId:=1 + filter vlanId=1; vlanId:=2))*;
+filter vlanId=1

examples/decision-procedure/unrollable2.kat

@@ -0,0 +1,8 @@
+(* NetKAT automata have the strange property that they can sometimes be unrolled
+   into a loop-free automaton.
+   This is the unrolled version of the "unrollable1.kat" automaton.
+*)
+
+vlanId:=0;
+dup; filter vlanId=0; vlanId:=1;
+filter vlanId=1

frenetic/Decide.ml

@@ -0,0 +1,48 @@
+open Core
+open Dump
+
+
+(*===========================================================================*)
+(* COMMANDS                                                                  *)
+(*===========================================================================*)
+
+
+module Main = struct
+  let spec = Command.Spec.(
+    empty
+    +> anon ("file" %: file)
+  )
+
+  let run file () =
+    let equalities = Frenetic_NetKAT_Parser.equalities_of_file file in
+    List.iter equalities ~f:(fun (p,q) ->
+      let open Frenetic_NetKAT_Pretty in
+      printf "===================================================\n";
+      printf "(%s)  ==  (%s)\n\n" (string_of_policy p) (string_of_policy q);
+      let (ta, (a1, a2)) = Dump.time (fun () ->
+        Frenetic_NetKAT_Compiler.Automaton.(of_pol p, of_pol q)) in
+      Dump.print_time ~prefix:"automata construction " ta;
+      let (th, rh) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Hopcroft.equiv a1 a2) in
+      printf "\nHopcroft: %s\n" (Bool.to_string rh);
+      Dump.print_time th;
+      let (ts, rs) = Dump.time (fun () ->
+        Frenetic_NetKAT_Equivalence.Simple.equiv a1 a2) in
+      printf "\nSimple: %s\n" (Bool.to_string rs);
+      Dump.print_time ts)
+
+end
+
+
+
+(*===========================================================================*)
+(* BASIC SPECIFICATION OF COMMANDS                                           *)
+(*===========================================================================*)
+
+
+let main : Command.t =
+  Command.basic
+    ~summary:"Parses file of NetKAT (in-)equalities and decides them."
+    (* ~readme: *)
+    Main.spec
+    Main.run

frenetic/Dump.ml

@@ -43,7 +43,7 @@ let time f =
   (t2 -. t1, r)
 
 let print_time ?(prefix="") time =
-  printf "%scompilation time: %.4f\n" prefix time
+  printf "%stime: %.4f\n" prefix time
 
 let print_order () =
   Frenetic_NetKAT_Compiler.Field.(get_order ()
@@ -148,7 +148,7 @@ end
 
 
 (*===========================================================================*)
-(* COMMANDS: Local, Global, Virtual, Auto                                    *)
+(* COMMANDS: Local, Global, Virtual, Auto, Decision                          *)
 (*===========================================================================*)
 
 module Local = struct
@@ -178,7 +178,7 @@ module Local = struct
       if printfdd then print_fdd fdd;
       if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
       print_all_tables ~no_tables fdd switches;
-      print_time t;
+      print_time ~prefix:"compilation " t;
 end
 
 
@@ -204,7 +204,7 @@ module Global = struct
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
-    print_time t;
+    print_time ~prefix:"compilation " t;
 
 end
 
@@ -259,8 +259,8 @@ module Virtual = struct
     if printfdd then print_fdd fdd;
     if dumpfdd then dump_fdd fdd ~file:(vpol_file ^ ".dot");
     print_all_tables ~no_tables fdd switches;
-    print_time ~prefix:"virtual " t1;
-    print_time ~prefix:"global " t2;
+    print_time ~prefix:"virtual compilation " t1;
+    print_time ~prefix:"global compilation " t2;
 end
 
 
@@ -277,13 +277,41 @@ module Auto = struct
   let run file json printorder dedup cheap_minimize () =
     let pol = parse_pol ~json file in
     let (t, auto) = time (fun () ->
-      Frenetic_NetKAT_Compiler.Automaton.of_policy pol ~dedup ~cheap_minimize) in
+      Frenetic_NetKAT_Compiler.Automaton.of_pol pol ~dedup ~cheap_minimize) in
     if printorder then print_order ();
     dump_auto auto ~file:(file ^ ".auto.dot");
     print_time t;
 
 end
 
+module Decision = struct
+  let spec = Command.Spec.(
+    empty
+    +> anon ("file-1" %: file)
+    +> anon ("file-2" %: file)
+    +> Flag.dump_auto
+    +> Flag.json
+    +> Flag.print_order
+  )
+
+  let run file1 file2 dumpauto json printorder () =
+    let pol1 = parse_pol ~json file1 in
+    let pol2 = parse_pol ~json file2 in
+    let (a1, a2) = Frenetic_NetKAT_Compiler.Automaton.(of_pol pol1, of_pol pol2) in
+    if printorder then print_order ();
+    if dumpauto then dump_auto a1 ~file:(file1 ^ ".auto.dot");
+    if dumpauto then dump_auto a2 ~file:(file2 ^ ".auto.dot");
+    let module Hopcroft = Frenetic_NetKAT_Equivalence.Hopcroft in
+    let module Simple = Frenetic_NetKAT_Equivalence.Simple in
+    let (th, h) = time (fun () -> Hopcroft.equiv a1 a2) in
+    let (ts, s) = time (fun () -> Simple.equiv a1 a2) in
+    printf "equivalent (Hopcroft): %s\n" (Bool.to_string h);
+    print_time th;
+    printf "\nequivalent (Simple): %s\n" (Bool.to_string s);
+    print_time ts
+
+end
+
 
 
 (*===========================================================================*)
@@ -318,8 +346,16 @@ let auto : Command.t =
     Auto.spec
     Auto.run
 
+let decision : Command.t =
+  Command.basic
+    ~summary:"Decides program equivalence."
+    (* ~readme: *)
+    Decision.spec
+    Decision.run
+
 let main : Command.t =
   Command.group
     ~summary:"Runs (local/global/virtual) compiler and dumps resulting tables."
     (* ~readme: *)
-    [("local", local); ("global", global); ("virtual", virt); ("auto", auto)]
+    [("local", local); ("global", global); ("virtual", virt); ("auto", auto);
+     ("decision", decision)]

frenetic/frenetic.ml

@@ -153,7 +153,8 @@ let main : Command.t =
     ; ("http-controller", http_controller)
     ; ("openflow13", openflow13_controller)
     ; ("fault-tolerant", openflow13_fault_tolerant_controller)
-    ; ("dump", Dump.main)]
+    ; ("dump", Dump.main)
+    ; ("decide", Decide.main)]
 
 let () =
   Frenetic_Util.pp_exceptions ();

lib/Frenetic_NetKAT_Compiler.ml

@@ -851,7 +851,7 @@ module Automaton = struct
     in
     Tbl.add_exn automaton.states ~key:id ~data:(Lazy.from_fun f)
 
-  let of_policy ?(dedup=true) ?ing ?(cheap_minimize=true) (pol : Frenetic_NetKAT.policy) : t =
+  let of_pol ?(dedup=true) ?ing ?(cheap_minimize=true) (pol : Frenetic_NetKAT.policy) : t =
     let automaton = create_t0 () in
     let pol = Pol.of_pol ing pol in
     let () = add_policy automaton (automaton.source, pol) in
@@ -971,7 +971,7 @@ end
 
 let compile_global ?(options=default_compiler_options) ?(pc=Field.Vlan) pol : FDD.t =
   prepare_compilation ~options pol;
-  Automaton.of_policy pol
+  Automaton.of_pol pol
   |> Automaton.to_local ~pc
 
 

lib/Frenetic_NetKAT_Compiler.mli

@@ -10,23 +10,33 @@ type order
     | `Static of Field.t list
     | `Heuristic ]
 
-module FDD : module type of Frenetic_Fdd.FDD
+module FDD : sig
+  include module type of Frenetic_Fdd.FDD
+  val union : t -> t -> t
+  val seq : t -> t -> t
+  val star : t -> t
+end
+
 type t = FDD.t
 (** The type of the intermediate compiler representation (FDD). *)
 
 val to_dot : t -> string
 
 (** Intermediate representation of global compiler: NetKAT Automata *)
 module Automaton : sig
-  type t
+  type t = private
+    { states : (FDD.t * FDD.t) Int.Table.t;
+      has_state : int FDD.BinTbl.t;
+      mutable source : int;
+      mutable nextState : int }
 
   val fold_reachable: ?order:[< `Post | `Pre > `Pre ]
     -> t
     -> init:'a
     -> f:('a -> int -> (FDD.t * FDD.t) -> 'a)
     -> 'a
 
-  val of_policy: ?dedup:bool -> ?ing:pred -> ?cheap_minimize:bool -> policy -> t
+  val of_pol: ?dedup:bool -> ?ing:pred -> ?cheap_minimize:bool -> policy -> t
   val to_local: pc:Field.t -> t -> FDD.t
 
   val to_dot: t -> string