X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c19c37f0cdc778684d6796842043a7b71afee440;hb=33b5b3edcfd8e5a2c0349c60be2bef6da08d1e33;hp=84b296e56b109e2a4295d312c1a7746a5267d30c;hpb=34a8b735d1de5aafa72277a40ee3280efc32cd4a;p=model-checker.git

diff --git a/model.cc b/model.cc
index 84b296e..c19c37f 100644
--- a/model.cc
+++ b/model.cc
@@ -1,55 +1,98 @@
 #include <stdio.h>
 
 #include "model.h"
+#include "action.h"
+#include "tree.h"
 #include "schedule.h"
 #include "common.h"
 
 #define INITIAL_THREAD_ID	0
 
+class Backtrack {
+public:
+	Backtrack(ModelAction *d, action_list_t *t) {
+		diverge = d;
+		actionTrace = t;
+		iter = actionTrace->begin();
+	}
+	ModelAction * get_diverge() { return diverge; }
+	action_list_t * get_trace() { return actionTrace; }
+	void advance_state() { iter++; }
+	ModelAction * get_state() {
+		return iter == actionTrace->end() ? NULL : *iter;
+	}
+private:
+	ModelAction *diverge;
+	action_list_t *actionTrace;
+	/* points to position in actionTrace as we replay */
+	action_list_t::iterator iter;
+};
+
 ModelChecker *model;
 
-ModelChecker::ModelChecker()
+void free_action_list(action_list_t *list)
 {
-	/* First thread created will have id (INITIAL_THREAD_ID + 1) */
-	this->used_thread_id = INITIAL_THREAD_ID;
-	/* Initialize default scheduler */
-	this->scheduler = new Scheduler();
-
-	num_executions = 0;
-	this->current_action = NULL;
-	this->exploring = NULL;
-	this->nextThread = THREAD_ID_T_NONE;
+	action_list_t::iterator it;
+	for (it = list->begin(); it != list->end(); it++)
+		delete (*it);
+	delete list;
+}
 
-	rootNode = new TreeNode(NULL);
-	currentNode = rootNode;
-	action_trace = new action_list_t();
+ModelChecker::ModelChecker()
+	:
+	/* Initialize default scheduler */
+	scheduler(new Scheduler()),
+	/* First thread created will have id INITIAL_THREAD_ID */
+	next_thread_id(INITIAL_THREAD_ID),
+	used_sequence_numbers(0),
+
+	num_executions(0),
+	current_action(NULL),
+	exploring(NULL),
+	nextThread(THREAD_ID_T_NONE),
+	action_trace(new action_list_t()),
+	rootNode(new TreeNode()),
+	currentNode(rootNode)
+{
 }
 
 ModelChecker::~ModelChecker()
 {
-	delete action_trace;
-	delete this->scheduler;
+	std::map<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 scheduler;
 	delete rootNode;
 }
 
 void ModelChecker::reset_to_initial_state()
 {
 	DEBUG("+++ Resetting to initial state +++\n");
-	std::map<thread_id_t, class Thread *>::iterator it;
-	for (it = thread_map.begin(); it != thread_map.end(); it++) {
+	std::map<int, class Thread *>::iterator it;
+	for (it = thread_map.begin(); it != thread_map.end(); it++)
 		delete (*it).second;
-	}
 	thread_map.clear();
 	action_trace = new action_list_t();
 	currentNode = rootNode;
 	current_action = NULL;
-	used_thread_id = INITIAL_THREAD_ID;
+	next_thread_id = INITIAL_THREAD_ID;
+	used_sequence_numbers = 0;
+	nextThread = 0;
 	/* scheduler reset ? */
 }
 
-int ModelChecker::get_next_id()
+thread_id_t ModelChecker::get_next_id()
+{
+	return next_thread_id++;
+}
+
+int ModelChecker::get_next_seq_num()
 {
-	return ++used_thread_id;
+	return ++used_sequence_numbers;
 }
 
 Thread * ModelChecker::schedule_next_thread()
@@ -57,9 +100,10 @@ Thread * ModelChecker::schedule_next_thread()
 	Thread *t;
 	if (nextThread == THREAD_ID_T_NONE)
 		return NULL;
-	t = thread_map[nextThread];
-	if (t == NULL)
-		DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+	t = thread_map[id_to_int(nextThread)];
+
+	ASSERT(t != NULL);
+
 	return t;
 }
 
@@ -75,10 +119,19 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	ModelAction *next;
 	thread_id_t tid;
 
