X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=51715d22614afaa3e61afa05df063cddba64c4a6;hp=e3238258a3aa86b0570ff8ed8159eb62e27a899c;hb=02792abf9399d1dca2fab7bc511f09e934d05f1d;hpb=c5e14aa2426f21f8de620cf24ed321447d75c989

diff --git a/model.cc b/model.cc
index e3238258..51715d22 100644
--- a/model.cc
+++ b/model.cc
@@ -4,6 +4,8 @@
 #include "action.h"
 #include "tree.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
+#undef DEBUG
 #include "common.h"
 
 #define INITIAL_THREAD_ID	0
@@ -30,6 +32,14 @@ private:
 
 ModelChecker *model;
 
+void free_action_list(action_list_t *list)
+{
+	action_list_t::iterator it;
+	for (it = list->begin(); it != list->end(); it++)
+		delete (*it);
+	delete list;
+}
+
 ModelChecker::ModelChecker()
 {
 	/* First thread created will have id INITIAL_THREAD_ID */
@@ -50,7 +60,13 @@ ModelChecker::ModelChecker()
 
 ModelChecker::~ModelChecker()
 {
-	delete action_trace;
+	std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
+	for (it = thread_map.begin(); it != thread_map.end(); it++)
+		delete (*it).second;
+	thread_map.clear();
+
+	free_action_list(action_trace);
+
 	delete this->scheduler;
 	delete rootNode;
 }
@@ -58,7 +74,7 @@ ModelChecker::~ModelChecker()
 void ModelChecker::reset_to_initial_state()
 {
 	DEBUG("+++ Resetting to initial state +++\n");
-	std::map<int, class Thread *>::iterator it;
+	std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
 	for (it = thread_map.begin(); it != thread_map.end(); it++)
 		delete (*it).second;
 	thread_map.clear();
@@ -86,8 +102,9 @@ Thread * ModelChecker::schedule_next_thread()
 	if (nextThread == THREAD_ID_T_NONE)
 		return NULL;
 	t = thread_map[id_to_int(nextThread)];
-	if (t == NULL)
-		DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+
+	ASSERT(t != NULL);
+
 	return t;
 }
 
@@ -285,99 +302,3 @@ int ModelChecker::switch_to_master(ModelAction *act)
 	old->set_state(THREAD_READY);
 	return Thread::swap(old, get_system_context());
 }
-
-ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
-{
-	Thread *t = thread_current();
-	ModelAction *act = this;
-
-	act->type = type;
-	act->order = order;
-	act->location = loc;
-	act->tid = t->get_id();
-	act->value = value;
-	act->seq_number = model->get_next_seq_num();
-}
-
-bool ModelAction::is_read()
-{
-	return type == ATOMIC_READ;
-}
-
-bool ModelAction::is_write()
-{
-	return type == ATOMIC_WRITE;
-}
-
-bool ModelAction::is_acquire()
-{
-	switch (order) {
-	case memory_order_acquire:
-	case memory_order_acq_rel:
-	case memory_order_seq_cst:
-		return true;
-	default:
-		return false;
-	}
-}
-
-bool ModelAction::is_release()
-{
-	switch (order) {
-	case memory_order_release:
-	case memory_order_acq_rel:
-	case memory_order_seq_cst:
-		return true;
-	default:
-		return false;
-	}
-}
-
-bool ModelAction::same_var(ModelAction *act)
-{
-	return location == act->location;
-}
-
-bool ModelAction::same_thread(ModelAction *act)
-{
-	return tid == act->tid;
-}
-
-bool ModelAction::is_dependent(ModelAction *act)
-{
-	if (!is_read() && !is_write())
-		return false;
-	if (!act->is_read() && !act->is_write())
-		return false;
-	if (same_var(act) && !same_thread(act) &&
-			(is_write() || act->is_write()))
-		return true;
-	return false;
-}
-
-void ModelAction::print(void)
-{
-	const char *type_str;
-	switch (this->type) {
-	case THREAD_CREATE:
-		type_str = "thread create";
-		break;
-	case THREAD_YIELD:
-		type_str = "thread yield";
-		break;
-	case THREAD_JOIN:
-		type_str = "thread join";
-		break;
-	case ATOMIC_READ:
-		type_str = "atomic read";
-		break;
-	case ATOMIC_WRITE:
-		type_str = "atomic write";
-		break;
-	default:
-		type_str = "unknown type";
-	}
-
-	printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n",
-			seq_number, id_to_int(tid), type_str, order, location, value);
-}