memory_manager_context.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file memory_manager_context.h
00004  *\brief Stack-based memory manager
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Aug  3 21:39:07 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  *
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 #ifndef _cvc3__include__memory_manager_context_h
00022 #define _cvc3__include__memory_manager_context_h
00023 
00024 #include <cstdlib>
00025 #include <vector>
00026 #include "memory_manager.h"
00027 
00028 namespace CVC3 {
00029 
00030   const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
00031 
00032 /*****************************************************************************/
00033 /*!
00034  *\class ContextMemoryManager
00035  *\brief ContextMemoryManager
00036  *
00037  * Author: Clark Barrett
00038  *
00039  * Created: Thu Aug  3 16:41:35 2006
00040  *
00041  * Stack-based memory manager
00042  */
00043 /*****************************************************************************/
00044 class ContextMemoryManager :public MemoryManager {
00045   static std::vector<char*> s_freePages;
00046   std::vector<char*> d_chunkList; // Pointers to the beginning of each chunk
00047 
00048   // Pointers to the next free block of memory in the current chunk
00049   char* d_nextFree;
00050   // Pointer to end of current chunk (1 byte off the end)
00051   char* d_endChunk;
00052   // Index into chunk vector
00053   unsigned d_indexChunkList;
00054 
00055   // Stack of pointers to the next free block of memory in the current chunk
00056   std::vector<char*> d_nextFreeStack;
00057   // Stack of pointers to end of current chunk (1 byte off the end)
00058   std::vector<char*> d_endChunkStack;
00059   // Stack of indices into chunk vector
00060   std::vector<unsigned> d_indexChunkListStack;
00061 
00062   // Private methods
00063   void newChunk() { // Allocate new chunk
00064     DebugAssert(d_chunkList.size() > 0, "expected unempty list");
00065     ++d_indexChunkList;
00066     DebugAssert(d_chunkList.size() == d_indexChunkList, "invariant violated");
00067     if (s_freePages.empty()) {
00068       d_chunkList.push_back((char*)malloc(chunkSizeBytes));
00069     }
00070     else {
00071       d_chunkList.push_back(s_freePages.back());
00072       s_freePages.pop_back();
00073     }
00074     d_nextFree = d_chunkList.back();
00075     FatalAssert(d_nextFree != NULL, "Out of memory");
00076     d_endChunk = d_nextFree + chunkSizeBytes;
00077   }
00078 
00079  public:
00080   // Constructor
00081   ContextMemoryManager()
00082     : d_indexChunkList(0)
00083   {
00084     if (s_freePages.empty()) {
00085       d_chunkList.push_back((char*)malloc(chunkSizeBytes));
00086     }
00087     else {
00088       d_chunkList.push_back(s_freePages.back());
00089       s_freePages.pop_back();
00090     }      
00091     d_nextFree = d_chunkList.back();
00092     FatalAssert(d_nextFree != NULL, "Out of memory");
00093     d_endChunk = d_nextFree + chunkSizeBytes;
00094   }
00095 
00096   // Destructor
00097   ~ContextMemoryManager() {
00098     while(!d_chunkList.empty()) {
00099       s_freePages.push_back(d_chunkList.back());
00100       d_chunkList.pop_back();
00101     }
00102   }
00103 
00104   void* newData(size_t size) {
00105     void* res = (void*)d_nextFree;
00106     d_nextFree += size;
00107     if (d_nextFree > d_endChunk) {
00108       newChunk();
00109       res = (void*)d_nextFree;
00110       d_nextFree += size;
00111       DebugAssert(d_nextFree <= d_endChunk, "chunk not big enough");
00112     }
00113     return res;
00114   }
00115 
00116   void deleteData(void* d) { }
00117 
00118   void push() {
00119     d_nextFreeStack.push_back(d_nextFree);
00120     d_endChunkStack.push_back(d_endChunk);
00121     d_indexChunkListStack.push_back(d_indexChunkList);
00122   }
00123 
00124   void pop() {
00125     d_nextFree = d_nextFreeStack.back();
00126     d_nextFreeStack.pop_back();
00127     d_endChunk = d_endChunkStack.back();
00128     d_endChunkStack.pop_back();
00129     while (d_indexChunkList > d_indexChunkListStack.back()) {
00130       s_freePages.push_back(d_chunkList.back());
00131       d_chunkList.pop_back();
00132       --d_indexChunkList;
00133     }
00134     d_indexChunkListStack.pop_back();
00135   }
00136 
00137   static void garbageCollect(void) {
00138     while (!s_freePages.empty()) {
00139       free(s_freePages.back());
00140       s_freePages.pop_back();
00141     }
00142   }
00143 
00144   unsigned getMemory(int verbosity) {
00145     unsigned long memSelf = sizeof(ContextMemoryManager);
00146     unsigned long mem = 0;
00147 
00148     mem += MemoryTracker::getVec(verbosity - 1, d_chunkList);
00149     mem += MemoryTracker::getVec(verbosity - 1, d_nextFreeStack);
00150     mem += MemoryTracker::getVec(verbosity - 1, d_endChunkStack);
00151     mem += MemoryTracker::getVec(verbosity - 1, d_indexChunkListStack);
00152 
00153     mem += d_chunkList.size() * chunkSizeBytes;
00154 
00155     MemoryTracker::print("ContextMemoryManager", verbosity, memSelf, mem);
00156 
00157     return mem + memSelf;
00158   }
00159 
00160   static unsigned getStaticMemory(int verbosity) {
00161     unsigned mem = 0;
00162     mem += MemoryTracker::getVec(verbosity - 1, s_freePages);
00163     mem += s_freePages.size() * chunkSizeBytes;
00164     MemoryTracker::print("ContextMemoryManager Static", verbosity, 0, mem);
00165     return mem;
00166   }
00167 
00168 }; // end of class ContextMemoryManager
00169 
00170 }
00171 
00172 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2