X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=775b796f167d68ee8394a0e828b0791e122a4937;hb=dd7f61668db41bed95b0cbf43f0b2cad5cd41060;hp=101a5f0864cb6bc7472ee40e58e8b33b36d3f726;hpb=ffc110b3aaa80564dbf85f3c6a9049efd40571f1;p=model-checker.git

diff --git a/model.cc b/model.cc
index 101a5f0..775b796 100644
--- a/model.cc
+++ b/model.cc
@@ -235,7 +235,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);
 			}
@@ -441,7 +441,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();
@@ -498,8 +498,17 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  * @return True if synchronization was updated; false otherwise
  */
 bool ModelChecker::process_mutex(ModelAction *curr) {
-	std::mutex *mutex = (std::mutex *)curr->get_location();
-	struct std::mutex_state *state = mutex->get_state();
+	std::mutex *mutex=NULL;
+	struct std::mutex_state *state=NULL;
+
+	if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+		mutex = (std::mutex *)curr->get_location();
+		state = mutex->get_state();
+	} else if(curr->is_wait()) {
+		mutex = (std::mutex *)curr->get_value();
+		state = mutex->get_state();
+	}
+
 	switch (curr->get_type()) {
 	case ATOMIC_TRYLOCK: {
 		bool success = !state->islocked;
@@ -847,7 +856,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 	ModelAction *newcurr = initialize_curr_action(curr);
 
-	wake_up_sleeping_actions(curr);
+	wake_up_sleeping_actions(newcurr);
 
 	/* Add the action to lists before any other model-checking tasks */
 	if (!second_part_of_rmw)
@@ -1357,32 +1366,40 @@ 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;
 
-	//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;
-
-	for (rit = list->rbegin(); rit != list->rend(); rit++) {
-		ModelAction *act = *rit;
-		if (act==reader)
-			break;
-		if (act->is_write())
-			first_write_after_read=act;
-	}
+	/* Iterate over all threads */
+	for (i = 0; i < thrd_lists->size(); i++) {
+		ModelAction *write_after_read = NULL;
 
-	if (first_write_after_read==NULL)
-		return true;
+		/* 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;
 
-	return !mo_graph->checkReachable(first_write_after_read, writer);
-}
+			if (!reader->happens_before(act))
+				break;
+			else if (act->is_write())
+				write_after_read = act;
+		}
 
+		if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+			return false;
+	}
 
+	return true;
+}
 
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
@@ -1500,8 +1517,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 */
@@ -1657,6 +1674,20 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 	if ((int)thrd_last_action->size() <= tid)
 		thrd_last_action->resize(get_num_threads());
 	(*thrd_last_action)[tid] = act;
+
+	if (act->is_wait()) {
+		void *mutex_loc=(void *) act->get_value();
+		obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+	
+		std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+		if (tid >= (int)vec->size())
+			vec->resize(priv->next_thread_id);
+		(*vec)[tid].push_back(act);
+
+		if ((int)thrd_last_action->size() <= tid)
+			thrd_last_action->resize(get_num_threads());
+		(*thrd_last_action)[tid] = act;
+	}
 }
 
 /**
@@ -1708,7 +1739,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
 	/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
 	for (rit = list->rbegin(); rit != list->rend(); rit++)
-		if ((*rit)->is_unlock())
+		if ((*rit)->is_unlock() || (*rit)->is_wait())
 			return *rit;
 	return NULL;
 }
@@ -1792,6 +1823,7 @@ 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);
 		}
@@ -1970,6 +2002,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) {
@@ -1979,8 +2012,6 @@ 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) {