diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-02 20:56:55 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-02 20:56:55 +0000 |
commit | 1a558a30bec496444742ed75c0a6973d9789daf7 (patch) | |
tree | 81d5f4aedc3a320c4b95945c71a1e3cf0d8e88af /src/context/cdchunk_list.h | |
parent | f9d3552033d8214c833b58ed54d99c836de4ce37 (diff) |
- Merged in the branch cdlist-cleanup.
- This adds a CleanUp template argument to CDList.
- CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator.
- CDVector<T> has been simplified and improved.
- The expected performance impact is negligible.
Diffstat (limited to 'src/context/cdchunk_list.h')
-rw-r--r-- | src/context/cdchunk_list.h | 496 |
1 files changed, 496 insertions, 0 deletions
diff --git a/src/context/cdchunk_list.h b/src/context/cdchunk_list.h new file mode 100644 index 000000000..e18d9b972 --- /dev/null +++ b/src/context/cdchunk_list.h @@ -0,0 +1,496 @@ +/********************* */ +/*! \file cdchunk_list.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Context-dependent list class designed for use with a + ** context memory allocator. + ** + ** Context-dependent list class designed for use with a context + ** memory allocator. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDCHUNK_LIST_H +#define __CVC4__CONTEXT__CDCHUNK_LIST_H + +#include <iterator> +#include <memory> + +#include "context/context.h" +#include "context/context_mm.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * Generic context-dependent dynamic array. Like the usual CDList<>, + * but allocates all memory from context memory. Elements are kept in + * cascading "list segments." Access to elements by operator[] is not O(1) but + * O(log n). As with CDList<>, update is not permitted, only + * appending to the end of the list. + */ +template <class T> +class CDChunkList : public ContextObj { +public: + + /** The value type with which this CDChunkList<> was instantiated. */ + typedef T value_type; + /** The allocator type with which this CDChunkList<> was instantiated. */ + typedef ContextMemoryAllocator<T> Allocator; + +protected: + + static const size_t INITIAL_SEGMENT_SIZE = 10; + static const size_t INCREMENTAL_GROWTH_FACTOR = 2; + + /** + * ListSegment is itself allocated in Context memory, but it is + * never updated; it serves as information about the d_list segment + * pointer it contains only. + */ + class ListSegment { + ListSegment* d_nextSegment; + size_t d_segmentSize; + T* d_list; + public: + ListSegment() : + d_nextSegment(NULL), + d_segmentSize(0), + d_list(NULL) { + } + void initialize(T* list) { + Assert( d_nextSegment == NULL && + d_segmentSize == 0 && + d_list == NULL, + "Double-initialization of ListSegment not permitted" ); + d_list = list; + } + void linkTo(ListSegment* nextSegment) { + Assert( d_nextSegment == NULL, + "Double-linking of ListSegment not permitted" ); + d_nextSegment = nextSegment; + } + void cutLink() { + d_nextSegment = NULL; + } + ListSegment* getNextSegment() const { return d_nextSegment; } + size_t& size() { return d_segmentSize; } + size_t size() const { return d_segmentSize; } + const T* list() const { return d_list; } + T& operator[](size_t i) { return d_list[i]; } + const T& operator[](size_t i) const { return d_list[i]; } + };/* struct CDChunkList<T>::ListSegment */ + + /** + * The first segment of list memory. + */ + ListSegment d_headSegment; + + /** + * A pointer to the final segment of list memory. + */ + ListSegment* d_tailSegment; + + /** + * Whether to call the destructor when items are popped from the + * list. True by default, but can be set to false by setting the + * second argument in the constructor to false. + */ + bool d_callDestructor; + + /** + * Number of objects in list across all segments. + */ + size_t d_size; + + /** + * Total allocated size across all segments. + */ + size_t d_totalSizeAlloc; + + /** + * Our allocator. + */ + Allocator d_allocator; + + /** + * Lightweight save object for CDChunkList<T, ContextMemoryAllocator<T> >. + */ + struct CDChunkListSave : public ContextObj { + ListSegment* d_tail; + size_t d_tailSize, d_size, d_sizeAlloc; + CDChunkListSave(const CDChunkList<T>& list, ListSegment* tail, + size_t size, size_t sizeAlloc) : + ContextObj(list), + d_tail(tail), + d_tailSize(tail->size()), + d_size(size), + d_sizeAlloc(sizeAlloc) { + } + ~CDChunkListSave() { + this->destroy(); + } + ContextObj* save(ContextMemoryManager* pCMM) { + // This type of object _is_ the save/restore object. It isn't + // itself saved or restored. + Unreachable(); + } + void restore(ContextObj* data) { + // This type of object _is_ the save/restore object. It isn't + // itself saved or restored. + Unreachable(); + } + };/* struct CDChunkList<T>::CDChunkListSave */ + + /** + * Private copy constructor undefined (no copy permitted). + */ + CDChunkList(const CDChunkList<T>& l) CVC4_UNDEFINED; + + /** + * Allocate the first list segment. + */ + void allocateHeadSegment() { + Assert(d_headSegment.list() == NULL); + Assert(d_totalSizeAlloc == 0 && d_size == 0); + + // Allocate an initial list if one does not yet exist + size_t newSize = INITIAL_SEGMENT_SIZE; + Debug("cdlist:cmm") << "initial grow of cdlist " << this + << " level " << getContext()->getLevel() + << " to " << newSize << std::endl; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + } + T* newList = d_allocator.allocate(newSize); + if(newList == NULL) { + throw std::bad_alloc(); + } + d_totalSizeAlloc = newSize; + d_headSegment.initialize(newList); + } + + /** + * Allocate a new segment with more space. + * Throws bad_alloc if memory allocation fails. + */ + void grow() { + Assert(d_totalSizeAlloc == d_size); + + // Allocate a new segment + typedef typename Allocator::template rebind<ListSegment>::other + SegmentAllocator; + ContextMemoryManager* cmm = d_allocator.getCMM(); + SegmentAllocator segAllocator = SegmentAllocator(cmm); + ListSegment* newSegment = segAllocator.allocate(1); + if(newSegment == NULL) { + throw std::bad_alloc(); + } + segAllocator.construct(newSegment, ListSegment()); + size_t newSize = INCREMENTAL_GROWTH_FACTOR * d_totalSizeAlloc; + if(newSize > d_allocator.max_size()) { + newSize = d_allocator.max_size(); + } + T* newList = d_allocator.allocate(newSize); + Debug("cdlist:cmm") << "new segment of cdlistcontext " << this + << " level " << getContext()->getLevel() + << " to " << newSize + << " (from " << d_tailSegment->list() + << " to " << newList << ")" << std::endl; + if(newList == NULL) { + throw std::bad_alloc(); + } + d_tailSegment->linkTo(newSegment); + d_tailSegment = newSegment; + d_tailSegment->initialize(newList); + d_totalSizeAlloc += newSize; + } + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current size to a copy using the copy constructor (the pointer and the + * allocated size are *not* copied as they are not restored on a pop). + * The saved information is allocated using the ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + ContextObj* data = new(pCMM) CDChunkListSave(*this, d_tailSegment, + d_size, d_totalSizeAlloc); + Debug("cdlist:cmm") << "save " << this + << " at level " << this->getContext()->getLevel() + << " size at " << this->d_size + << " totalSizeAlloc at " << this->d_totalSizeAlloc + << " data:" << data << std::endl; + return data; + } + + /** + * Implementation of mandatory ContextObj method restore: simply restores the + * previous size. Note that the list pointer and the allocated size are not + * changed. + */ + void restore(ContextObj* data) { + CDChunkListSave* save = static_cast<CDChunkListSave*>(data); + Debug("cdlist:cmm") << "restore " << this + << " level " << this->getContext()->getLevel() + << " data == " << data + << " call dtor == " << this->d_callDestructor + << " d_tail == " << this->d_tailSegment << std::endl; + if(this->d_callDestructor) { + ListSegment* seg = &d_headSegment; + size_t i = save->d_size; + while(i >= seg->size()) { + i -= seg->size(); + seg = seg->getNextSegment(); + } + do { + while(i < seg->size()) { + this->d_allocator.destroy(&(*seg)[i++]); + } + i = 0; + } while((seg = seg->getNextSegment()) != NULL); + } + + this->d_size = save->d_size; + this->d_tailSegment = save->d_tail; + this->d_tailSegment->size() = save->d_tailSize; + this->d_tailSegment->cutLink(); + this->d_totalSizeAlloc = save->d_sizeAlloc; + Debug("cdlist:cmm") << "restore " << this + << " level " << this->getContext()->getLevel() + << " size back to " << this->d_size + << " totalSizeAlloc at " << this->d_totalSizeAlloc + << std::endl; + } + +public: + + CDChunkList(Context* context, bool callDestructor, const Allocator& alloc) : + ContextObj(context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(alloc) { + allocateHeadSegment(); + } + + CDChunkList(Context* context, bool callDestructor = true) : + ContextObj(context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(Allocator(context->getCMM())) { + allocateHeadSegment(); + } + + CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor, + const Allocator& alloc) : + ContextObj(allocatedInCMM, context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(alloc) { + allocateHeadSegment(); + } + + CDChunkList(bool allocatedInCMM, Context* context, bool callDestructor = true) : + ContextObj(allocatedInCMM, context), + d_headSegment(), + d_tailSegment(&d_headSegment), + d_callDestructor(callDestructor), + d_size(0), + d_totalSizeAlloc(0), + d_allocator(Allocator(context->getCMM())) { + allocateHeadSegment(); + } + + /** + * Destructor: delete the list + */ + ~CDChunkList() throw(AssertionException) { + this->destroy(); + + if(this->d_callDestructor) { + for(ListSegment* segment = &d_headSegment; + segment != NULL; + segment = segment->getNextSegment()) { + for(size_t i = 0; i < segment->size(); ++i) { + this->d_allocator.destroy(&(*segment)[i]); + } + } + } + } + + /** + * Return the current size of (i.e. valid number of objects in) the + * list. + */ + size_t size() const { + return d_size; + } + + /** + * Return true iff there are no valid objects in the list. + */ + bool empty() const { + return d_size == 0; + } + + /** + * Add an item to the end of the list. + */ + void push_back(const T& data) { + Debug("cdlist:cmm") << "push_back " << this + << " level " << getContext()->getLevel() + << ": make-current, " + << "d_list == " << d_tailSegment->list() << std::endl; + makeCurrent(); + + Debug("cdlist:cmm") << "push_back " << this + << " level " << getContext()->getLevel() + << ": grow? " << d_size + << " size_alloc " << d_totalSizeAlloc + << std::endl; + + if(d_size == d_totalSizeAlloc) { + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": grow!\n"; + grow(); + } + Assert(d_size < d_totalSizeAlloc); + + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": construct! at [" << d_size << "] == " + << &(*d_tailSegment)[d_tailSegment->size()] + << std::endl; + d_allocator.construct(&(*d_tailSegment)[d_tailSegment->size()], data); + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": done..." << std::endl; + ++d_tailSegment->size(); + ++d_size; + Debug("cdlist:cmm") << "push_back " << this + << " " << getContext()->getLevel() + << ": size now " << d_size << std::endl; + } + + /** + * Access to the ith item in the list in O(log n). + */ + const T& operator[](size_t i) const { + Assert(i < d_size, "index out of bounds in CDChunkList::operator[]"); + const ListSegment* seg = &d_headSegment; + while(i >= seg->size()) { + i -= seg->size(); + seg = seg->getNextSegment(); + } + return (*seg)[i]; + } + + /** + * Returns the most recent item added to the list. + */ + const T& back() const { + Assert(d_size > 0, "CDChunkList::back() called on empty list"); + return (*d_tailSegment)[d_tailSegment->size() - 1]; + } + + /** + * Iterator for CDChunkList class. It has to be const because we don't + * allow items in the list to be changed. It's a straightforward + * wrapper around a pointer. Note that for efficiency, we implement + * only prefix increment and decrement. Also note that it's OK to + * create an iterator from an empty, uninitialized list, as begin() + * and end() will have the same value (NULL). + */ + class const_iterator { + const ListSegment* d_segment; + size_t d_index; + + const_iterator(const ListSegment* segment, size_t i) : + d_segment(segment), + d_index(i) { + } + + friend class CDChunkList<T>; + + public: + + typedef std::input_iterator_tag iterator_category; + typedef T value_type; + typedef std::ptrdiff_t difference_type; + typedef const T* pointer; + typedef const T& reference; + + const_iterator() : d_segment(NULL), d_index(0) {} + + inline bool operator==(const const_iterator& i) const { + return d_segment == i.d_segment && d_index == i.d_index; + } + + inline bool operator!=(const const_iterator& i) const { + return !(*this == i); + } + + inline const T& operator*() const { + return (*d_segment)[d_index]; + } + + /** Prefix increment */ + const_iterator& operator++() { + if(++d_index >= d_segment->size()) { + d_segment = d_segment->getNextSegment(); + d_index = 0; + } + return *this; + } + + /** Postfix increment: returns new iterator with the old value. */ + const_iterator operator++(int) { + const_iterator i = *this; + ++(*this); + return i; + } + };/* class CDChunkList<>::const_iterator */ + + /** + * Returns an iterator pointing to the first item in the list. + */ + const_iterator begin() const { + // This looks curious, but we have to make sure that begin() == end() + // for an empty list, and begin() == (head,0) for a nonempty one. + // Since the segment spill-over is implemented in + // iterator::operator++(), let's reuse it. */ + return ++const_iterator(&d_headSegment, -1); + } + + /** + * Returns an iterator pointing one past the last item in the list. + */ + const_iterator end() const { + return const_iterator(NULL, 0); + } +};/* class CDChunkList<T, ContextMemoryAllocator<T> > */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDCHUNK_LIST_H */ |