00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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 const unsigned chunkSizeBytes = 16384;
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039
00040
00041
00042
00043 class ContextMemoryManager :public MemoryManager {
00044 static std::vector<char*> s_freePages;
00045 std::vector<char*> d_chunkList;
00046
00047
00048 char* d_nextFree;
00049
00050 char* d_endChunk;
00051
00052 unsigned d_indexChunkList;
00053
00054
00055 std::vector<char*> d_nextFreeStack;
00056
00057 std::vector<char*> d_endChunkStack;
00058
00059 std::vector<unsigned> d_indexChunkListStack;
00060
00061
00062 void newChunk() {
00063 DebugAssert(d_chunkList.size() > 0, "expected unempty list");
00064 ++d_indexChunkList;
00065 DebugAssert(d_chunkList.size() == d_indexChunkList, "invariant violated");
00066 if (s_freePages.empty()) {
00067 d_chunkList.push_back((char*)malloc(chunkSizeBytes));
00068 }
00069 else {
00070 d_chunkList.push_back(s_freePages.back());
00071 s_freePages.pop_back();
00072 }
00073 d_nextFree = d_chunkList.back();
00074 FatalAssert(d_nextFree != NULL, "Out of memory");
00075 d_endChunk = d_nextFree + chunkSizeBytes;
00076 }
00077
00078 public:
00079
00080 ContextMemoryManager()
00081 : d_indexChunkList(0)
00082 {
00083 if (s_freePages.empty()) {
00084 d_chunkList.push_back((char*)malloc(chunkSizeBytes));
00085 }
00086 else {
00087 d_chunkList.push_back(s_freePages.back());
00088 s_freePages.pop_back();
00089 }
00090 d_nextFree = d_chunkList.back();
00091 FatalAssert(d_nextFree != NULL, "Out of memory");
00092 d_endChunk = d_nextFree + chunkSizeBytes;
00093 }
00094
00095
00096 ~ContextMemoryManager() {
00097 while(!d_chunkList.empty()) {
00098 s_freePages.push_back(d_chunkList.back());
00099 d_chunkList.pop_back();
00100 }
00101 }
00102
00103 void* newData(size_t size) {
00104 void* res = (void*)d_nextFree;
00105 d_nextFree += size;
00106 if (d_nextFree > d_endChunk) {
00107 newChunk();
00108 res = (void*)d_nextFree;
00109 d_nextFree += size;
00110 DebugAssert(d_nextFree <= d_endChunk, "chunk not big enough");
00111 }
00112 return res;
00113 }
00114
00115 void deleteData(void* d) { }
00116
00117 void push() {
00118 d_nextFreeStack.push_back(d_nextFree);
00119 d_endChunkStack.push_back(d_endChunk);
00120 d_indexChunkListStack.push_back(d_indexChunkList);
00121 }
00122
00123 void pop() {
00124 d_nextFree = d_nextFreeStack.back();
00125 d_nextFreeStack.pop_back();
00126 d_endChunk = d_endChunkStack.back();
00127 d_endChunkStack.pop_back();
00128 while (d_indexChunkList > d_indexChunkListStack.back()) {
00129 s_freePages.push_back(d_chunkList.back());
00130 d_chunkList.pop_back();
00131 --d_indexChunkList;
00132 }
00133 d_indexChunkListStack.pop_back();
00134 }
00135
00136 static void garbageCollect(void) {
00137 while (!s_freePages.empty()) {
00138 free(s_freePages.back());
00139 s_freePages.pop_back();
00140 }
00141 }
00142
00143 unsigned getMemory(int verbosity) {
00144 unsigned long memSelf = sizeof(ContextMemoryManager);
00145 unsigned long mem = 0;
00146
00147 mem += MemoryTracker::getVec(verbosity - 1, d_chunkList);
00148 mem += MemoryTracker::getVec(verbosity - 1, d_nextFreeStack);
00149 mem += MemoryTracker::getVec(verbosity - 1, d_endChunkStack);
00150 mem += MemoryTracker::getVec(verbosity - 1, d_indexChunkListStack);
00151
00152 mem += d_chunkList.size() * chunkSizeBytes;
00153
00154 MemoryTracker::print("ContextMemoryManager", verbosity, memSelf, mem);
00155
00156 return mem + memSelf;
00157 }
00158
00159 static unsigned getStaticMemory(int verbosity) {
00160 unsigned mem = 0;
00161 mem += MemoryTracker::getVec(verbosity - 1, s_freePages);
00162 mem += s_freePages.size() * chunkSizeBytes;
00163 MemoryTracker::print("ContextMemoryManager Static", verbosity, 0, mem);
00164 return mem;
00165 }
00166
00167 };
00168
00169 }
00170
00171 #endif