Skip to content

XJTU-NetVerify/NDD

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

10 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

A library for Network Decision Diagram (NDD)

This is an implementation of the following paper:

Zechun Li, Peng Zhang, Yichi Zhang, and Hongkun Yang. "NDD: A Decision Diagram for Network Verification", NSDI 2025

Introduction

Network Decision Diagram (NDD) is a new decision diagram based on the classical Binary Decision Diagram (BDD). In BDD, each node looks at a single bit, and branches based on whether the bit is true or false; while in NDD, each node looks at a field which either bears some semantics meaning, say an IP address, or simply a fixed number of bits. Since the node may have more than 2 branches, we represent the branching condition with external data structures. Current, NDD uses BDD to represent the branching condition: if the field has $n$ bits, then the condition for each branch is a BDD with $n$ variables. In this sense, NDD can be seen as wrapping the original BDD with another layer of decision diagram, and therefore can also be interpreted as "Nested Decision Diagram".

Benchmark

Benchmark (time second) on NQueens

N BDD (JDD) BDD (JavaBDD - JFactory) NDD (JNDD)
6 0.017 0.056 0.012
7 0.023 0.072 0.019
8 0.04 0.109 0.038
9 0.223 0.28 0.176
10 0.615 0.913 0.344
11 2.567 4.424 2.257
12 19.109 33.024 12.417

More benchmarks will be available soon.

The Origin of NDD

NDD was originally proposed for network verification, where each NDD node represents a packet header field (destination IP address) We observed NDD was more efficient than BDD in terms of memory and computation. The reason is due to the locality of field-based matching semantics, NDD can significantly reduce the number of BDD nodes for each field. The figure below shows an example, where the three BDDs in (a) can be represented by three equivalent NDDs in (c), where each edge of which is labelled by per-field BDDs in (b).

fig4 drawio

Project Structure

  • /doc stores an api documentation generated by javadoc.
  • /lib stores the third party jar packages.
    • jdd-111.jar is a modified version of jdd library. The jar has been decompiled into /src/main/java/jdd so it can be edited directly.
    • javabdd_1.0b2.tar.gz is the original version of javabdd (for comparison).
  • /results stores some experimental results generated by codes in /src/experiment.
  • /src stores source code.

Getting Started

add <dependency> in pom.xml

<dependencies>
    <dependency>
        <groupId>org.ants</groupId>
        <artifactId>ndd</artifactId>
        <version>1.0</version>
        <scope>system</scope>
        <systemPath>${project.basedir}/lib/ndd-1.0-jar-with-dependencies.jar</systemPath>
    </dependency>
</dependencies>

After Maven sync, jndd and javandd can be chosen to import by:

import org.ants.jndd.*;
// or
import org.ants.javandd.*;

JNDD

/**
 * init NDD library
 * define cache size by `initNDD(NDD_TABLE_SIZE, NDD_CACHE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE)` if required (default 10000)
 */
NDD.initNDD(NDD_TABLE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE);

/**
 * declare ndd fields based on the situation {x, y, z}
 * declareField() only records the bit count, does not create BDD variables yet
 */
for (int i = 0; i < n; i++) {
    NDD.declareField(n);    // same number of variables in every field in nqueens
}

/**
 * generate fields after all declarations
 * this creates shared BDD variables with right-alignment for maximum node reuse
 */
NDD.generateFields();

/**
 * ndd logical operation
 */
NDD[] orBatch = new NDD[n];
for (int i = 0; i < n; i++) {
    /**
     * `getTrue()` or `getFalse()` to get NDD terminal nodes
     */
    NDD condition = NDD.getFalse();
    for (int j = 0; j < n; j++) {
        /**
         * `getVar(field_num, num)` same as `ithVar` after `createVar` in BDD
         * `orTo` will free (`deref`) the NDD variable in the first parameter
         * use `or` instead to keep it
         */
        condition = NDD.orTo(condition, NDD.getVar(i, j));
    }
    orBatch[i] = condition;
}

NDD queen = NDD.getTrue();

/**
 * sat count for result
 */
NDD.satCount(queen);

JavaNDD

If you are using a BDD version of factory and changing to NDD, please refer to src/main/java/org/ants/javandd/README.md

BDDFactory factory = new NDDFactory(BDD_TABLE_SIZE, BDD_CACHE_SIZE);

int[] fields = {}; // partion fields

factory.setVarNum(fields, NDD_TABLE_SIZE);

BDD TRUE = factory.one();
BDD FALSE = factory.zero();

BDD[] bdd_list = {};
for () {
    // or use `factory.getVar(field_num, num)` but it is incompatible with other factory
    // `ithVar(i)` will find its `field_num` first
    bdd_list[i] = factory.ithVar(i);
}

for (BDD bdd : bdd_list) {
    TRUE.and(bdd);
    FALSE.orWith(bdd);  // `applyWith` will free (`deref`) the BDD in parameter
}

return TRUE.satCount();

It is our first time to get access to the APIs in JavaBDD. If some are misunderstood, please contact us or Pull Request if you can. Your contribution to Network Decision Diagram is much appreciated.

GC Log Output

NDD provides optional GC (Garbage Collection) log output for debugging and performance analysis. When enabled, detailed logs will be printed before and after GC operations for both JDD (BDD layer) and NDD layers.

Enable GC Log

import jdd.util.Options;

// Enable GC log output
Options.gc_log = true;

// Disable GC log output (default)
Options.gc_log = false;

Log Output Format

When Options.gc_log = true, GC operations will output logs like:

[JDD GC] Start: table_size=10000, free_nodes=500, dead_nodes=100
[NDD GC] Start (triggered by JDD prehook): currentSize=5000, tableSize=100000
[NDD GC] End (triggered by JDD prehook): freed=200, currentSize=4800, time=15ms
[JDD GC] End: #5, freed=300, free_nodes=800, time=25ms

For JavaNDD (NDDFactory), the log prefix is [JavaNDD GC] instead of [NDD GC].

The triggered by field indicates whether the NDD GC was:

  • JDD prehook: Called automatically before JDD GC to ensure NDD nodes are cleaned up first
  • NDD self: Triggered by NDD's own table size limit

Bibtex

@inproceedings {NDD,
  author = {Zechun Li, Peng Zhang, Yichi Zhang, Hongkun Yang},
  title = {{NDD}: A Decision Diagram for Network Verification},
  booktitle = {22th USENIX Symposium on Networked Systems Design and Implementation (NSDI 25)},
  year = {2025},
  isbn = {},
  address = {},
  pages = {},
  url = {https://www.usenix.org/conference/nsdi25/presentation},
  publisher = {USENIX Association},
  month = apr
}

Contact

License

Apache-2.0 License, see LICENSE.

About

[NSDI'25] The library of Network Decision Diagram based on JDD.

Resources

License

Stars

Watchers

Forks

Packages

 
 
 

Contributors

Languages