X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=41e4421c52f3c8b8c932330523771c7a32622649;hb=38dbc133c5e2712828cf13e17d05331d2b48dcf2;hp=93e06d0262de2b4c4d93bf8c9207f018b710cb3e;hpb=6cb1abb7f1f69690ecf78a293744204980912a7d;p=model-checker.git

diff --git a/model.cc b/model.cc
index 93e06d0..41e4421 100644
--- a/model.cc
+++ b/model.cc
@@ -26,7 +26,7 @@ ModelChecker::ModelChecker()
 	diverge(NULL),
 	nextThread(THREAD_ID_T_NONE),
 	action_trace(new action_list_t()),
-	thread_map(new std::map<int, class Thread *>),
+	thread_map(new std::map<int, 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()),
@@ -37,7 +37,7 @@ ModelChecker::ModelChecker()
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-	std::map<int, class Thread *>::iterator it;
+	std::map<int, Thread *>::iterator it;
 	for (it = thread_map->begin(); it != thread_map->end(); it++)
 		delete (*it).second;
 	delete thread_map;
@@ -78,7 +78,7 @@ int ModelChecker::get_num_threads()
 }
 
 /** @returns a sequence number for a new ModelAction */
-int ModelChecker::get_next_seq_num()
+modelclock_t ModelChecker::get_next_seq_num()
 {
 	return ++used_sequence_numbers;
 }
@@ -124,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
-		Node *node = next->get_node();
+		Node *node = next->get_node()->get_parent();
 
 		/* Reached divergence point */
 		DEBUG("*** Divergence point ***\n");
@@ -196,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	if (prev == NULL)
 		return;
 
-	node = prev->get_node();
+	node = prev->get_node()->get_parent();
 
 	while (!node->is_enabled(t))
 		t = t->get_parent();
@@ -205,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	if (node->has_been_explored(t->get_id()))
 		return;
 
+	/* Cache the latest backtracking point */
 	if (!next_backtrack || *prev > *next_backtrack)
 		next_backtrack = prev;
 
@@ -262,7 +263,7 @@ void ModelChecker::check_current_action(void)
 
 	nextThread = get_next_replay_thread();
 
-	currnode = curr->get_node();
+	currnode = curr->get_node()->get_parent();
 
 	if (!currnode->backtrack_empty())
 		if (!next_backtrack || *curr > *next_backtrack)
@@ -308,6 +309,10 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 	return parent;
 }
 
+ClockVector * ModelChecker::get_cv(thread_id_t tid) {
+	return get_parent_action(tid)->get_cv();
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"
@@ -322,6 +327,9 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
 	ASSERT(curr->is_read());
 
+	/* Track whether this object has been initialized */
+	bool initialized = false;
+
 	for (i = 0; i < thrd_lists->size(); i++) {
 		action_list_t *list = &(*thrd_lists)[i];
 		action_list_t::reverse_iterator rit;
@@ -339,11 +347,28 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			}
 			curr->get_node()->add_read_from(act);
 
-			/* Include at most one act that "happens before" curr */
-			if (act->happens_before(curr))
+			/* Include at most one act per-thread that "happens before" curr */
+			if (act->happens_before(curr)) {
+				initialized = true;
 				break;
+			}
 		}
 	}
+
+	if (!initialized) {
+		/* TODO: need a more informative way of reporting errors */
+		printf("ERROR: may read from uninitialized atomic\n");
+	}
+
+	if (DBG_ENABLED() || !initialized) {
+		printf("Reached read action:\n");
+		curr->print();
+		printf("Printing may_read_from\n");
+		curr->get_node()->print_may_read_from();
+		printf("End printing may_read_from\n");
+	}
+
+	ASSERT(initialized);
 }
 
 static void print_list(action_list_t *list)