src/context/context_mm.h

   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    */
 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:
 164   static unsigned getMaxAllocationSize()
 165   {
 166     return std::numeric_limits<unsigned>::max();
 167   }
 168
 169   ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); }
 170   ~ContextMemoryManager()
 171   {
 172     for (const auto& levelAllocs : d_allocations)
 173     {
 174       for (auto alloc : levelAllocs)
 175       {
 176         free(alloc);
 177       }
 178     }
 179   }
 180
 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
 188   void push() { d_allocations.push_back(std::vector<char*>()); }
 189
 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
 225   ContextMemoryAllocator(ContextMemoryManager* mm) : d_mm(mm) {}
 226   template <class U>
 227   ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc)
 228       : d_mm(alloc.getCMM())
 229   {
 230   }
 231   ~ContextMemoryAllocator() {}
 232
 233   ContextMemoryManager* getCMM() const { return d_mm; }
 234   T* address(T& v) const { return &v; }
 235   T const* address(T const& v) const { return &v; }
 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   }
 243   void deallocate(T* p, size_t n) const {
 244     /* no explicit delete */
 245   }
 246   void construct(T* p, T const& v) const {
 247     ::new(reinterpret_cast<void*>(p)) T(v);
 248   }
 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 */