Skip to content

Commit

Permalink
Performance optimizations
Browse files Browse the repository at this point in the history
  • Loading branch information
nhusung committed Oct 13, 2024
1 parent 7084b14 commit 8f0874b
Show file tree
Hide file tree
Showing 10 changed files with 81 additions and 63 deletions.
7 changes: 6 additions & 1 deletion crates/oxidd-core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,10 @@ pub trait InnerNode<E: Edge>: Sized + Eq + Hash + DropWith<E> {
/// number and want to get the level number.
fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool;

/// Panics if the node types stores a level and the node's level is not
/// `level`
fn assert_level_matches(&self, level: LevelNo);

/// Get the children of this node as an iterator
#[must_use]
fn children(&self) -> Self::ChildrenIter<'_>;
Expand Down Expand Up @@ -293,7 +297,8 @@ pub type AtomicLevelNo = std::sync::atomic::AtomicU32;
/// 1. A node in a [`LevelView`] with level number L has level number L (i.e.
/// `self.level()` returns L).
/// 2. [`InnerNode::check_level()`] with a check `c` must return
/// `c(self.level())`.
/// `c(self.level())`. Similarly, [`InnerNode::assert_level_matches()`] must
/// panic if the level does not match.
///
/// These conditions are crucial to enable concurrent level swaps as part of
/// reordering (see the `oxidd-reorder` crate): The algorithm iterates over the
Expand Down
22 changes: 5 additions & 17 deletions crates/oxidd-manager-index/src/manager.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1004,7 +1004,7 @@ where
Ok(e2)
}

#[inline]
#[inline(always)]
fn level(&self, no: LevelNo) -> Self::LevelView<'_> {
LevelView {
store: self.store(),
Expand Down Expand Up @@ -1486,19 +1486,13 @@ where
// No need to check if the node referenced by `edge` is stored in
// `self.store` due to lifetime restrictions.
let nodes = &self.store.inner_nodes;
nodes.inner_node(&edge).check_level(|level| {
assert_eq!(level, self.level, "node level does not match");
true
});
nodes.inner_node(&edge).assert_level_matches(self.level);
self.set.insert(nodes, edge)
}

#[inline(always)]
fn get_or_insert(&mut self, node: N) -> AllocResult<Edge<'id, N, ET>> {
node.check_level(|level| {
assert_eq!(level, self.level, "node level does not match");
true
});
node.assert_level_matches(self.level);
// No need to check if the children of `node` are stored in `self.store`
// due to lifetime restrictions.
self.set.get_or_insert(
Expand Down Expand Up @@ -1605,19 +1599,13 @@ where
// No need to check if the node referenced by `edge` is stored in
// `self.store` due to lifetime restrictions.
let nodes = &self.store.inner_nodes;
nodes.inner_node(&edge).check_level(|level| {
assert_eq!(level, self.level, "node level does not match");
true
});
nodes.inner_node(&edge).assert_level_matches(self.level);
self.set.insert(nodes, edge)
}

#[inline(always)]
fn get_or_insert(&mut self, node: N) -> AllocResult<Edge<'id, N, ET>> {
node.check_level(|level| {
assert_eq!(level, self.level, "node level does not match");
true
});
node.assert_level_matches(self.level);
// No need to check if the children of `node` are stored in `self.store`
// due to lifetime restrictions.
self.set.get_or_insert(
Expand Down
9 changes: 9 additions & 0 deletions crates/oxidd-manager-index/src/node/fixed_arity.rs
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,15 @@ impl<'id, ET: Tag, const ARITY: usize> InnerNode<manager::Edge<'id, Self, ET>>
fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool {
check(self.level.load(Relaxed))
}
#[inline(always)]
#[track_caller]
fn assert_level_matches(&self, level: LevelNo) {
assert_eq!(
self.level.load(Relaxed),
level,
"the level number does not match"
);
}

#[inline(always)]
fn children(&self) -> Self::ChildrenIter<'_> {
Expand Down
27 changes: 6 additions & 21 deletions crates/oxidd-manager-pointer/src/manager.rs
Original file line number Diff line number Diff line change
Expand Up @@ -674,10 +674,7 @@ where
let level_no = self.unique_table.len() as LevelNo;
assert!(level_no < LevelNo::MAX, "too many levels");
let node = f(level_no);
node.check_level(|l| {
assert_eq!(l, level_no, "node level does not match");
true
});
node.assert_level_matches(level_no);

let [e1, e2] = add_node(self.store(), node)?;

Expand All @@ -690,7 +687,7 @@ where
Ok(e2)
}

