package frenetic

  1. Overview
  2. Docs
package frenetic
Legend:
Library
Module
Module type
Parameter
Class
Class type

Forwarding Decision Diagrams

FDD's are an extension of Binary Decision Diagrams (BDD's). NetKAT predicates, which are mostly based on OpenFlow matches, are just binary formulas after all. An FDD extends a BDD by (1) using OpenFlow actions at the leaves instead of binary values True and False (2) using complete header matches instead of individual bit matches.

As in BDD's, field ordering is important to prevent combinatorial explosions. Fortunately we can exploit what goes in real FDD's to get decent heuristics. Nevertheless, the field ordering is part of the data structure and can also be set manually by the programming through compiler options.

Basically, the flow goes: you turn NetKAT into an FDD, then an FDD into a Flow Table. See paper "A Fast Compiler for NetKAT" (http://www.cs.cornell.edu/~jnfoster/papers/netkat-compiler.pdf) for details and theory behind it. FDD's are nice because you can operate on them using the full well-established theory of BDD's.

module Field : sig ... end
module Value : sig ... end

In a BDD, each node is an implicit predicate, "variable = true". In a FDD, each node is a test of a field against a particular value, as in EthSrc = "FE:89:00:12:34:12". The edges are either true or false just like in a BDD. But we also use values in modifcations - as in "port := 2". Note only Const and Mask are really used by OpenFlow. Both Pipe and Query are translated to the pseudoport Controller.

exception FieldValue_mismatch of Field.t * Value.t
module Pattern : sig ... end
module Action : sig ... end
module FDD : sig ... end