From: Brian Norris <banorris@uci.edu>
Date: Sat, 9 Mar 2013 20:51:36 +0000 (-0800)
Subject: mymemory, threads: add allocator specifically for Thread
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=db2c4ca161b4cba9e453431517af86798c0e9bdb;p=cdsspec-compiler.git

mymemory, threads: add allocator specifically for Thread

clas Thread is a special exception, where user-space allocations should
happend from the model-checker context. So provide a special set of
functions to specifically differentiate these allocations.
---

diff --git a/mymemory.cc b/mymemory.cc
index 44985fa..ea8670d 100644
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -155,14 +155,30 @@ static bool DontFree(void *ptr)
 	return (ptr >= (&bootstrapmemory[0]) && ptr < (&bootstrapmemory[BOOTSTRAPBYTES]));
 }
 
-/** @brief Snapshotting malloc implementation for user programs */
+/**
+ * @brief The allocator function for "user" allocation
+ *
+ * Should only be used for allocations which will not disturb the allocation
+ * patterns of a user thread.
+ */
+static void * user_malloc(size_t size)
+{
+	void *tmp = mspace_malloc(user_snapshot_space, size);
+	ASSERT(tmp);
+	return tmp;
+}
+
+/**
+ * @brief Snapshotting malloc implementation for user programs
+ *
+ * Do NOT call this function from a model-checker context. Doing so may disrupt
+ * the allocation patterns of a user thread.
+ */
 void *malloc(size_t size)
 {
-	if (user_snapshot_space) {
-		void *tmp = mspace_malloc(user_snapshot_space, size);
-		ASSERT(tmp);
-		return tmp;
-	} else
+	if (user_snapshot_space)
+		return user_malloc(size);
+	else
 		return HandleEarlyAllocationRequest(size);
 }
 
@@ -195,6 +211,18 @@ void * calloc(size_t num, size_t size)
 	}
 }
 
+/** @brief Snapshotting allocation function for use by the Thread class only */
+void * Thread_malloc(size_t size)
+{
+	return user_malloc(size);
+}
+
+/** @brief Snapshotting free function for use by the Thread class only */
+void Thread_free(void *ptr)
+{
+	free(ptr);
+}
+
 /** @brief Snapshotting new operator for user programs */
 void * operator new(size_t size) throw(std::bad_alloc)
 {
diff --git a/mymemory.h b/mymemory.h
index f2a3186..a62ab83 100644
--- a/mymemory.h
+++ b/mymemory.h
@@ -56,6 +56,9 @@ void * snapshot_calloc(size_t count, size_t size);
 void * snapshot_realloc(void *ptr, size_t size);
 void snapshot_free(void *ptr);
 
+void * Thread_malloc(size_t size);
+void Thread_free(void *ptr);
+
 /** @brief Provides a non-snapshotting allocator for use in STL classes.
  *
  * The code was adapted from a code example from the book The C++
diff --git a/threads-model.h b/threads-model.h
index e77e80c..eb0fd43 100644
--- a/threads-model.h
+++ b/threads-model.h
@@ -126,6 +126,18 @@ public:
 	 * to allow their allocation/deallocation to follow the same pattern as
 	 * the rest of the backtracked/replayed program.
 	 */
+	void * operator new(size_t size) {
+		return Thread_malloc(size);
+	}
+	void operator delete(void *p, size_t size) {
+		Thread_free(p);
+	}
+	void * operator new[](size_t size) {
+		return Thread_malloc(size);
+	}
+	void operator delete[](void *p, size_t size) {
+		Thread_free(p);
+	}
 private:
 	int create_context();