From: Brian Norris <banorris@uci.edu>
Date: Sat, 9 Mar 2013 20:54:58 +0000 (-0800)
Subject: mymemory: enforce that user allocations come from user context
X-Git-Tag: oopsla2013~142
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=a635c5cdf004963a948dfb40e0fa27ce258bbccf

mymemory: enforce that user allocations come from user context
---

diff --git a/model.cc b/model.cc
index 0cc2079..2aa94cf 100644
--- a/model.cc
+++ b/model.cc
@@ -3021,6 +3021,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
 	DBG();
 	Thread *old = thread_current();
+	scheduler->set_current_thread(NULL);
 	ASSERT(!old->get_pending());
 	old->set_pending(act);
 	if (Thread::swap(old, &system_context) < 0) {
diff --git a/mymemory.cc b/mymemory.cc
index ea8670d..c79ad9a 100644
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -8,6 +8,8 @@
 #include "mymemory.h"
 #include "snapshot.h"
 #include "common.h"
+#include "threads-model.h"
+#include "model.h"
 
 #define REQUESTS_BEFORE_ALLOC 1024
 
@@ -176,9 +178,11 @@ static void * user_malloc(size_t size)
  */
 void *malloc(size_t size)
 {
-	if (user_snapshot_space)
+	if (user_snapshot_space) {
+		/* Only perform user allocations from user context */
+		ASSERT(!model || thread_current());
 		return user_malloc(size);
-	else
+	} else
 		return HandleEarlyAllocationRequest(size);
 }
 
diff --git a/schedule.cc b/schedule.cc
index 1eb57d7..62ba8fb 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -250,7 +250,7 @@ void Scheduler::set_scheduler_thread(thread_id_t tid) {
  */
 void Scheduler::set_current_thread(Thread *t)
 {
-	ASSERT(t && !t->is_model_thread());
+	ASSERT(!t || !t->is_model_thread());
 
 	current = t;
 	if (DBG_ENABLED())