1 /********************* */ 2 /*! \file context_mm.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Clark Barrett, Andres Noetzli, Morgan Deters 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief Region-based memory manager with stack-based push and pop. 13 ** 14 ** Region-based memory manager with stack-based push and pop. Designed 15 ** for use by ContextManager. 16 **/ 17 18 #include "cvc4_private.h" 19 20 #ifndef __CVC4__CONTEXT__CONTEXT_MM_H 21 #define __CVC4__CONTEXT__CONTEXT_MM_H 22 23 #include <deque> 24 #include <limits> 25 #include <vector> 26 27 namespace CVC4 { 28 namespace context { 29 30 #ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER 31 32 /** 33 * Region-based memory manager for contexts. Calls to newData provide memory 34 * from the current region. This memory will persist until the entire 35 * region is deallocated (by calling pop). 36 * 37 * If push is called, the current region is deactivated and pushed on a 38 * stack, and a new current region is created. A subsequent call to pop 39 * releases the new region and restores the top region from the stack. 40 * 41 */ 42 class ContextMemoryManager { 43 44 /** 45 * Memory in regions is allocated in chunks. This is the chunk size 46 */ 47 static const unsigned chunkSizeBytes = 16384; 48 49 /** 50 * A list of free chunks is maintained. This is the maximum number of 51 * free chunks. 52 */ 53 static const unsigned maxFreeChunks = 100; 54 55 /** 56 * List of all chunks that are currently active 57 */ 58 std::vector<char*> d_chunkList; 59 60 /** 61 * Queue of free chunks (for best cache performance, LIFO order is used) 62 */ 63 std::deque<char*> d_freeChunks; 64 65 /** 66 * Pointer to the beginning of available memory in the current chunk in 67 * the current region. 68 */ 69 char* d_nextFree; 70 71 /** 72 * Pointer to one past the last available byte in the current chunk in 73 * the current region. 74 */ 75 char* d_endChunk; 76 77 /** 78 * The index in d_chunkList of the current chunk in the current region 79 */ 80 unsigned d_indexChunkList; 81 82 /** 83 * Part of the stack of saved regions. This vector stores the saved value 84 * of d_nextFree 85 */ 86 std::vector<char*> d_nextFreeStack; 87 88 /** 89 * Part of the stack of saved regions. This vector stores the saved value 90 * of d_endChunk. 91 */ 92 std::vector<char*> d_endChunkStack; 93 94 /** 95 * Part of the stack of saved regions. This vector stores the saved value 96 * of d_indexChunkList 97 */ 98 std::vector<unsigned> d_indexChunkListStack; 99 100 /** 101 * Private method to grab a new chunk for the current region. Uses chunk 102 * from d_freeChunks if available. Creates a new one otherwise. Sets the 103 * new chunk to be the current chunk. 104 */ 105 void newChunk(); 106 107 #ifdef CVC4_VALGRIND 108 /** 109 * Vector of allocations for each level. Used for accurately marking 110 * allocations as free'd in Valgrind. 111 */ 112 std::vector<std::vector<char*>> d_allocations; 113 #endif 114 115 public: 116 /** 117 * Get the maximum allocation size for this memory manager. 118 */ getMaxAllocationSize()119 static unsigned getMaxAllocationSize() { 120 return chunkSizeBytes; 121 } 122 123 /** 124 * Constructor - creates an initial region and an empty stack 125 */ 126 ContextMemoryManager(); 127 128 /** 129 * Destructor - deletes all memory in all regions 130 */ 131 ~ContextMemoryManager(); 132 133 /** 134 * Allocate size bytes from the current region 135 */ 136 void* newData(size_t size); 137 138 /** 139 * Create a new region. Push old region on the stack. 140 */ 141 void push(); 142 143 /** 144 * Delete all memory allocated in the current region and restore the top 145 * region from the stack 146 */ 147 void pop(); 148 149 };/* class ContextMemoryManager */ 150 151 #else /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ 152 153 #warning \ 154 "Using the debug version of ContextMemoryManager, expect performance degradation" 155 156 /** 157 * Dummy implementation of the ContextMemoryManager for debugging purposes. Use 158 * the configure flag "--enable-debug-context-memory-manager" to use this 159 * implementation. 160 */ 161 class ContextMemoryManager 162 { 163 public: getMaxAllocationSize()164 static unsigned getMaxAllocationSize() 165 { 166 return std::numeric_limits<unsigned>::max(); 167 } 168 ContextMemoryManager()169 ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); } ~ContextMemoryManager()170 ~ContextMemoryManager() 171 { 172 for (const auto& levelAllocs : d_allocations) 173 { 174 for (auto alloc : levelAllocs) 175 { 176 free(alloc); 177 } 178 } 179 } 180 newData(size_t size)181 void* newData(size_t size) 182 { 183 void* alloc = malloc(size); 184 d_allocations.back().push_back(static_cast<char*>(alloc)); 185 return alloc; 186 } 187 push()188 void push() { d_allocations.push_back(std::vector<char*>()); } 189 pop()190 void pop() 191 { 192 for (auto alloc : d_allocations.back()) 193 { 194 free(alloc); 195 } 196 d_allocations.pop_back(); 197 } 198 199 private: 200 std::vector<std::vector<char*>> d_allocations; 201 }; /* ContextMemoryManager */ 202 203 #endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */ 204 205 /** 206 * An STL-like allocator class for allocating from context memory. 207 */ 208 template <class T> 209 class ContextMemoryAllocator { 210 ContextMemoryManager* d_mm; 211 212 public: 213 214 typedef size_t size_type; 215 typedef std::ptrdiff_t difference_type; 216 typedef T* pointer; 217 typedef T const* const_pointer; 218 typedef T& reference; 219 typedef T const& const_reference; 220 typedef T value_type; 221 template <class U> struct rebind { 222 typedef ContextMemoryAllocator<U> other; 223 }; 224 ContextMemoryAllocator(ContextMemoryManager * mm)225 ContextMemoryAllocator(ContextMemoryManager* mm) : d_mm(mm) {} 226 template <class U> ContextMemoryAllocator(const ContextMemoryAllocator<U> & alloc)227 ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc) 228 : d_mm(alloc.getCMM()) 229 { 230 } ~ContextMemoryAllocator()231 ~ContextMemoryAllocator() {} 232 getCMM()233 ContextMemoryManager* getCMM() const { return d_mm; } address(T & v)234 T* address(T& v) const { return &v; } address(T const & v)235 T const* address(T const& v) const { return &v; } max_size()236 size_t max_size() const 237 { 238 return ContextMemoryManager::getMaxAllocationSize() / sizeof(T); 239 } 240 T* allocate(size_t n, const void* = 0) const { 241 return static_cast<T*>(d_mm->newData(n * sizeof(T))); 242 } deallocate(T * p,size_t n)243 void deallocate(T* p, size_t n) const { 244 /* no explicit delete */ 245 } construct(T * p,T const & v)246 void construct(T* p, T const& v) const { 247 ::new(reinterpret_cast<void*>(p)) T(v); 248 } destroy(T * p)249 void destroy(T* p) const { 250 p->~T(); 251 } 252 };/* class ContextMemoryAllocator<T> */ 253 254 template <class T> 255 inline bool operator==(const ContextMemoryAllocator<T>& a1, 256 const ContextMemoryAllocator<T>& a2) { 257 return a1.d_mm == a2.d_mm; 258 } 259 260 template <class T> 261 inline bool operator!=(const ContextMemoryAllocator<T>& a1, 262 const ContextMemoryAllocator<T>& a2) { 263 return a1.d_mm != a2.d_mm; 264 } 265 266 }/* CVC4::context namespace */ 267 }/* CVC4 namespace */ 268 269 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */ 270