blob: d48cbedc07a35e40ff3a63cf4d0abeebd0d744e7 (
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
|
/********************* -*- C++ -*- */
/** context_mm.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
** Region-based memory manager with stack-based push and pop. Designed
** for use by ContextManager.
**/
#ifndef __CVC4__CONTEXT__CONTEXT_MM_H
#define __CVC4__CONTEXT__CONTEXT_MM_H
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 minimum chunk size
*/
static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
/**
* 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:
/**
* Constructor - creates an initial region and an empty stack
*/
ContextMemoryManager();
/**
* Destructor - deletes all memory in all regions
*/
~ContextMemoryManager();
/**
* 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 */
}/* CVC4::context namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
|
