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

diff --git a/model.cc b/model.cc
index 51715d2..06fe72f 100644
--- a/model.cc
+++ b/model.cc
@@ -2,88 +2,57 @@
 
 #include "model.h"
 #include "action.h"
-#include "tree.h"
+#include "nodestack.h"
 #include "schedule.h"
 #include "snapshot-interface.h"
-#undef DEBUG
 #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;
 
-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 */
-	this->next_thread_id = INITIAL_THREAD_ID;
-	used_sequence_numbers = 0;
+	:
 	/* Initialize default scheduler */
-	this->scheduler = new Scheduler();
-
-	num_executions = 0;
-	this->current_action = NULL;
-	this->exploring = NULL;
-	this->nextThread = THREAD_ID_T_NONE;
-
-	rootNode = new TreeNode();
-	currentNode = rootNode;
-	action_trace = new action_list_t();
+	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),
+	diverge(NULL),
+	nextThread(THREAD_ID_T_NONE),
+	action_trace(new action_list_t()),
+	thread_map(new std::map<int, class Thread *>),
+	node_stack(new NodeStack()),
+	next_backtrack(NULL)
+{
 }
 
 ModelChecker::~ModelChecker()
 {
-	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++)
+	std::map<int, class Thread *>::iterator it;
+	for (it = thread_map->begin(); it != thread_map->end(); it++)
 		delete (*it).second;
-	thread_map.clear();
+	delete thread_map;
 
-	free_action_list(action_trace);
+	delete action_trace;
 
-	delete this->scheduler;
-	delete rootNode;
+	delete node_stack;
+	delete scheduler;
 }
 
 void ModelChecker::reset_to_initial_state()
 {
 	DEBUG("+++ Resetting to initial state +++\n");
-	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();
-	action_trace = new action_list_t();
-	currentNode = rootNode;
+	node_stack->reset_execution();
 	current_action = NULL;
 	next_thread_id = INITIAL_THREAD_ID;
 	used_sequence_numbers = 0;
-	/* scheduler reset ? */
+	nextThread = 0;
+	next_backtrack = NULL;
+	snapshotObject->backTrackBeforeStep(0);
 }
 
 thread_id_t ModelChecker::get_next_id()
@@ -101,7 +70,7 @@ Thread * ModelChecker::schedule_next_thread()
 	Thread *t;
 	if (nextThread == THREAD_ID_T_NONE)
 		return NULL;
-	t = thread_map[id_to_int(nextThread)];
+	t = (*thread_map)[id_to_int(nextThread)];
 
 	ASSERT(t != NULL);
 
@@ -120,16 +89,20 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	ModelAction *next;
 	thread_id_t tid;
 
-	next = exploring->get_state();
+	/* Have we completed exploring the preselected path? */
+	if (diverge == NULL)
+		return THREAD_ID_T_NONE;
+
+	/* Else, we are trying to replay an execution */
+	next = node_stack->get_next()->get_action();
 
-	if (next == exploring->get_diverge()) {
-		TreeNode *node = next->get_node();
+	if (next == diverge) {
+		Node *node = next->get_node();
 
-		/* Reached divergence point; discard our current 'exploring' */
-		DEBUG("*** Discard 'Backtrack' object ***\n");
-		tid = node->getNextBacktrack();
-		delete exploring;
-		exploring = NULL;
+		/* Reached divergence point */
+		DEBUG("*** Divergence point ***\n");
+		tid = node->get_next_backtrack();
+		diverge = NULL;
 	} else {
 		tid = next->get_tid();
 	}
@@ -137,37 +110,21 @@ 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();
-
-	ASSERT(exploring->get_state() != NULL);
-
-	return get_next_replay_thread();
-}
-
 bool ModelChecker::next_execution()
 {
 	DBG();
 
 	num_executions++;
 	print_summary();
-	if ((exploring = model->get_next_backtrack()) == NULL)
+	if ((diverge = 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());
+		diverge->print();
 	}
 
 	model->reset_to_initial_state();
-	nextThread = get_next_replay_thread();
 	return true;
 }
 
@@ -198,7 +155,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 void ModelChecker::set_backtracking(ModelAction *act)
 {
 	ModelAction *prev;
-	TreeNode *node;
+	Node *node;
 	Thread *t = get_thread(act->get_tid());
 
 	prev = get_last_conflict(act);
@@ -207,64 +164,68 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
 	node = prev->get_node();
 
-	while (t && !node->is_enabled(t))
+	while (!node->is_enabled(t))
 		t = t->get_parent();
 
 	/* Check if this has been explored already */
-	if (node->hasBeenExplored(t->get_id()))
+	if (node->has_been_explored(t->get_id()))
 		return;
+
+	if (!next_backtrack || *prev > *next_backtrack)
+		next_backtrack = prev;
+
 	/* If this is a new backtracking point, mark the tree */
-	if (node->setBacktrack(t->get_id()) != 0)
+	if (!node->set_backtrack(t->get_id()))
 		return;
-
 	DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 			prev->get_tid(), t->get_id());
 	if (DBG_ENABLED()) {
 		prev->print();
 		act->print();
 	}
-
-	Backtrack *back = new Backtrack(prev, action_trace);
-	backtrack_list.push_back(back);
 }
 
-Backtrack * ModelChecker::get_next_backtrack()
+ModelAction * ModelChecker::get_next_backtrack()
 {
-	Backtrack *next;
-	if (backtrack_list.empty())
-		return NULL;
-	next = backtrack_list.back();
-	backtrack_list.pop_back();
+	ModelAction *next = next_backtrack;
+	next_backtrack = NULL;
 	return next;
 }
 
 void ModelChecker::check_current_action(void)
 {
-	ModelAction *next = this->current_action;
+	Node *currnode;
 
-	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->explore_child(next);
-	this->action_trace->push_back(next);
+
+	curr = node_stack->explore_action(curr);
+	nextThread = get_next_replay_thread();
+
+	currnode = curr->get_node();
+
+	if (!currnode->backtrack_empty())
+		if (!next_backtrack || *curr > *next_backtrack)
+			next_backtrack = curr;
+
+	set_backtracking(curr);
+	this->action_trace->push_back(curr);
 }
 
 void ModelChecker::print_summary(void)
 {
 	printf("\n");
 	printf("Number of executions: %d\n", num_executions);
-	printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
+	printf("Total nodes created: %d\n", Node::get_total_nodes());
 
 	scheduler->print();
 
 	print_list(action_trace);
 	printf("\n");
-
 }
 
 void ModelChecker::print_list(action_list_t *list)
@@ -282,7 +243,7 @@ void ModelChecker::print_list(action_list_t *list)
 
 int ModelChecker::add_thread(Thread *t)
 {
-	thread_map[id_to_int(t->get_id())] = t;
+	(*thread_map)[id_to_int(t->get_id())] = t;
 	scheduler->add_thread(t);
 	return 0;
 }