X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=da982d0db415395ed2be39e9dfcf3b34f74c1efe;hp=2aaa1c26dbea3ad9e78720683635a117d83243f1;hb=c2d7fa973e562c194eb732d8dc58ab7659b7a2ee;hpb=55eb20c50ec656d385fb6e94c01aea55e9514917

diff --git a/model.cc b/model.cc
index 2aaa1c2..da982d0 100644
--- a/model.cc
+++ b/model.cc
@@ -218,7 +218,8 @@ void ModelChecker::execute_sleep_set() {
 	for(unsigned int i=0;i<get_num_threads();i++) {
 		thread_id_t tid=int_to_id(i);
 		Thread *thr=get_thread(tid);
-		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+				 thr->get_pending() == NULL ) {
 			thr->set_state(THREAD_RUNNING);
 			scheduler->next_thread(thr);
 			Thread::swap(&system_context, thr);
@@ -235,7 +236,7 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) {
 		Thread *thr=get_thread(tid);
 		if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
 			ModelAction *pending_act=thr->get_pending();
-			if (pending_act->could_synchronize_with(curr)) {
+			if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
 				//Remove this thread from sleep set
 				scheduler->remove_sleep(thr);
 			}
@@ -271,8 +272,10 @@ bool ModelChecker::next_execution()
 			pending_rel_seqs->size());
 
 
-	if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+	if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+		checkDataRaces();
 		print_summary();
+	}
 
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
@@ -383,8 +386,12 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	for(int i = low_tid; i < high_tid; i++) {
 		thread_id_t tid = int_to_id(i);
 
+		/* Make sure this thread can be enabled here. */
+		if (i >= node->get_num_threads())
+			break;
+
 		/* Don't backtrack into a point where the thread is disabled or sleeping. */
-		if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+		if (node->enabled_status(tid)!=THREAD_ENABLED)
 			continue;
 	
 		/* Check if this has been explored already */
@@ -441,7 +448,7 @@ ModelAction * ModelChecker::get_next_backtrack()
  */
 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 {
-	uint64_t value;
+	uint64_t value = VALUE_NONE;
 	bool updated = false;
 	while (true) {
 		const ModelAction *reads_from = curr->get_node()->get_read_from();
@@ -744,41 +751,46 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
  * initializing clock vectors, and computing the promises to fulfill.
  *
  * @param curr The current action, as passed from the user context; may be
- * freed/invalidated after the execution of this function
- * @return The current action, as processed by the ModelChecker. Is only the
- * same as the parameter @a curr if this is a newly-explored action.
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
  */
-ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
 {
 	ModelAction *newcurr;
 
-	if (curr->is_rmwc() || curr->is_rmw()) {
-		newcurr = process_rmw(curr);
-		delete curr;
+	if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+		newcurr = process_rmw(*curr);
+		delete *curr;
 
 		if (newcurr->is_rmw())
 			compute_promises(newcurr);
-		return newcurr;
+
+		*curr = newcurr;
+		return false;
 	}
 
-	curr->set_seq_number(get_next_seq_num());
+	(*curr)->set_seq_number(get_next_seq_num());
 
-	newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
+	newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
 	if (newcurr) {
 		/* First restore type and order in case of RMW operation */
-		if (curr->is_rmwr())
-			newcurr->copy_typeandorder(curr);
+		if ((*curr)->is_rmwr())
+			newcurr->copy_typeandorder(*curr);
 
-		ASSERT(curr->get_location() == newcurr->get_location());
-		newcurr->copy_from_new(curr);
+		ASSERT((*curr)->get_location() == newcurr->get_location());
+		newcurr->copy_from_new(*curr);
 
 		/* Discard duplicate ModelAction; use action from NodeStack */
-		delete curr;
+		delete *curr;
 
 		/* Always compute new clock vector */
 		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+		*curr = newcurr;
+		return false; /* Action was explored previously */
 	} else {
-		newcurr = curr;
+		newcurr = *curr;
 
 		/* Always compute new clock vector */
 		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
@@ -795,8 +807,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		else if (newcurr->is_notify_one()) {
 			newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
 		}
+		return true; /* This was a new ModelAction */
 	}
-	return newcurr;
 }
 
 /**
@@ -854,18 +866,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		return get_next_thread(NULL);
 	}
 
-	ModelAction *newcurr = initialize_curr_action(curr);
+	bool newly_explored = initialize_curr_action(&curr);
 
 	wake_up_sleeping_actions(curr);
 
 	/* Add the action to lists before any other model-checking tasks */
 	if (!second_part_of_rmw)
-		add_action_to_lists(newcurr);
+		add_action_to_lists(curr);
 
 	/* Build may_read_from set for newly-created actions */
-	if (curr == newcurr && curr->is_read())
+	if (newly_explored && curr->is_read())
 		build_reads_from_past(curr);
-	curr = newcurr;
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
@@ -963,7 +974,7 @@ bool ModelChecker::promises_expired() {
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
-	return promises->size() == 0 && pending_rel_seqs->size() == 0;
+	return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
@@ -1086,7 +1097,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
 				ModelAction *act=*rit;
 				bool foundvalue = false;
 				for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-					if (act->get_node()->get_read_from_at(i)==write) {
+					if (act->get_node()->get_read_from_at(j)==write) {
 						foundvalue = true;
 						break;
 					}
@@ -1366,33 +1377,42 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
 	return true;
 }
 
-/** Arbitrary reads from the future are not allowed.  Section 29.3
- * part 9 places some constraints.  This method checks one result of constraint
- * constraint.  Others require compiler support. */
-bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ *   If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
 	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+	unsigned int i;
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		const ModelAction *write_after_read = NULL;
 
-	//Get write that follows reader action
-	action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
-	action_list_t::reverse_iterator rit;
-	ModelAction *first_write_after_read=NULL;
+		/* Iterate over actions in thread, starting from most recent */
+		action_list_t *list = &(*thrd_lists)[i];
+		action_list_t::reverse_iterator rit;
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
 
-	for (rit = list->rbegin(); rit != list->rend(); rit++) {
-		ModelAction *act = *rit;
-		if (act==reader)
-			break;
-		if (act->is_write())
-			first_write_after_read=act;
+			if (!reader->happens_before(act))
+				break;
+			else if (act->is_write())
+				write_after_read = act;
+			else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
+				write_after_read = act->get_reads_from();
+			}
+		}
+		
+		if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
+			return false;
 	}
-
-	if (first_write_after_read==NULL)
-		return true;
-
-	return !mo_graph->checkReachable(first_write_after_read, writer);
+	return true;
 }
 
-
-
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -1509,8 +1529,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 				continue;
 			}
 
