Skip to content

Commit c7a661d

Browse files
AugistsAugists
authored
Merge pull request #8 from TelosCheney/SoA
Optimize NDD implementation with SoA
2 parents 73191c2 + 075ab53 commit c7a661d

512 files changed

Lines changed: 10400 additions & 253090 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎README.md‎

Lines changed: 77 additions & 205 deletions
Original file line numberDiff line numberDiff line change
@@ -1,256 +1,128 @@
1-
# A library for Network Decision Diagram (NDD)
1+
# NDD-SoA
22

3-
This is an implementation of the following [paper](https://xjtu-netverify.github.io/papers/NDD/NDD-final-version.pdf):
3+
`NDD-SoA` is a performance-oriented branch of **Network Decision Diagram (NDD)**. It keeps the original NDD idea and benchmark targets, but replaces the object-heavy internal representation with a structure-of-arrays layout and a shared edge-collection stack so the hot path allocates less and reuses more.
44

5-
> Zechun Li, Peng Zhang, Yichi Zhang, and Hongkun Yang. "NDD: A Decision Diagram for Network Verification", NSDI 2025
5+
This tree is prepared as the optimized branch snapshot for upstreaming back into `NDD`. The original paper is: [NDD: A Decision Diagram for Network Verification](https://xjtu-netverify.github.io/papers/NDD/NDD-final-version.pdf), NSDI 2025.
66

7-
## Introduction
7+
## What Changed
88

9-
**Network Decision Diagram (NDD)** is a new decision diagram based on the classical Binary Decision Diagram (BDD).
10-
In BDD, each node looks at a single **bit**, and branches based on whether the bit is true or false;
11-
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.
12-
Since the node may have more than 2 branches, we represent the branching condition with external data structures.
13-
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.
14-
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".
9+
- Replaced the original nested `HashMap`-based node representation with array-backed storage in [`NodeTable.java`](src/main/java/org/ants/jndd/nodetable/NodeTable.java).
10+
- Removed per-node `NDD` objects from the JNDD hot path; JNDD operations now work on integer node IDs backed by SoA storage.
11+
- Replaced temporary edge maps with one global stack-based edge collector in [`NDD.java`](src/main/java/org/ants/jndd/diagram/NDD.java).
12+
- Right-aligned fields so compatible domains share the same underlying BDD variables, reducing BDD node counts.
13+
- Kept `JavaNDD` (`NDDFactory`) usage available for codebases that prefer a `BDDFactory`-style API.
1514

16-
## Benchmark
15+
## Variant Map
1716

18-
Benchmark (time `second`) on **NQueens**
17+
The benchmark results in this repository use the following names:
1918

20-
| N | BDD (JDD) | BDD (JavaBDD - JFactory) | NDD (JNDD) |
21-
| - | --------- | ------------- | -------------------- |
22-
| 6 | 0.017 | 0.056 | 0.012 |
23-
| 7 | 0.023 | 0.072 | 0.019 |
24-
| 8 | 0.04 | 0.109 | 0.038 |
25-
| 9 | 0.223 | 0.28 | 0.176 |
26-
| 10 | 0.615 | 0.913 | 0.344 |
27-
| 11 | 2.567 | 4.424 | 2.257 |
28-
| 12 | 19.109 | 33.024 | 12.417 |
19+
| Variant | Meaning |
20+
| --- | --- |
21+
| `ndd` | Original object-based NDD baseline |
22+
| `ndd-reuse` | Baseline NDD plus shared-BDD-variable reuse |
23+
| `ndd-soa` | The version in this repository: reuse + global edge stack + SoA node table |
2924

30-
More benchmarks will be available soon.
25+
## Repository Layout
3126

32-
## The Origin of NDD
27+
- [`src/`](src/) contains the Java source code, including `jndd`, `javandd`, and application examples.
28+
- [`doc/javadoc/`](doc/javadoc/) contains the regenerated API documentation for the SoA branch.
29+
- [`lib/`](lib/) contains bundled third-party artifacts such as `jdd-111.jar`.
30+
- [`results/`](results/) contains the current benchmark data and plots for this branch.
31+
- [`wiki/Optimization-Summary.md`](wiki/Optimization-Summary.md) summarizes the optimization work in reviewer-facing form.
32+
- [`wiki/`](wiki/) contains GitHub Wiki-ready pages for installation, usage, parameters, and detailed benchmark results.
3333

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

40-
![fig4 drawio](NDD.svg)
36+
Build the project with Maven:
4137

42-
<!--
43-
**Atomized Network Decision Diagram (Atomized NDD)** is an extension of NDD, which offers a native support for equivalence classes, a key technique underlying most network verifiers.
44-
In atomized NDD, the label of each edge is a set of atoms, instead of a BDD as in standard NDD.
45-
Using atomized NDD, network verifiers do not need to implement their own algorithms for computing and updating equivalence classes.
46-
47-
48-
### Definitions
49-
50-
**Definition 1.** A **Network Decision Diagram (NDD)** is a rooted, directed acyclic graph with:
51-
52-
- two terminal nodes ***true*** and ***false***, with an out-degree of zero.
53-
54-
- a set of non-terminal nodes. Each node u is associated with a variable var(u) representing a field of one or multiple bits, and has a set of outgoing edges, denoted as edges(u). Each e $\in$ edges(u) points to a successor of u, denoted as next(e), and has a predicate over the variable var(u), denoted as label(e).
55-
56-
- $\forall u, \forall x, y \in edges(u)$ with $x \ne y$: $label(x)\wedge label(y) = false$, and $\bigvee_{e \in edges(u)}label(e) = true$.
57-
58-
**Todo: add a figure of redundancy in NDD.**
59-
60-
**Definition 2.** A NDD is said to be an **Ordered (ONDD)** if the field variables follow a fixed variable order
61-
(say $f_1 < f_2 < ...,< f_n$ where $f_i < f_j$ means variable $f_i$ appears before variable $f_j$) on all paths through the graph. An ONDD is said to be a **Reduced (RONDD)** if it satisfies the following three conditions:
62-
- Uniqueness: no two distinct nodes represent the same variable and have the same successors;
63-
- No redundant node: no non-terminal node has only edge e with $label(e) = true$;
64-
- No redundant edges: no two edges from the same node point to the same successor, i.e., $\forall u,\forall x, y \in edge(u) : next(x) = next(y) \Rightarrow x = y$.
65-
66-
**Definition 3.** Given a set of NDDs $N$ for a set of variables $F$, we say $A(f) = {{a_1}^f,...,{a_k}^f}$ is the set of **atoms** for variable $f \in F$, with respect with $N$ , if it satisfies the following conditions:
67-
- $a_i^f \ne false,\forall i ∈ {1,..., k}$;
68-
- $\vee_{i=1}^k a_i^f = true$;
69-
- $a_i^f∧a_j^f = false$, if $i \ne j$;
70-
- $\forall e \in edges(u)$, $u$ is a node of $N$ $var(u) = f$: there exists a set $atoms(e) \subset A(f)$, s.t., $label(e) = $\bigvee_{a \in atoms(e)}a$;
71-
- $k$ is the minimum number satisfy the above properties.
72-
73-
**Definition 4.** Given a set of NDDs $N$, we say $N^a$ a is the **atomized NDDs** of $N$, if $N^a = N$ , except that for each $e$ of $N^a$: $label(e) \leftarrow atoms(e)$.
74-
-->
75-
76-
## Project Structure
77-
78-
- `/doc` stores an api documentation generated by `javadoc`.
79-
- `/lib` stores the third party jar packages.
80-
- `jdd-111.jar` is a modified version of [jdd library](https://bitbucket.org/vahidi/jdd). The jar has been decompiled into `/src/main/java/jdd` so it can be edited directly.
81-
- `javabdd_1.0b2.tar.gz` is the original version of [javabdd](https://sourceforge.net/projects/javabdd/) (for comparison).
82-
- `/results` stores some experimental results generated by codes in `/src/experiment`.
83-
- `/src` stores source code.
84-
85-
## Getting Started
86-
87-
* lib
88-
* `/lib/ndd-1.0-jar-with-dependencies.jar`
89-
* [`/lib/jdd-111.jar`](https://github.com/Augists/jdd/releases/tag/111-modified)
90-
91-
add `<dependency>` in `pom.xml`
92-
93-
```xml
94-
<dependencies>
95-
<dependency>
96-
<groupId>org.ants</groupId>
97-
<artifactId>ndd</artifactId>
98-
<version>1.0</version>
99-
<scope>system</scope>
100-
<systemPath>${project.basedir}/lib/ndd-1.0-jar-with-dependencies.jar</systemPath>
101-
</dependency>
102-
</dependencies>
38+
```bash
39+
mvn -DskipTests package
10340
```
10441

105-
After Maven sync, `jndd` and `javandd` can be chosen to import by:
106-
107-
```java
108-
import org.ants.jndd.*;
109-
// or
110-
import org.ants.javandd.*;
111-
```
112-
113-
### JNDD
114-
115-
```java
116-
/**
117-
* init NDD library
118-
* define cache size by `initNDD(NDD_TABLE_SIZE, NDD_CACHE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE)` if required (default 10000)
119-
*/
120-
NDD.initNDD(NDD_TABLE_SIZE, BDD_TABLE_SIZE, BDD_CACHE_SIZE);
121-
122-
/**
123-
* declare ndd fields based on the situation {x, y, z}
124-
* declareField() only records the bit count, does not create BDD variables yet
125-
*/
126-
for (int i = 0; i < n; i++) {
127-
NDD.declareField(n); // same number of variables in every field in nqueens
128-
}
129-
130-
/**
131-
* generate fields after all declarations
132-
* this creates shared BDD variables with right-alignment for maximum node reuse
133-
*/
134-
NDD.generateFields();
135-
136-
/**
137-
* ndd logical operation
138-
*/
139-
NDD[] orBatch = new NDD[n];
140-
for (int i = 0; i < n; i++) {
141-
/**
142-
* `getTrue()` or `getFalse()` to get NDD terminal nodes
143-
*/
144-
NDD condition = NDD.getFalse();
145-
for (int j = 0; j < n; j++) {
146-
/**
147-
* `getVar(field_num, num)` same as `ithVar` after `createVar` in BDD
148-
* `orTo` will free (`deref`) the NDD variable in the first parameter
149-
* use `or` instead to keep it
150-
*/
151-
condition = NDD.orTo(condition, NDD.getVar(i, j));
152-
}
153-
orBatch[i] = condition;
154-
}
155-
156-
NDD queen = NDD.getTrue();
42+
The default Maven build targets the core `JNDD` / `JavaNDD` paths and the maintained examples. Experimental paths that still depend on the pre-SoA object-based API are excluded from the default compile for now:
15743

158-
/**
159-
* sat count for result
160-
*/
161-
NDD.satCount(queen);
162-
```
44+
- `org.ants.jndd.diagram.AtomizedNDD`
45+
- `org.ants.jndd.nodetable.AtomizedNodeTable`
46+
- `application.nqueen.FiniteDomainZddNDDSolution`
47+
- `application.wan.bdd.*`
48+
- `application.wan.ndd.*`
16349

164-
### JavaNDD
165-
166-
> If you are using a BDD version of factory and changing to NDD, please refer to [`src/main/java/org/ants/javandd/README.md`](/src/main/java/org/ants/javandd/README.md)
50+
For the low-level `JNDD` API, the optimized implementation now uses integer node IDs:
16751

16852
```java
169-
BDDFactory factory = new NDDFactory(BDD_TABLE_SIZE, BDD_CACHE_SIZE);
170-
171-
int[] fields = {}; // partion fields
53+
NDD.initNDD(nddTableSize, nddCacheSize, bddTableSize, bddCacheSize);
17254

173-
factory.setVarNum(fields, NDD_TABLE_SIZE);
174-
175-
BDD TRUE = factory.one();
176-
BDD FALSE = factory.zero();
177-
178-
BDD[] bdd_list = {};
179-
for () {
180-
// or use `factory.getVar(field_num, num)` but it is incompatible with other factory
181-
// `ithVar(i)` will find its `field_num` first
182-
bdd_list[i] = factory.ithVar(i);
55+
for (int i = 0; i < fieldCount; i++) {
56+
NDD.declareField(fieldBitWidths[i]);
18357
}
58+
NDD.generateFields();
18459

185-
for (BDD bdd : bdd_list) {
186-
TRUE.and(bdd);
187-
FALSE.orWith(bdd); // `applyWith` will free (`deref`) the BDD in parameter
60+
int acc = NDD.getFalse();
61+
for (int bit = 0; bit < fieldBitWidths[0]; bit++) {
62+
acc = NDD.orTo(acc, NDD.getVar(0, bit));
18863
}
18964

190-
return TRUE.satCount();
65+
double sat = NDD.satCount(acc);
19166
```
19267

193-
> 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 **N**etwork **D**ecision **D**iagram is much appreciated.
68+
For the `JavaNDD` factory-style API, see [`wiki/Usage.md`](wiki/Usage.md) and [`src/main/java/org/ants/javandd/README.md`](src/main/java/org/ants/javandd/README.md).
19469

195-
## GC Log Output
70+
## Performance Snapshot
19671

197-
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.
72+
### NQueens
19873

199-
### Enable GC Log
200-
201-
```java
202-
import jdd.util.Options;
74+
Compared with the original `NDD` baseline, `NDD-SoA` keeps the same solution counts while reducing runtime and memory use on the tested Java NQueens workload:
20375

204-
// Enable GC log output
205-
Options.gc_log = true;
76+
| Size | NDD time (s) | NDD-SoA time (s) | Speedup | NDD max RSS (KB) | NDD-SoA max RSS (KB) | RSS reduction |
77+
| --- | ---: | ---: | ---: | ---: | ---: | ---: |
78+
| 10 | 0.744 | 0.221 | 3.37x | 314148 | 134680 | 57.1% |
79+
| 11 | 2.835 | 0.792 | 3.58x | 603572 | 218416 | 63.8% |
80+
| 12 | 14.821 | 4.353 | 3.40x | 2233308 | 579796 | 74.0% |
20681

207-
// Disable GC log output (default)
208-
Options.gc_log = false;
209-
```
82+
Detailed tables and plots: [`wiki/Results-NQueens.md`](wiki/Results-NQueens.md)
21083

211-
### Log Output Format
84+
### SRE
21285

213-
When `Options.gc_log = true`, GC operations will output logs like:
86+
On the SRE benchmark set, the SoA implementation consistently improves over the original `ndd` variant on medium and large cases:
21487

215-
```
216-
[JDD GC] Start: table_size=10000, free_nodes=500, dead_nodes=100
217-
[NDD GC] Start (triggered by JDD prehook): currentSize=5000, tableSize=100000
218-
[NDD GC] End (triggered by JDD prehook): freed=200, currentSize=4800, time=15ms
219-
[JDD GC] End: #5, freed=300, free_nodes=800, time=25ms
220-
```
88+
| Dataset | Metric | NDD | NDD-SoA | Improvement |
89+
| --- | --- | ---: | ---: | ---: |
90+
| `bgp_fattree08`, `MF=3` | total time (s) | 60.829 | 25.602 | 2.38x faster |
91+
| `bgp_fattree08`, `MF=3` | peak RSS (MB) | 4220.4 | 2046.0 | 51.5% lower |
92+
| `bgp_fattree08`, `MF=3` | BDD nodes | 38199434 | 3208829 | 91.6% fewer |
93+
| `bgp_fattree12`, `MF=3` | total time (s) | 636.086 | 230.906 | 2.75x faster |
94+
| `bgp_fattree12`, `MF=3` | peak RSS (MB) | 26274.3 | 18113.7 | 31.1% lower |
95+
| `bgp_fattree16`, `MF=2` | total time (s) | 1178.287 | 472.056 | 2.50x faster |
22196

222-
For JavaNDD (NDDFactory), the log prefix is `[JavaNDD GC]` instead of `[NDD GC]`.
97+
Detailed tables: [`wiki/Results-SRE.md`](wiki/Results-SRE.md)
22398

224-
The `triggered by` field indicates whether the NDD GC was:
225-
- `JDD prehook`: Called automatically before JDD GC to ensure NDD nodes are cleaned up first
226-
- `NDD self`: Triggered by NDD's own table size limit
99+
## Documentation
227100

101+
- Overview: [`wiki/Home.md`](wiki/Home.md)
102+
- Optimization summary: [`wiki/Optimization-Summary.md`](wiki/Optimization-Summary.md)
103+
- Installation and build: [`wiki/Installation.md`](wiki/Installation.md)
104+
- API usage: [`wiki/Usage.md`](wiki/Usage.md)
105+
- Parameter guide: [`wiki/Parameters.md`](wiki/Parameters.md)
106+
- Benchmark methodology: [`wiki/Benchmarks.md`](wiki/Benchmarks.md)
107+
- Design notes for this branch: [`wiki/Design-Notes.md`](wiki/Design-Notes.md)
228108

109+
## Paper and Citation
229110

230-
## Bibtex
111+
- Paper PDF: <https://xjtu-netverify.github.io/papers/NDD/NDD-final-version.pdf>
112+
- NSDI 2025 page: <https://www.usenix.org/conference/nsdi25/presentation>
231113

232114
```bibtex
233-
@inproceedings {NDD,
234-
author = {Zechun Li, Peng Zhang, Yichi Zhang, Hongkun Yang},
115+
@inproceedings{NDD,
116+
author = {Zechun Li and Peng Zhang and Yichi Zhang and Hongkun Yang},
235117
title = {{NDD}: A Decision Diagram for Network Verification},
236118
booktitle = {22th USENIX Symposium on Networked Systems Design and Implementation (NSDI 25)},
237119
year = {2025},
238-
isbn = {},
239-
address = {},
240-
pages = {},
241120
url = {https://www.usenix.org/conference/nsdi25/presentation},
242121
publisher = {USENIX Association},
243122
month = apr
244123
}
245124
```
246125

247-
### Contact
248-
249-
- Zechun Li (1467874668@qq.com)
250-
- Peng Zhang (p-zhang@xjtu.edu.cn)
251-
- Yichi Zhang (augists@outlook.com)
252-
- Hongkun Yang (hkyang@google.com)
253-
254126
## License
255127

256-
Apache-2.0 License, see [LICENSE](LICENSE).
128+
Apache-2.0. See [`LICENSE`](LICENSE).

0 commit comments

Comments
 (0)