blob: eeaa0a2c89fc97070d0a145b9b0842778af02236 (
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
|
/********************* -*- C++ -*- */
/** context_mm.h
** Original author: barrett
** Major contributors: none
** Minor contributors (to current version): mdeters
** 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 */
|
