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 <vector>
00025 #include "memory_manager.h"
00026 
00027 namespace CVC3 {
00028 
00029 /*****************************************************************************/
00030 /*!
00031  *\class ContextMemoryManager
00032  *\brief ContextMemoryManager
00033  *
00034  * Author: Clark Barrett
00035  *
00036  * Created: Thu Aug  3 16:41:35 2006
00037  *
00038  * Stack-based memory manager
00039  */
00040 /*****************************************************************************/
00041 class ContextMemoryManager :public MemoryManager {
00042   private:
00043   unsigned d_chunkSizeBytes; // #bytes in each chunk
00044 
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(d_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 + d_chunkSizeBytes;
00077   }
00078 
00079  public:
00080   // Constructor
00081   ContextMemoryManager(unsigned chunkSize = 16384)
00082     : d_chunkSizeBytes(chunkSize), d_indexChunkList(0)
00083   {
00084     if (s_freePages.empty()) {
00085       d_chunkList.push_back((char*)malloc(d_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 + d_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() {
00145     return d_chunkList.size() * d_chunkSizeBytes;
00146   }
00147 
00148   static unsigned getStaticMemory() {
00149     return s_freePages.size() * 16384;
00150   }
00151 
00152 }; // end of class ContextMemoryManager
00153 
00154 }
00155 
00156 #endif

Generated on Tue Jul 3 14:33:37 2007 for CVC3 by  doxygen 1.5.1