Added context_mm (haven't tested compilation yet...)

3 files changed, 254 insertions, 1 deletions

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 <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 */
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 */