From: Tim King Date: Fri, 14 Jul 2017 22:18:23 +0000 (-0700) Subject: Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap... X-Git-Tag: cvc5-1.0.0~5714 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f3b77bbd30be2388558000085d910d82e81d989;p=cvc5.git Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage. --- diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 86a7cb141..21e30cef6 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -58,7 +58,7 @@ ** its CDOhash_map object memory freed. Here, the CDOhash_map is restored ** to a "NULL-map" state (see above), signaling it to remove ** itself from the map completely and put itself on a "trash - ** list" for the map. + ** list" for its scope. ** ** Third, you might obliterate() the key. This calls the CDOhash_map ** destructor, which calls destroy(), which does a successive @@ -70,24 +70,18 @@ ** Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()). ** This first calls destroy(), as per ContextObj contract, but ** cdhashmapdoesn't save/restore itself, so that does nothing at the - ** CDHashMap-level. Then it empties the trash. Then, for each - ** element in the map, it marks it as being "part of a complete - ** map destruction", which essentially short-circuits + ** CDHashMap-level. Then, for each element in the map, it marks it as being + ** "part of a complete map destruction", which essentially short-circuits ** CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates - ** it. Finally it asserts that the trash is empty (which it - ** should be, since restore() was short-circuited). + ** it. ** ** Fifth, you might clear() the CDHashMap. This does exactly the ** same as CDHashMap::~CDHashMap(), except that it doesn't call destroy() ** on itself. ** - ** CDHashMap::emptyTrash() simply goes through and calls - ** ->deleteSelf() on all elements in the trash. ** ContextObj::deleteSelf() calls the CDOhash_map destructor, then ** frees the memory associated to the CDOhash_map. CDOhash_map::~CDOhash_map() - ** calls destroy(), which restores as much as possible. (Note, - ** though, that since objects placed on the trash have already - ** restored to the fullest extent possible, it does nothing.) + ** calls destroy(), which restores as much as possible. **/ #include "cvc4_private.h" @@ -157,7 +151,7 @@ class CDOhash_map : public ContextObj { } else { Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl; //this->deleteSelf(); - d_map->d_trash.push_back(this); + enqueueToGarbageCollect(); } } else { d_data = p->d_data; @@ -290,8 +284,6 @@ class CDHashMap : public ContextObj { Element* d_first; Context* d_context; - std::vector d_trash; - // Nothing to save; the elements take care of themselves virtual ContextObj* save(ContextMemoryManager* pCMM) { Unreachable(); @@ -302,75 +294,38 @@ class CDHashMap : public ContextObj { Unreachable(); } - void emptyTrash() { - //FIXME multithreading - for(typename std::vector::iterator i = d_trash.begin(); - i != d_trash.end(); - ++i) { - Debug("gc") << "emptyTrash(): " << *i << std::endl; - (*i)->deleteSelf(); - } - d_trash.clear(); - } - // no copy or assignment CDHashMap(const CDHashMap&) CVC4_UNDEFINED; CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED; public: - - CDHashMap(Context* context) : - ContextObj(context), - d_map(), - d_first(NULL), - d_context(context), - d_trash() { - } + CDHashMap(Context* context) + : ContextObj(context), d_map(), d_first(NULL), d_context(context) {} ~CDHashMap() { - Debug("gc") << "cdhashmap" << this - << " disappearing, destroying..." << std::endl; + Debug("gc") << "cdhashmap" << this << " disappearing, destroying..." + << std::endl; destroy(); - Debug("gc") << "cdhashmap" << this - << " disappearing, done destroying" << std::endl; - - Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl; - emptyTrash(); - Debug("gc") << "done emptying trash for " << this << std::endl; - - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { - // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); - } - } - d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); + Debug("gc") << "cdhashmap" << this << " disappearing, done destroying" + << std::endl; + clear(); } - void clear() throw(AssertionException) { - Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl; - emptyTrash(); + void clear() { + Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" + << std::endl; Debug("gc") << "done emptying trash for " << this << std::endl; - for(typename table_type::iterator i = d_map.begin(); - i != d_map.end(); - ++i) { + for (auto& key_element_pair : d_map) { // mark it as being a destruction (short-circuit restore()) - (*i).second->d_map = NULL; - if(!(*i).second->d_noTrash) { - (*i).second->deleteSelf(); + Element* element = key_element_pair.second; + element->d_map = nullptr; + if (!element->d_noTrash) { + element->deleteSelf(); } } d_map.clear(); - d_first = NULL; - - Assert(d_trash.empty()); + d_first = nullptr; } // The usual operators of map @@ -389,8 +344,6 @@ public: // If a key is not present, a new object is created and inserted Element& operator[](const Key& k) { - emptyTrash(); - typename table_type::iterator i = d_map.find(k); Element* obj; @@ -404,8 +357,6 @@ public: } bool insert(const Key& k, const Data& d) { - emptyTrash(); - typename table_type::iterator i = d_map.find(k); if(i == d_map.end()) {// create new object @@ -443,8 +394,6 @@ public: * insertAtContextLevelZero() a key that already is in the map. */ void insertAtContextLevelZero(const Key& k, const Data& d) { - emptyTrash(); - AlwaysAssert(d_map.find(k) == d_map.end()); Element* obj = new(true) Element(d_context, this, k, d, @@ -566,10 +515,6 @@ public: } } - iterator find(const Key& k) { - emptyTrash(); - return const_cast(this)->find(k); - } };/* class CDHashMap<> */ diff --git a/src/context/context.cpp b/src/context/context.cpp index 2b781b95c..66d6a6542 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) : d_pScope->addToChain(this); } +void ContextObj::enqueueToGarbageCollect() { + Assert(d_pScope != NULL); + d_pScope->enqueueToGarbageCollect(this); +} ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { if(preNotify) { @@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out, return out << " --> NULL"; } +Scope::~Scope() { + // Call restore() method on each ContextObj object in the list. + // Note that it is the responsibility of restore() to return the + // next item in the list. + while (d_pContextObjList != NULL) { + d_pContextObjList = d_pContextObjList->restoreAndContinue(); + } + + if (d_garbage) { + while (!d_garbage->empty()) { + ContextObj* obj = d_garbage->back(); + d_garbage->pop_back(); + obj->deleteSelf(); + } + } +} + +void Scope::enqueueToGarbageCollect(ContextObj* obj) { + if (!d_garbage) { + d_garbage.reset(new std::vector); + } + d_garbage->push_back(obj); +} } /* CVC4::context namespace */ } /* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 9b3f57a5d..92eb10441 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -19,12 +19,13 @@ #ifndef __CVC4__CONTEXT__CONTEXT_H #define __CVC4__CONTEXT__CONTEXT_H -#include #include #include -#include +#include +#include #include #include +#include #include "base/cvc4_assert.h" #include "base/output.h" @@ -257,6 +258,14 @@ class Scope { */ ContextObj* d_pContextObjList; + /** + * A list of ContextObj to be garbage collected before the destruction of this + * scope. deleteSelf() will be called on each element during ~Scope(). + * + * This is either nullptr or list owned by this scope. + */ + std::unique_ptr> d_garbage; + friend std::ostream& operator<<(std::ostream&, const Scope&) throw(AssertionException); @@ -266,54 +275,60 @@ public: * Constructor: Create a new Scope; set the level and the previous Scope * if any. */ - Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() : - d_pContext(pContext), - d_pCMM(pCMM), - d_level(level), - d_pContextObjList(NULL) { + Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() + : d_pContext(pContext), + d_pCMM(pCMM), + d_level(level), + d_pContextObjList(nullptr), + d_garbage() {} + + /** + * Destructor: Clears out all of the garbage and restore all of the objects + * in ContextObjList. + */ + ~Scope(); + + /** + * Get the Context for this Scope + */ + Context* getContext() const throw() { return d_pContext; } + + /** + * Get the ContextMemoryManager for this Scope + */ + ContextMemoryManager* getCMM() const throw() { return d_pCMM; } + + /** + * Get the level of the current Scope + */ + int getLevel() const throw() { return d_level; } + + /** + * Return true iff this Scope is the current top Scope + */ + bool isCurrent() const throw() { return this == d_pContext->getTopScope(); } + + /** + * When a ContextObj object is modified for the first time in this + * Scope, it should call this method to add itself to the list of + * objects that will need to be restored. Defined inline below. + */ + void addToChain(ContextObj* pContextObj) throw(AssertionException); + + /** + * Overload operator new for use with ContextMemoryManager to allow + * creation of new Scope objects in the current memory region. + */ + static void* operator new(size_t size, ContextMemoryManager* pCMM) { + Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl; + return pCMM->newData(size); } /** - * Destructor: Restore all of the objects in ContextObjList. Defined inline - * below. - */ - ~Scope(); - - /** - * Get the Context for this Scope - */ - Context* getContext() const throw() { return d_pContext; } - - /** - * Get the ContextMemoryManager for this Scope + * Enqueues a ContextObj to be garbage collected via a call to deleteSelf() + * during the destruction of this scope. */ - ContextMemoryManager* getCMM() const throw() { return d_pCMM; } - - /** - * Get the level of the current Scope - */ - int getLevel() const throw() { return d_level; } - - /** - * Return true iff this Scope is the current top Scope - */ - bool isCurrent() const throw() { return this == d_pContext->getTopScope(); } - - /** - * When a ContextObj object is modified for the first time in this - * Scope, it should call this method to add itself to the list of - * objects that will need to be restored. Defined inline below. - */ - void addToChain(ContextObj* pContextObj) throw(AssertionException); - - /** - * Overload operator new for use with ContextMemoryManager to allow - * creation of new Scope objects in the current memory region. - */ - static void* operator new(size_t size, ContextMemoryManager* pCMM) { - Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl; - return pCMM->newData(size); - } + void enqueueToGarbageCollect(ContextObj* obj); /** * Overload operator delete for Scope objects allocated using @@ -647,6 +662,12 @@ public: ::operator delete(this); } + /** + * Use this to enqueue calling deleteSelf() at the time of the destruction of + * the enclosing Scope. + */ + void enqueueToGarbageCollect(); + };/* class ContextObj */ /** @@ -725,15 +746,6 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) { update(); } -inline Scope::~Scope() { - // Call restore() method on each ContextObj object in the list. - // Note that it is the responsibility of restore() to return the - // next item in the list. - while(d_pContextObjList != NULL) { - d_pContextObjList = d_pContextObjList->restoreAndContinue(); - } -} - inline void Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) { if(d_pContextObjList != NULL) {