Module Frenetic_netkat.FddSource

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.