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