#[inline]
#[inline(always)]
fn level(&self, no: LevelNo) -> Self::LevelView<'_> {
LevelView {
store: self.store(),
Expand Down Expand Up @@ -1282,19 +1279,13 @@ where
0,
"can only insert untagged edges pointing to inner nodes"
);
unsafe { edge.inner_node_unchecked() }.check_level(|l| {
assert_eq!(l, self.level, "node level does not match");
true
});
unsafe { edge.inner_node_unchecked() }.assert_level_matches(self.level);
self.set.insert(edge)
}

#[inline(always)]
fn get_or_insert(&mut self, node: N) -> AllocResult<Edge<'id, N, ET, TAG_BITS>> {
node.check_level(|l| {
assert_eq!(l, self.level, "node level does not match");
true
});
node.assert_level_matches(self.level);
// No need to check if the children of `node` are stored in `self.store`
// due to lifetime restrictions.
LevelViewSet::get_or_insert(&mut *self.set, node, |node| add_node(self.store, node))
Expand Down Expand Up @@ -1399,19 +1390,13 @@ where
0,
"can only insert untagged edges pointing to inner nodes"
);
unsafe { edge.inner_node_unchecked() }.check_level(|l| {
assert_eq!(l, self.level, "node level does not match");
true
});
unsafe { edge.inner_node_unchecked() }.assert_level_matches(self.level);
self.set.insert(edge)
}

#[inline(always)]
fn get_or_insert(&mut self, node: N) -> AllocResult<Edge<'id, N, ET, TAG_BITS>> {
node.check_level(|l| {
assert_eq!(l, self.level, "node level does not match");
true
});
node.assert_level_matches(self.level);
// No need to check if the children of `node` are stored in `self.store`
// due to lifetime restrictions.
self.set
Expand Down
9 changes: 9 additions & 0 deletions crates/oxidd-manager-pointer/src/node/fixed_arity.rs
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,15 @@ impl<'id, ET: Tag, const TAG_BITS: u32, const ARITY: usize>
fn check_level(&self, check: impl FnOnce(LevelNo) -> bool) -> bool {
check(self.level.load(Relaxed))
}
#[inline(always)]
#[track_caller]
fn assert_level_matches(&self, level: LevelNo) {
assert_eq!(
self.level.load(Relaxed),
level,
"the level number does not match"
);
}

