diff options
author | Tim King <taking@google.com> | 2016-11-10 15:22:49 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-10 15:22:49 -0800 |
commit | 16e809f698060645812667925b3e0c4d403ee71a (patch) | |
tree | 6952e767825c1d99166e1308c39aece2cc9c33c9 /src/expr/node_manager.cpp | |
parent | 13be3be39454a3cf7b05c4399a53bd2dd27996f6 (diff) |
Adding garbage collection of nodes with maxed out reference counts.
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 71 |
1 files changed, 67 insertions, 4 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index b07af0c14..1d54d0f9d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -42,6 +42,8 @@ namespace CVC4 { CVC4_THREADLOCAL(NodeManager*) NodeManager::s_current = NULL; +namespace { + /** * This class sets it reference argument to true and ensures that it gets set * to false on destruction. This can be used to make sure a flag gets toggled @@ -82,6 +84,9 @@ struct NVReclaim { } }; +} // namespace + + NodeManager::NodeManager(ExprManager* exprManager) : d_options(new Options()), d_statisticsRegistry(new StatisticsRegistry()), @@ -169,7 +174,7 @@ NodeManager::~NodeManager() { for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) { d_operators[i] = Node::null(); } - + d_unique_vars.clear(); TypeNode dummy; @@ -178,7 +183,9 @@ NodeManager::~NodeManager() { d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; - for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(), datatype_end = d_ownedDatatypes.end(); + for (std::vector<Datatype*>::iterator + datatype_iter = d_ownedDatatypes.begin(), + datatype_end = d_ownedDatatypes.end(); datatype_iter != datatype_end; ++datatype_iter) { Datatype* datatype = *datatype_iter; delete datatype; @@ -186,8 +193,25 @@ NodeManager::~NodeManager() { d_ownedDatatypes.clear(); Assert(!d_attrManager->inGarbageCollection() ); - while(!d_zombies.empty()) { - reclaimZombies(); + + std::vector<NodeValue*> order = TopologicalSort(d_maxedOut); + d_maxedOut.clear(); + + while (!d_zombies.empty() || !order.empty()) { + if (d_zombies.empty()) { + // Delete the maxed out nodes in toplogical order once we know + // there are no additional zombies, or other nodes to worry about. + Assert(!order.empty()); + // We process these in reverse to reverse the topological order. + NodeValue* greatest_maxed_out = order.back(); + order.pop_back(); + Assert(greatest_maxed_out->HasMaximizedReferenceCount()); + Debug("gc") << "Force zombify " << greatest_maxed_out << std::endl; + greatest_maxed_out->d_rc = 0; + markForDeletion(greatest_maxed_out); + } else { + reclaimZombies(); + } } poolRemove( &expr::NodeValue::null() ); @@ -333,6 +357,45 @@ void NodeManager::reclaimZombies() { } }/* NodeManager::reclaimZombies() */ +std::vector<NodeValue*> NodeManager::TopologicalSort( + const std::vector<NodeValue*>& roots) { + std::vector<NodeValue*> order; + std::vector<std::pair<bool, NodeValue*> > stack; + NodeValueIDSet visited; + const NodeValueIDSet root_set(roots.begin(), roots.end()); + + for (size_t index = 0; index < roots.size(); index++) { + NodeValue* root = roots[index]; + if (visited.find(root) == visited.end()) { + stack.push_back(std::make_pair(false, root)); + } + while (!stack.empty()) { + NodeValue* current = stack.back().second; + const bool visited_children = stack.back().first; + Debug("gc") << "Topological sort " << current << " " << visited_children + << std::endl; + if (visited_children) { + if (root_set.find(current) != root_set.end()) { + order.push_back(current); + } + stack.pop_back(); + } else { + stack.back().first = true; + Assert(visited.count(current) == 0); + visited.insert(current); + for (int i = 0; i < current->getNumChildren(); ++i) { + expr::NodeValue* child = current->getChild(i); + if (visited.find(child) == visited.end()) { + stack.push_back(std::make_pair(false, child)); + } + } + } + } + } + Assert(order.size() == roots.size()); + return order; +} /* NodeManager::TopologicalSort() */ + TypeNode NodeManager::getType(TNode n, bool check) throw(TypeCheckingExceptionPrivate, AssertionException) { |