X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=70440f5050b3c3bc0adaf157e44db0959f3c6476;hp=f4da33071170beb37d21e55fbe21f498281a79a2;hb=b8bcaaa5a4b4d2413e3a0f419bbb91c540b28e50;hpb=4ec91459b01a4e514f60393c2feadb94f6a75378

diff --git a/model.cc b/model.cc
index f4da330..70440f5 100644
--- a/model.cc
+++ b/model.cc
@@ -4,20 +4,13 @@
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
 #include "common.h"
 
 #define INITIAL_THREAD_ID	0
 
 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()
 	:
 	/* Initialize default scheduler */
@@ -31,6 +24,9 @@ ModelChecker::ModelChecker()
 	diverge(NULL),
 	nextThread(THREAD_ID_T_NONE),
 	action_trace(new action_list_t()),
+	thread_map(new std::map<int, class Thread *>),
+	obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
+	thrd_last_action(new std::vector<ModelAction *>(1)),
 	node_stack(new NodeStack()),
 	next_backtrack(NULL)
 {
@@ -39,12 +35,13 @@ ModelChecker::ModelChecker()
 ModelChecker::~ModelChecker()
 {
 	std::map<int, class Thread *>::iterator it;
-	for (it = thread_map.begin(); it != thread_map.end(); it++)
+	for (it = thread_map->begin(); it != thread_map->end(); it++)
 		delete (*it).second;
-	thread_map.clear();
+	delete thread_map;
 
+	delete obj_thrd_map;
 	delete action_trace;
-
+	delete thrd_last_action;
 	delete node_stack;
 	delete scheduler;
 }
@@ -52,19 +49,13 @@ ModelChecker::~ModelChecker()
 void ModelChecker::reset_to_initial_state()
 {
 	DEBUG("+++ Resetting to initial state +++\n");
-	std::map<int, class Thread *>::iterator it;
-	for (it = thread_map.begin(); it != thread_map.end(); it++)
-		delete (*it).second;
-	thread_map.clear();
-	delete action_trace;
-	action_trace = new action_list_t();
 	node_stack->reset_execution();
 	current_action = NULL;
 	next_thread_id = INITIAL_THREAD_ID;
 	used_sequence_numbers = 0;
 	nextThread = 0;
 	next_backtrack = NULL;
-	/* scheduler reset ? */
+	snapshotObject->backTrackBeforeStep(0);
 }
 
 thread_id_t ModelChecker::get_next_id()
@@ -72,6 +63,11 @@ thread_id_t ModelChecker::get_next_id()
 	return next_thread_id++;
 }
 
+int ModelChecker::get_num_threads()
+{
+	return next_thread_id;
+}
+
 int ModelChecker::get_next_seq_num()
 {
 	return ++used_sequence_numbers;
@@ -82,7 +78,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);
 
@@ -216,6 +212,14 @@ void ModelChecker::check_current_action(void)
 	}
 
 	curr = node_stack->explore_action(curr);
+	curr->create_cv(get_parent_action(curr->get_tid()));
+
+	/* Assign 'creation' parent */
+	if (curr->get_type() == THREAD_CREATE) {
+		Thread *th = (Thread *)curr->get_location();
+		th->set_creation(curr);
+	}
+
 	nextThread = get_next_replay_thread();
 
 	currnode = curr->get_node();
@@ -225,14 +229,43 @@ void ModelChecker::check_current_action(void)
 			next_backtrack = curr;
 
 	set_backtracking(curr);
-	this->action_trace->push_back(curr);
+
+	add_action_to_lists(curr);
+}
+
+void ModelChecker::add_action_to_lists(ModelAction *act)
+{
+	action_trace->push_back(act);
+
+	std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
+	if (id_to_int(act->get_tid()) >= (int)vec->size())
+		vec->resize(next_thread_id);
+	(*vec)[id_to_int(act->get_tid())].push_back(act);
+
+	(*thrd_last_action)[id_to_int(act->get_tid())] = act;
+}
+
+ModelAction * ModelChecker::get_last_action(thread_id_t tid)
+{
+	int nthreads = get_num_threads();
+	if ((int)thrd_last_action->size() < nthreads)
+		thrd_last_action->resize(nthreads);
+	return (*thrd_last_action)[id_to_int(tid)];
+}
+
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+{
+	ModelAction *parent = get_last_action(tid);
+	if (!parent)
+		parent = get_thread(tid)->get_creation();
+	return parent;
 }
 
 void ModelChecker::print_summary(void)
 {
 	printf("\n");
 	printf("Number of executions: %d\n", num_executions);
-	printf("Total nodes created: %d\n", Node::get_total_nodes());
+	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 
 	scheduler->print();
 
@@ -255,7 +288,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;
 }