--- /dev/null
+/********************* -*- C++ -*- */
+/** context_mm.cpp
+ ** 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.
+ **
+ ** Implementation of Context Memory Manaer
+ **/
+
+
+#include <cstdlib>
+#include <vector>
+#include <deque>
+#include "context/context_mm.h"
+#include "util/Assert.h"
+
+
+namespace CVC4 {
+namespace context {
+
+
+void ContextMemoryManager::newChunk() {
+
+ // Increment index to chunk list
+ ++d_indexChunkList;
+ Assert(d_chunkList.size() == d_indexChunkList,
+ "Index should be at the end of the list");
+
+ // Create new chunk if no free chunk available
+ if (d_freePages.empty()) {
+ d_chunkList.push_back((char*)malloc(chunkSizeBytes));
+ if (d_chunkList.back() == NULL) {
+ throw bad_alloc();
+ }
+ }
+ // If there is a free chunk, use that
+ else {
+ d_chunkList.push_back(d_freePages.back());
+ d_freePages.pop_back();
+ }
+ // Set up the current chunk pointers
+ d_nextFree = d_chunkList.back();
+ d_endChunk = d_nextFree + chunkSizeBytes;
+}
+
+
+ContextMemoryManager() : d_indexChunkList(0) {
+ // Create initial chunk
+ d_chunkList.push_back((char*)malloc(chunkSizeBytes));
+ d_nextFree = d_chunkList.back();
+ if (d_nextFree == NULL) {
+ throw bad_alloc;
+ }
+ d_endChunk = d_nextFree + chunkSizeBytes;
+}
+
+
+~ContextMemoryManager() {
+ // Delete all chunks
+ while (!d_chunkList.empty()) {
+ free(d_chunkList.back());
+ d_chunkList.pop_back();
+ }
+ while (!d_freePages.empty()) {
+ free(d_freePages.back());
+ d_freePages.pop_back();
+ }
+}
+
+void* newData(size_t size) {
+ // Use next available free location in current chunk
+ void* res = (void*)d_nextFree;
+ d_nextFree += size;
+ // Check if the request is too big for the chunk
+ if (d_nextFree > d_endChunk) {
+ newChunk();
+ res = (void*)d_nextFree;
+ d_nextFree += size;
+ AlwaysAssert(d_nextFree <= d_endChunk,
+ "Request is bigger than memory chunk size");
+ }
+ return res;
+}
+
+
+void push() {
+ // Store current state on the stack
+ d_nextFreeStack.push_back(d_nextFree);
+ d_endChunkStack.push_back(d_endChunk);
+ d_indexChunkListStack.push_back(d_indexChunkList);
+}
+
+
+void pop() {
+ // Restore state from stack
+ d_nextFree = d_nextFreeStack.back();
+ d_nextFreeStack.pop_back();
+ d_endChunk = d_endChunkStack.back();
+ d_endChunkStack.pop_back();
+
+ // Free all the new chunks since the last push
+ while (d_indexChunkList > d_indexChunkListStack.back()) {
+ d_freePages.push_back(d_chunkList.back());
+ d_chunkList.pop_back();
+ --d_indexChunkList;
+ }
+ d_indexChunkListStack.pop_back();
+
+ // Delete excess free chunks
+ while (d_freeChunks.size() > maxFreeChunks) {
+ free(d_freePages.front());
+ d_freePages.pop_front();
+ }
+}
+
+
+}/* CVC4::context namespace */
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- 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 */
projects / cvc5.git / commitdiff