X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=3716d78838ba26ab694ef6faca6d66aa283b1b04;hb=11265e873a6618952820f76da4d702a6485b4678;hp=86d28ec0bfc4119b16f0c5c0eba62c34d05ea3d5;hpb=5734b17b928d722e2c6a37c4e152c0dcbf58175d;p=c11tester.git

diff --git a/model.cc b/model.cc
index 86d28ec0..3716d788 100644
--- a/model.cc
+++ b/model.cc
@@ -26,6 +26,7 @@ ModelChecker::ModelChecker()
 	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)
 {
@@ -40,6 +41,7 @@ ModelChecker::~ModelChecker()
 
 	delete obj_thrd_map;
 	delete action_trace;
+	delete thrd_last_action;
 	delete node_stack;
 	delete scheduler;
 }
@@ -83,7 +85,7 @@ Thread * ModelChecker::schedule_next_thread()
 	return t;
 }
 
-/*
+/**
  * get_next_replay_thread() - Choose the next thread in the replay sequence
  *
  * If we've reached the 'diverge' point, then we pick a thread from the
@@ -152,7 +154,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 	action_list_t::reverse_iterator rit;
 	for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 		ModelAction *prev = *rit;
-		if (act->is_dependent(prev))
+		if (act->is_synchronizing(prev))
 			return prev;
 	}
 	return NULL;
@@ -210,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();
@@ -219,19 +229,43 @@ void ModelChecker::check_current_action(void)
 			next_backtrack = curr;
 
 	set_backtracking(curr);
-	this->action_trace->push_back(curr);
 
-	std::vector<action_list_t> *vec = &(*obj_thrd_map)[curr->get_location()];
-	if (id_to_int(curr->get_tid()) >= (int)vec->size())
+	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(curr->get_tid())].push_back(curr);
+	(*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();