-
Notifications
You must be signed in to change notification settings - Fork 8
Design Notes
This page gives the implementation-level rationale behind the optimized branch.
It is meant for readers who already understand what NDD is and want to know how this repository's array-backed implementation is organized internally.
The optimized branch keeps the same conceptual model:
- one NDD node corresponds to one field
- each outgoing edge is guarded by a lower-level decision-diagram label
- logical operations recurse over fields and labels
What changes is the storage and execution strategy used to implement that model efficiently in Java.
The original implementation represented each node as an object with nested edge structures. In this branch, NodeTable.java stores node state in parallel arrays.
That means:
- node metadata lives in dense primitive arrays
- edge payloads are stored in shared arrays
- canonical nodes reference edge blocks by index rather than owning separate edge containers
This is the main memory-layout change behind the current NDD implementation.
During recursive logical operations, the implementation accumulates candidate edges in one shared stack-like structure instead of allocating temporary maps inside each call. Each recursive operation owns a stack frame [frameStart, stackTop) in that shared buffer.
Two helpers in NDD.java manage the frame:
-
edgeCollect(target, label)appends one edge to the current frame in O(1). It does not deduplicate on the way in: duplicate targets are tolerated and merged later. The earlier implementation merged duplicates on every collect, which cost an O(D^2) linear scan per node at high fan-out D; deferring the merge keeps this hot path branch-free. -
edgeFlush(field)turns the frame into a canonical node. It (1) sorts the frame by target, (2) merges runs of equal targets with a consuming OR on their labels, then (3) creates or reuses the node throughNodeTable.mk, which requires a sorted, deduplicated edge order.
The sort inside edgeFlush is size-adaptive:
- small/medium frames use an in-place quicksort that falls back to insertion sort for short runs. NDD fan-out is usually tiny, so this matches the cost of the previous insertion-sort path in the common case.
- large frames — at or above
ndd.radixThreshold(default 64) — use an O(n) LSD radix sort over the packed(target, label)pairs, which avoids the comparison-sort blow-up at high fan-out.
Safe-point maintenance after the recursion unwinds keeps retired stack and edge slots reusable.
The point of this design is to keep the hot collect path allocation-free, then defer the single canonicalization step (sort + merge) to one place that can pick the right algorithm for the frame size.
declareField(...) and generateFields() are deliberately separate.
Why:
- the implementation needs to know every field width before laying out shared BDD variables
- that global view is what makes right-aligned reuse possible within each label backend
- it also keeps the field model explicit for packet-processing applications
For mixed diagrams, fields are grouped by LabelMode. Each group computes its own maximum width
and creates one shared right-aligned variable layout, so BDD, BCDD, and finite-domain ZDD fields do
not allocate duplicate engines or lose reuse among fields of the same type.
This is why the library expects users to commit to a field partition and its label modes early.
The array-backed layout introduces a constraint that the implementation must respect: recursive operations may still hold raw edge-array positions while the recursion stack is active.
Because of that, edge compaction and retired-slot reuse happen only at safe points after recursion unwinds. Relevant methods include:
NDD.runSafePointMaintenance()NodeTable.compactEdgesIfNeeded()NodeTable.compactEdgesAtSafePoint()
The low-level implementation supports multiple edge-label engines behind one internal backend interface:
- standard BDD labels
- complemented-edge BDD labels
- finite-domain ZDD labels
declareField(width, mode) selects a backend per field. The overload without a mode uses the
initialization default. A small backend registry creates at most one engine for each active
LabelMode; unused modes allocate no engine.
An edge does not store a backend tag. Its parent NDD node already stores a field index, and that field determines the backend used to interpret, reference, combine, count, or release the edge label. Labels are combined only when recursive operations reach the same field, so handles from different engines never participate in the same label operation even if their integer values coincide.
Common label operations such as ref, deref, and, or, diff, not, matches, satCount,
node counting, and GC go through the same backend API. The edge collector carries the owning field
when it may release a label; NodeTable.mk and NDD GC similarly derive the backend from the node's
field. This avoids adding a backend array to the node or edge table.
Homogeneous diagrams retain a direct labelBackend fast path. Only diagrams that actually mix
modes perform a field-to-backend lookup. Per-engine node creation counters are used for statistics
because the legacy JDD counter is process-global and cannot distinguish simultaneous BDD and ZDD
engines.
The current mixed-mode boundaries are deliberate:
-
substituterequires source and target fields to use the same backend and width -
encodePrefixsupports binary BDD/BCDD fields, not finite-domain ZDD fields - raw-label
refLabel/derefLabelcalls require a field in mixed mode -
toBDDandtoNDDremain homogeneous standard-BDD conversion helpers
The low-level API uses integer node IDs. This matches the array-backed representation and avoids wrapper allocation on the hot path.
The NDDFactory layer keeps a BDDFactory-style API for compatibility with codebases built around JavaBDD.
That compatibility layer is especially relevant for the Batfish-style integration documented in Network Verification Applications.
When reading the result pages:
-
NDD-Originis the baseline implementation -
NDD-Reuseisolates the effect of shared-BDD-variable reuse -
NDDadds the array-backed node table and stack-based edge collection
That split is useful because it shows which gains come from better symbolic structure and which come from the new runtime representation.