From 7cc208713f373ee83946b9d53a9c405bfec9e107 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 15 Dec 2009 18:20:31 +0000 Subject: Added context_mm (haven't tested compilation yet...) --- src/context/Makefile.am | 5 +- src/context/context_mm.cpp | 122 ++++++++++++++++++++++++++++++++++++++++++ src/context/context_mm.h | 128 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 254 insertions(+), 1 deletion(-) create mode 100644 src/context/context_mm.cpp create mode 100644 src/context/context_mm.h (limited to 'src') diff --git a/src/context/Makefile.am b/src/context/Makefile.am index eac088a9f..e38f7f4eb 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -6,4 +6,7 @@ noinst_LTLIBRARIES = libcontext.la libcontext_la_SOURCES = \ context.cpp \ - context.h + context.h \ + context_mm.cpp \ + context_mm.h + diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp new file mode 100644 index 000000000..51f192f2a --- /dev/null +++ b/src/context/context_mm.cpp @@ -0,0 +1,122 @@ +/********************* -*- 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 +#include +#include +#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 */ 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 d_chunkList; + + /** + * Queue of free chunks (for best cache performance, LIFO order is used) + */ + std::deque 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 d_nextFreeStack; + + /** + * Part of the stack of saved regions. This vector stores the saved value + * of d_endChunk. + */ + std::vector d_endChunkStack; + + /** + * Part of the stack of saved regions. This vector stores the saved value + * of d_indexChunkList + */ + std::vector 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 */ -- cgit v1.2.3