#[inline(always)]
fn children(&self) -> Self::ChildrenIter<'_> {
Expand Down
26 changes: 21 additions & 5 deletions crates/oxidd-rules-bdd/src/complement_edge/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -209,16 +209,32 @@ fn reduce<M>(
level: LevelNo,
t: M::Edge,
e: M::Edge,
_op: BCDDOp,
op: BCDDOp,
) -> AllocResult<M::Edge>
where
M: Manager<Terminal = BCDDTerminal, EdgeTag = EdgeTag>,
{
let tmp = <BCDDRules as DiagramRules<_, _, _>>::reduce(manager, level, [t, e]);
if let ReducedOrNew::Reduced(..) = &tmp {
stat!(reduced _op);
// We do not use `DiagramRules::reduce()` here, as the iterator is
// apparently not fully optimized away.
if t == e {
stat!(reduced op);
manager.drop_edge(e);
return Ok(t);
}
tmp.then_insert(manager, level)

let tt = t.tag();
let (node, tag) = if tt == EdgeTag::Complemented {
let et = e.tag();
let node = M::InnerNode::new(
level,
[t.with_tag_owned(EdgeTag::None), e.with_tag_owned(!et)],
);
(node, EdgeTag::Complemented)
} else {
(M::InnerNode::new(level, [t, e]), EdgeTag::None)
};

Ok(oxidd_core::LevelView::get_or_insert(&mut manager.level(level), node)?.with_tag_owned(tag))
}

// --- Terminal Type -----------------------------------------------------------
Expand Down
22 changes: 11 additions & 11 deletions crates/oxidd-rules-bdd/src/simple/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,21 +59,21 @@ impl<E: Edge, N: InnerNode<E>> DiagramRules<E, N, BDDTerminal> for BDDRules {

/// Apply the reduction rules, creating a node in `manager` if necessary
#[inline(always)]
fn reduce<M>(
manager: &M,
level: LevelNo,
t: M::Edge,
e: M::Edge,
_op: BDDOp,
) -> AllocResult<M::Edge>
fn reduce<M>(manager: &M, level: LevelNo, t: M::Edge, e: M::Edge, op: BDDOp) -> AllocResult<M::Edge>
where
M: Manager<Terminal = BDDTerminal>,
{
let tmp = <BDDRules as DiagramRules<_, _, _>>::reduce(manager, level, [t, e]);
if let ReducedOrNew::Reduced(..) = &tmp {
stat!(reduced _op);
// We do not use `DiagramRules::reduce()` here, as the iterator is
// apparently not fully optimized away.
if t == e {
stat!(reduced op);
manager.drop_edge(e);
return Ok(t);
}
tmp.then_insert(manager, level)
oxidd_core::LevelView::get_or_insert(
&mut manager.level(level),
M::InnerNode::new(level, [t, e]),
)
}

/// Collect the two children of a binary node
Expand Down
13 changes: 9 additions & 4 deletions crates/oxidd-rules-zbdd/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -71,12 +71,17 @@ fn reduce<M>(
where
M: Manager<Terminal = ZBDDTerminal>,
{
let _ = op;
let tmp = <ZBDDRules as DiagramRules<_, _, _>>::reduce(manager, level, [hi, lo]);
if let ReducedOrNew::Reduced(..) = &tmp {
// We do not use `DiagramRules::reduce()` here, as the iterator is
// apparently not fully optimized away.
if manager.get_node(&hi).is_terminal(&ZBDDTerminal::Empty) {
stat!(reduced op);
manager.drop_edge(hi);
return Ok(lo);
}
tmp.then_insert(manager, level)
oxidd_core::LevelView::get_or_insert(
&mut manager.level(level),
M::InnerNode::new(level, [hi, lo]),
)
}

#[inline(always)]
Expand Down
1 change: 1 addition & 0 deletions crates/oxidd-test-utils/src/edge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -326,6 +326,7 @@ impl InnerNode<DummyEdge> for DummyNode {
fn check_level(&self, _check: impl FnOnce(LevelNo) -> bool) -> bool {
true
}
fn assert_level_matches(&self, _level: LevelNo) {}

fn children(&self) -> Self::ChildrenIter<'_> {
std::iter::empty()
Expand Down
8 changes: 4 additions & 4 deletions crates/oxidd/tests/boolean_function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -709,10 +709,10 @@ impl<'a, B: BooleanFunction> TestAllBooleanFunctions<'a, B> {

let mut choice_requested = 0u32;
let cube = f.pick_cube([], |manager, edge, level| {
assert!(manager
manager
.get_node(edge)
.unwrap_inner()
.check_level(|l| l == level));
.assert_level_matches(level);
if choice_requested & (1 << level) != 0 {
panic!("choice requested twice for x{level}");
} else {
Expand All @@ -723,10 +723,10 @@ impl<'a, B: BooleanFunction> TestAllBooleanFunctions<'a, B> {
let mut choice_requested_sym = 0u32;
let dd_cube = f
.pick_cube_dd(|manager, edge, level| {
assert!(manager
manager
.get_node(edge)
.unwrap_inner()
.check_level(|l| l == level));
.assert_level_matches(level);
if choice_requested_sym & (1 << level) != 0 {
panic!("choice requested twice for x{level}");
} else {
Expand Down

0 comments on commit 8f0874b

Please sign in to comment.