+	/* Have we completed exploring the preselected path? */
+	if (exploring == NULL)
+		return THREAD_ID_T_NONE;
+
+	/* Else, we are trying to replay an execution */
+	exploring->advance_state();
+
+	ASSERT(exploring->get_state() != NULL);
+
 	next = exploring->get_state();
 
 	if (next == exploring->get_diverge()) {
-		TreeNode *node = next->get_node();
+		TreeNode *node = next->get_treenode();
 
 		/* Reached divergence point; discard our current 'exploring' */
 		DEBUG("*** Discard 'Backtrack' object ***\n");
@@ -92,28 +145,22 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	return tid;
 }
 
-thread_id_t ModelChecker::advance_backtracking_state()
-{
-	/* Have we completed exploring the preselected path? */
-	if (exploring == NULL)
-		return THREAD_ID_T_NONE;
-
-	/* Else, we are trying to replay an execution */
-	exploring->advance_state();
-	if (exploring->get_state() == NULL)
-		DEBUG("*** error: reached end of backtrack trace\n");
-
-	return get_next_replay_thread();
-}
-
 bool ModelChecker::next_execution()
 {
+	DBG();
+
 	num_executions++;
 	print_summary();
 	if ((exploring = model->get_next_backtrack()) == NULL)
 		return false;
+
+	if (DBG_ENABLED()) {
+		printf("Next execution will diverge at:\n");
+		exploring->get_diverge()->print();
+		print_list(exploring->get_trace());
+	}
+
 	model->reset_to_initial_state();
-	nextThread = get_next_replay_thread();
 	return true;
 }
 
@@ -145,22 +192,26 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
 	ModelAction *prev;
 	TreeNode *node;
+	Thread *t = get_thread(act->get_tid());
 
 	prev = get_last_conflict(act);
 	if (prev == NULL)
 		return;
 
-	node = prev->get_node();
+	node = prev->get_treenode();
+
+	while (t && !node->is_enabled(t))
+		t = t->get_parent();
 
 	/* Check if this has been explored already */
-	if (node->hasBeenExplored(act->get_tid()))
+	if (node->hasBeenExplored(t->get_id()))
 		return;
 	/* If this is a new backtracking point, mark the tree */
-	if (node->setBacktrack(act->get_tid()) != 0)
+	if (node->setBacktrack(t->get_id()) != 0)
 		return;
 
 	DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-			prev->get_tid(), act->get_tid());
+			prev->get_tid(), t->get_id());
 	if (DBG_ENABLED()) {
 		prev->print();
 		act->print();
@@ -182,35 +233,41 @@ Backtrack * ModelChecker::get_next_backtrack()
 
 void ModelChecker::check_current_action(void)
 {
-	ModelAction *next = this->current_action;
-
-	if (!next) {
+	ModelAction *curr = this->current_action;
+	current_action = NULL;
+	if (!curr) {
 		DEBUG("trying to push NULL action...\n");
 		return;
 	}
-	current_action = NULL;
-	nextThread = advance_backtracking_state();
-	next->set_node(currentNode);
-	set_backtracking(next);
-	currentNode = currentNode->exploreChild(next->get_tid());
-	this->action_trace->push_back(next);
+
+	nextThread = get_next_replay_thread();
+	curr->set_node(currentNode);
+	set_backtracking(curr);
+	currentNode = currentNode->explore_child(curr);
+	this->action_trace->push_back(curr);
 }
 
 void ModelChecker::print_summary(void)
 {
-	action_list_t::iterator it;
-
 	printf("\n");
-	printf("---------------------------------------------------------------------\n");
 	printf("Number of executions: %d\n", num_executions);
-	printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
+	printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
 
 	scheduler->print();
 
-	printf("Trace:\n\n");
+	print_list(action_trace);
+	printf("\n");
+
+}
+
+void ModelChecker::print_list(action_list_t *list)
+{
+	action_list_t::iterator it;
 
-	for (it = action_trace->begin(); it != action_trace->end(); it++) {
-		DBG();
+	printf("---------------------------------------------------------------------\n");
+	printf("Trace:\n");
+
+	for (it = list->begin(); it != list->end(); it++) {
 		(*it)->print();
 	}
 	printf("---------------------------------------------------------------------\n");
@@ -218,7 +275,7 @@ void ModelChecker::print_summary(void)
 
 int ModelChecker::add_thread(Thread *t)
 {
-	thread_map[t->get_id()] = t;
+	thread_map[id_to_int(t->get_id())] = t;
 	scheduler->add_thread(t);
 	return 0;
 }
@@ -238,97 +295,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;
-}
-
-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("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
-}