-			/* Only writes can break release sequences */
-			if (!act->is_write())
+			/* Only non-RMW writes can break release sequences */
+			if (!act->is_write() || act->is_rmw())
 				continue;
 
 			/* Check modification order */
@@ -1815,8 +1835,9 @@ void ModelChecker::compute_promises(ModelAction *curr)
 				act->is_read() &&
 				!act->could_synchronize_with(curr) &&
 				!act->same_thread(curr) &&
+				act->get_location() == curr->get_location() &&
 				promise->get_value() == curr->get_value()) {
-			curr->get_node()->set_promise(i);
+			curr->get_node()->set_promise(i, act->is_rmw());
 		}
 	}
 }
@@ -1838,6 +1859,16 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 	}
 }
 
+void ModelChecker::check_promises_thread_disabled() {
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		if (promise->check_promise()) {
+			failed_promise = true;
+			return;
+		}
+	}
+}
+
 /** Checks promises in response to addition to modification order for threads.
  * Definitions:
  * pthread is the thread that performed the read that created the promise
@@ -1897,7 +1928,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 		if (promise->has_sync_thread(tid))
 			continue;
 		
-		if (mo_graph->checkReachable(promise->get_write(), write)) {
+		if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
 			if (promise->increment_threads(tid)) {
 				failed_promise = true;
 				return;
@@ -1993,6 +2024,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 	if (!initialized) {
 		/** @todo Need a more informative way of reporting errors. */
 		printf("ERROR: may read from uninitialized atomic\n");
+		set_assert();
 	}
 
 	if (DBG_ENABLED() || !initialized) {
@@ -2002,14 +2034,13 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 		curr->get_node()->print_may_read_from();
 		printf("End printing may_read_from\n");
 	}
-
-	ASSERT(initialized);
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
 	while(true) {
 		Node *prevnode=write->get_node()->get_parent();
-		bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+		
+		bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
 		if (write->is_release()&&thread_sleep)
 			return true;
 		if (!write->is_rmw()) {