blob: b580d86d52e2c698fb8b477c7511ae07a31c2ac6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
|
/********************* */
/*! \file context_mm.h
** \verbatim
** Original author: Clark Barrett
** Major contributors: Morgan Deters
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Region-based memory manager with stack-based push and pop.
**
** Region-based memory manager with stack-based push and pop. Designed
** for use by ContextManager.
**/
#include "cvc4_private.h"
#ifndef __CVC4__CONTEXT__CONTEXT_MM_H
#define __CVC4__CONTEXT__CONTEXT_MM_H
#include <vector>
#include <deque>
namespace CVC4 {
namespace context {
/**
* Region-based memory manager for contexts. Calls to newData provide memory
* from the current region. This memory will persist until the entire
* region is deallocated (by calling pop).
*
* If push is called, the current region is deactivated and pushed on a
* stack, and a new current region is created. A subsequent call to pop
* releases the new region and restores the top region from the stack.
*
*/
class ContextMemoryManager {
/**
* Memory in regions is allocated in chunks. This is the chunk size
*/
static const unsigned chunkSizeBytes = 16384;
/**
* A list of free chunks is maintained. This is the maximum number of
* free chunks.
*/
static const unsigned maxFreeChunks = 100;
/**
* List of all chunks that are currently active
*/
std::vector<char*> d_chunkList;
/**
* Queue of free chunks (for best cache performance, LIFO order is used)
*/
std::deque<char*> d_freeChunks;
/**
* Pointer to the beginning of available memory in the current chunk in
* the current region.
*/
char* d_nextFree;
/**
* Pointer to one past the last available byte in the current chunk in
* the current region.
*/
char* d_endChunk;
/**
* The index in d_chunkList of the current chunk in the current region
*/
unsigned d_indexChunkList;
/**
* Part of the stack of saved regions. This vector stores the saved value
* of d_nextFree
*/
std::vector<char*> d_nextFreeStack;
/**
* Part of the stack of saved regions. This vector stores the saved value
* of d_endChunk.
*/
std::vector<char*> d_endChunkStack;
/**
* Part of the stack of saved regions. This vector stores the saved value
* of d_indexChunkList
*/
std::vector<unsigned> d_indexChunkListStack;
/**
* Private method to grab a new chunk for the current region. Uses chunk
* from d_freeChunks if available. Creates a new one otherwise. Sets the
* new chunk to be the current chunk.
*/
void newChunk();
public:
/**
* Get the maximum allocation size for this memory manager.
*/
static unsigned getMaxAllocationSize() {
return chunkSizeBytes;
}
/**
* Constructor - creates an initial region and an empty stack
*/
ContextMemoryManager();
/**
* Destructor - deletes all memory in all regions
*/
~ContextMemoryManager() throw();
/**
* Allocate size bytes from the current region
*/
void* newData(size_t size);
/**
* Create a new region. Push old region on the stack.
*/
void push();
/**
* Delete all memory allocated in the current region and restore the top
* region from the stack
*/
void pop();
};/* class ContextMemoryManager */
/**
* An STL-like allocator class for allocating from context memory.
*/
template <class T>
class ContextMemoryAllocator {
ContextMemoryManager* d_mm;
public:
typedef size_t size_type;
typedef std::ptrdiff_t difference_type;
typedef T* pointer;
typedef T const* const_pointer;
typedef T& reference;
typedef T const& const_reference;
typedef T value_type;
template <class U> struct rebind {
typedef ContextMemoryAllocator<U> other;
};
ContextMemoryAllocator(ContextMemoryManager* mm) throw() : d_mm(mm) {}
template <class U>
ContextMemoryAllocator(const ContextMemoryAllocator<U>& alloc) throw() : d_mm(alloc.getCMM()) {}
~ContextMemoryAllocator() throw() {}
ContextMemoryManager* getCMM() const { return d_mm; }
T* address(T& v) const { return &v; }
T const* address(T const& v) const { return &v; }
size_t max_size() const throw() {
return ContextMemoryManager::getMaxAllocationSize() / sizeof(T);
}
T* allocate(size_t n, const void* = 0) const {
return static_cast<T*>(d_mm->newData(n * sizeof(T)));
}
void deallocate(T* p, size_t n) const {
/* no explicit delete */
}
void construct(T* p, T const& v) const {
::new(reinterpret_cast<void*>(p)) T(v);
}
void destroy(T* p) const {
p->~T();
}
};/* class ContextMemoryAllocator<T> */
template <class T>
inline bool operator==(const ContextMemoryAllocator<T>& a1,
const ContextMemoryAllocator<T>& a2) {
return a1.d_mm == a2.d_mm;
}
template <class T>
inline bool operator!=(const ContextMemoryAllocator<T>& a1,
const ContextMemoryAllocator<T>& a2) {
return a1.d_mm != a2.d_mm;
}
}/* CVC4::context namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
|
