diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2009-12-15 18:20:31 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2009-12-15 18:20:31 +0000 |
commit | 7cc208713f373ee83946b9d53a9c405bfec9e107 (patch) | |
tree | 1843a7b1443f4ed879ebaed48d92bb9359e3e4ba /src/context/context_mm.h | |
parent | 094e37d8879834c7bd30452f841953293a5e2825 (diff) |
Added context_mm (haven't tested compilation yet...)
Diffstat (limited to 'src/context/context_mm.h')
-rw-r--r-- | src/context/context_mm.h | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/src/context/context_mm.h b/src/context/context_mm.h new file mode 100644 index 000000000..6b442d4a0 --- /dev/null +++ b/src/context/context_mm.h @@ -0,0 +1,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 + */ + const unsigned chunkSizeBytes = 16384; // #bytes in each chunk + + /** + * A list of free chunks is maintained. This is the maximum number of + * free chunks. + */ + 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 */ |