diff options
author | Tim King <taking@cs.nyu.edu> | 2016-11-11 16:44:19 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-11-11 16:44:19 -0800 |
commit | 51beecbceb28f30004bda32e0babf201bd1f94d6 (patch) | |
tree | ecec23fbc94566a7edefce8861f923dad59a1e9e /src | |
parent | 95ec94bd66d5b37e5e33f32024e400dd37ddd863 (diff) | |
parent | 0c65c780c6c7c52c26edf6ec0b8f45ef9fb496cf (diff) |
Merge pull request #105 from timothy-king/delete-maxed-out
Adding garbage collection of nodes with maxed out reference counts.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_manager.cpp | 71 | ||||
-rw-r--r-- | src/expr/node_manager.h | 61 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 18 | ||||
-rw-r--r-- | src/expr/node_value.h | 30 |
4 files changed, 147 insertions, 33 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) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index aaffeb322..d85ff23d5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -58,20 +58,24 @@ namespace expr { * to NodeManager events via NodeManager::subscribeEvents(this). */ class NodeManagerListener { -public: - virtual ~NodeManagerListener() { } - virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { } - virtual void nmNotifyNewSortConstructor(TypeNode tn) { } - virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { } - virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { } - virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } - virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } + public: + virtual ~NodeManagerListener() {} + virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {} + virtual void nmNotifyNewSortConstructor(TypeNode tn) {} + virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, + uint32_t flags) {} + virtual void nmNotifyNewDatatypes( + const std::vector<DatatypeType>& datatypes) {} + virtual void nmNotifyNewVar(TNode n, uint32_t flags) {} + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, + uint32_t flags) {} /** - * Notify a listener of a Node that's being GCed. If this function stores a reference + * Notify a listener of a Node that's being GCed. If this function stores a + * reference * to the Node somewhere, very bad things will happen. */ - virtual void nmNotifyDeleteNode(TNode n) { } -};/* class NodeManagerListener */ + virtual void nmNotifyDeleteNode(TNode n) {} +}; /* class NodeManagerListener */ class NodeManager { template <unsigned nchild_thresh> friend class CVC4::NodeBuilder; @@ -96,7 +100,7 @@ class NodeManager { expr::NodeValuePoolEq> NodeValuePool; typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueIDHashFunction, - expr::NodeValueIDEquality> ZombieSet; + expr::NodeValueIDEquality> NodeValueIDSet; static CVC4_THREADLOCAL(NodeManager*) s_current; @@ -146,7 +150,13 @@ class NodeManager { * we might like to delete nodes in least-recently-used order. But * we also need to avoid processing a zombie twice. */ - ZombieSet d_zombies; + NodeValueIDSet d_zombies; + + /** + * NodeValues with maxed out reference counts. These live as long as the + * NodeManager. They have a custom deallocation procedure at the very end. + */ + std::vector<expr::NodeValue*> d_maxedOut; /** * A set of operator singletons (w.r.t. to this NodeManager @@ -157,7 +167,7 @@ class NodeManager { * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back. */ Node d_operators[kind::LAST_KIND]; - + /** unique vars per (Kind,Type) */ std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; @@ -165,7 +175,7 @@ class NodeManager { * A list of subscribers for NodeManager events. */ std::vector<NodeManagerListener*> d_listeners; - + /** A list of datatypes owned by this node manager. */ std::vector<Datatype*> d_ownedDatatypes; @@ -278,6 +288,19 @@ class NodeManager { } /** + * Register a NodeValue as having a maxed out reference count. This NodeValue + * will live as long as its containing NodeManager. + */ + inline void markRefCountMaxedOut(expr::NodeValue* nv) { + Assert(nv->HasMaximizedReferenceCount()); + if(Debug.isOn("gc")) { + Debug("gc") << "marking node value " << nv + << " [" << nv->d_id << "]: as maxed out" << std::endl; + } + d_maxedOut.push_back(nv); + } + + /** * Reclaim all zombies. */ void reclaimZombies(); @@ -288,6 +311,14 @@ class NodeManager { bool safeToReclaimZombies() const; /** + * Returns a reverse topological sort of a list of NodeValues. The NodeValues + * must be valid and have ids. The NodeValues are not modified (including ref + * counts). + */ + static std::vector<expr::NodeValue*> TopologicalSort( + const std::vector<expr::NodeValue*>& roots); + + /** * This template gives a mechanism to stack-allocate a NodeValue * with enough space for N children (where N is a compile-time * constant). You use it like this: diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index a40075ca9..40649ef2c 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -37,7 +37,8 @@ namespace expr { string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage(); + OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO + : options::outputLanguage(); toStream(ss, -1, false, false, outlang); return ss.str(); } @@ -49,7 +50,8 @@ void NodeValue::toStream(std::ostream& out, int toDepth, bool types, size_t dag, // count, even just for printing. RefCountGuard guard(this); - Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, dag); + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, + dag); } void NodeValue::printAst(std::ostream& out, int ind) const { @@ -58,14 +60,14 @@ void NodeValue::printAst(std::ostream& out, int ind) const { indent(out, ind); out << '('; out << getKind(); - if(getMetaKind() == kind::metakind::VARIABLE) { + if (getMetaKind() == kind::metakind::VARIABLE) { out << ' ' << getId(); - } else if(getMetaKind() == kind::metakind::CONSTANT) { + } else if (getMetaKind() == kind::metakind::CONSTANT) { out << ' '; kind::metakind::NodeValueConstPrinter::toStream(out, this); } else { - if(nv_begin() != nv_end()) { - for(const_nv_iterator child = nv_begin(); child != nv_end(); ++child) { + if (nv_begin() != nv_end()) { + for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child) { out << std::endl; (*child)->printAst(out, ind + 1); } @@ -76,5 +78,5 @@ void NodeValue::printAst(std::ostream& out, int ind) const { out << ')'; } -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ +} /* CVC4::expr namespace */ +} /* CVC4 namespace */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index b403d0c86..79ce8cb4f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -122,6 +122,9 @@ class NodeValue { void inc(); void dec(); + // Returns true if the reference count is maximized. + inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; } + /** * Uninitializing constructor for NodeBuilder's use. */ @@ -294,14 +297,21 @@ public: private: + /** + * RAII guard that increases the reference count if the reference count to be + * > 0. Otherwise, this does nothing. This does not just increment the + * reference count to avoid maxing out the d_rc field. This is only for low + * level functions. + */ class RefCountGuard { NodeValue* d_nv; + bool d_increased; public: RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv)) { - // inc() - if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) { - ++d_nv->d_rc; + d_increased = (d_nv->d_rc == 0); + if(d_increased) { + d_nv->d_rc = 1; } } ~RefCountGuard() { @@ -310,7 +320,7 @@ private: // E.g., this can happen when debugging code calls the print // routines below. As RefCountGuards are scoped on the stack, // this should be fine---but not in multithreaded contexts! - if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) { + if(d_increased) { --d_nv->d_rc; } } @@ -413,8 +423,15 @@ inline void NodeValue::inc() { "NodeValue is currently being deleted " "and increment is being called on it. Don't Do That!"); // FIXME multithreading - if(__builtin_expect( ( d_rc < MAX_RC ), true )) { + if (__builtin_expect((d_rc < MAX_RC - 1), true)) { + ++d_rc; + } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) { ++d_rc; + Assert(NodeManager::currentNM() != NULL, + "No current NodeManager on incrementing of NodeValue: " + "maybe a public CVC4 interface function is missing a " + "NodeManagerScope ?"); + NodeManager::currentNM()->markRefCountMaxedOut(this); } } @@ -425,7 +442,8 @@ inline void NodeValue::dec() { if(__builtin_expect( ( d_rc == 0 ), false )) { Assert(NodeManager::currentNM() != NULL, "No current NodeManager on destruction of NodeValue: " - "maybe a public CVC4 interface function is missing a NodeManagerScope ?"); + "maybe a public CVC4 interface function is missing a " + "NodeManagerScope ?"); NodeManager::currentNM()->markForDeletion(this); } } |