X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=3e25dc6f0171d5efce0480504ec4c4ba14190c4b;hb=85c090982c2a8dd6e236aa8f3d0a79f974ab9603;hp=077cc53ea9cd252365214cb2a424a0da8476002b;hpb=eb8e9f61a400856421465d95ac52d9cffed2a491;p=model-checker.git

diff --git a/model.cc b/model.cc
index 077cc53..3e25dc6 100644
--- a/model.cc
+++ b/model.cc
@@ -6,6 +6,7 @@
 #include "schedule.h"
 #include "snapshot-interface.h"
 #include "common.h"
+#include "clockvector.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -25,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()),
@@ -36,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;
@@ -77,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;
 }
@@ -123,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");
@@ -195,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();
@@ -204,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;
 
@@ -239,11 +241,18 @@ void ModelChecker::check_current_action(void)
 
 	tmp = node_stack->explore_action(curr);
 	if (tmp) {
-		/* Discard duplicate ModelAction */
+		/* Discard duplicate ModelAction; use action from NodeStack */
 		delete curr;
 		curr = tmp;
 	} else {
+		/*
+		 * Perform one-time actions when pushing new ModelAction onto
+		 * NodeStack
+		 */
 		curr->create_cv(get_parent_action(curr->get_tid()));
+		/* Build may_read_from set */
+		if (curr->is_read())
+			build_reads_from_past(curr);
 	}
 
 	/* Assign 'creation' parent */
@@ -254,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)
@@ -265,12 +274,13 @@ void ModelChecker::check_current_action(void)
 	add_action_to_lists(curr);
 }
 
-
 /**
- * Adds an action to the per-object, per-thread action vector.
+ * Performs various bookkeeping operations for the current ModelAction. For
+ * instance, adds action to the per-object, per-thread action vector and to the
+ * action trace list of all thread actions.
+ *
  * @param act is the ModelAction to add.
  */
-
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
 	action_trace->push_back(act);
@@ -299,19 +309,45 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 	return parent;
 }
 
-void ModelChecker::print_summary(void)
+/**
+ * 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"
+ * relationship.
+ * @param curr is the current ModelAction that we are exploring; it must be a
+ * 'read' operation.
+ */
+void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
-	printf("\n");
-	printf("Number of executions: %d\n", num_executions);
-	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
-	scheduler->print();
-
-	print_list(action_trace);
-	printf("\n");
+	std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+	unsigned int i;
+
+	ASSERT(curr->is_read());
+
+	for (i = 0; i < thrd_lists->size(); i++) {
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+
+			/* Only consider 'write' actions */
+			if (!act->is_write())
+				continue;
+
+			DEBUG("Adding action to may_read_from:\n");
+			if (DBG_ENABLED()) {
+				act->print();
+				curr->print();
+			}
+			curr->get_node()->add_read_from(act);
+
+			/* Include at most one act that "happens before" curr */
+			if (act->happens_before(curr))
+				break;
+		}
+	}
 }
 
-void ModelChecker::print_list(action_list_t *list)
+static void print_list(action_list_t *list)
 {
 	action_list_t::iterator it;
 
@@ -324,6 +360,18 @@ void ModelChecker::print_list(action_list_t *list)
 	printf("---------------------------------------------------------------------\n");
 }
 
+void ModelChecker::print_summary(void)
+{
+	printf("\n");
+	printf("Number of executions: %d\n", num_executions);
+	printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+
+	scheduler->print();
+
+	print_list(action_trace);
+	printf("\n");
+}
+
 int ModelChecker::add_thread(Thread *t)
 {
 	(*thread_map)[id_to_int(t->get_id())] = t;