X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=62e75205e4ee9681bcef321856c744978c9cc5c1;hp=66ca8be3fdc89fa5014d8787819a657576cf138b;hb=718fed530a17d55ab479921e8dffebea4f98cbdf;hpb=c9e8710d3fc3e6915676c088511c9ff37c023de7

diff --git a/model.cc b/model.cc
index 66ca8be3..62e75205 100644
--- a/model.cc
+++ b/model.cc
@@ -38,7 +38,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
 	too_many_reads(false),
-	asserted(false)
+	asserted(false),
+	bad_synchronization(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -80,6 +81,7 @@ void ModelChecker::reset_to_initial_state()
 	node_stack->reset_execution();
 	failed_promise = false;
 	too_many_reads = false;
+	bad_synchronization = false;
 	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
@@ -334,7 +336,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			bool r_status = false;
 
 			if (!second_part_of_rmw) {
-				check_recency(curr);
+				check_recency(curr, reads_from);
 				r_status = r_modification_order(curr, reads_from);
 			}
 
@@ -374,8 +376,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  *
  * The unlock operation has to re-enable all of the threads that are
  * waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
  */
-void ModelChecker::process_mutex(ModelAction *curr) {
+bool ModelChecker::process_mutex(ModelAction *curr) {
 	std::mutex *mutex = (std::mutex *)curr->get_location();
 	struct std::mutex_state *state = mutex->get_state();
 	switch (curr->get_type()) {
@@ -397,8 +401,10 @@ void ModelChecker::process_mutex(ModelAction *curr) {
 		state->islocked = true;
 		ModelAction *unlock = get_last_unlock(curr);
 		//synchronize with the previous unlock statement
-		if (unlock != NULL)
+		if (unlock != NULL) {
 			curr->synchronize_with(unlock);
+			return true;
+		}
 		break;
 	}
 	case ATOMIC_UNLOCK: {
@@ -416,6 +422,7 @@ void ModelChecker::process_mutex(ModelAction *curr) {
 	default:
 		ASSERT(0);
 	}
+	return false;
 }
 
 /**
@@ -518,7 +525,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 	if (curr->is_rmwc() || curr->is_rmw()) {
 		newcurr = process_rmw(curr);
 		delete curr;
-		compute_promises(newcurr);
+
+		if (newcurr->is_rmw())
+			compute_promises(newcurr);
 		return newcurr;
 	}
 
@@ -535,8 +544,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		delete curr;
 
 		/* If we have diverged, we need to reset the clock vector. */
-		if (diverge == NULL)
+		if (diverge == NULL) {
 			newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+		}
 	} else {
 		newcurr = curr;
 		/*
@@ -608,6 +618,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		build_reads_from_past(curr);
 	curr = newcurr;
 
+	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
 	while (!work_queue.empty()) {
@@ -617,20 +628,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		switch (work.type) {
 		case WORK_CHECK_CURR_ACTION: {
 			ModelAction *act = work.action;
-			bool updated = false;
+			bool update = false; /* update this location's release seq's */
+			bool update_all = false; /* update all release seq's */
 
-			process_thread_action(curr);
+			if (process_thread_action(curr))
+				update_all = true;
 
 			if (act->is_read() && process_read(act, second_part_of_rmw))
-				updated = true;
+				update = true;
 
 			if (act->is_write() && process_write(act))
-				updated = true;
+				update = true;
 
-			if (act->is_mutex_op())
-				process_mutex(act);
+			if (act->is_mutex_op() && process_mutex(act))
+				update_all = true;
 
-			if (updated)
+			if (update_all)
+				work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+			else if (update)
 				work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
 			break;
 		}
@@ -650,6 +665,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 				if (w_modification_order(act))
 					updated = true;
 			}
+			mo_graph->commitChanges();
 
 			if (updated)
 				work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
@@ -713,6 +729,9 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @return whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
+	if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
+		DEBUG("Infeasible: RMW violation\n");
+
 	return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }
 
@@ -726,10 +745,12 @@ bool ModelChecker::isfeasibleotherthanRMW() {
 			DEBUG("Infeasible: failed promise\n");
 		if (too_many_reads)
 			DEBUG("Infeasible: too many reads\n");
+		if (bad_synchronization)
+			DEBUG("Infeasible: bad synchronization ordering\n");
 		if (promises_expired())
 			DEBUG("Infeasible: promises expired\n");
 	}
-	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -763,23 +784,21 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  *
  * If so, we decide that the execution is no longer feasible.
  */
-void ModelChecker::check_recency(ModelAction *curr) {
+void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
 	if (params.maxreads != 0) {
+
 		if (curr->get_node()->get_read_from_size() <= 1)
 			return;
-
 		//Must make sure that execution is currently feasible...  We could
 		//accidentally clear by rolling back
 		if (!isfeasible())
 			return;
-
 		std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 		int tid = id_to_int(curr->get_tid());
 
 		/* Skip checks */
 		if ((int)thrd_lists->size() <= tid)
 			return;
-
 		action_list_t *list = &(*thrd_lists)[tid];
 
 		action_list_t::reverse_iterator rit = list->rbegin();
@@ -798,17 +817,18 @@ void ModelChecker::check_recency(ModelAction *curr) {
 			ModelAction *act = *rit;
 			if (!act->is_read())
 				return;
-			if (act->get_reads_from() != curr->get_reads_from())
+			
+			if (act->get_reads_from() != rf)
 				return;
 			if (act->get_node()->get_read_from_size() <= 1)
 				return;
 		}
-
 		for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
 			//Get write
 			const ModelAction * write = curr->get_node()->get_read_from_at(i);
+
 			//Need a different write
-			if (write==curr->get_reads_from())
+			if (write==rf)
 				continue;
 
 			/* Test to see whether this is a feasible write to read from*/
@@ -1098,6 +1118,10 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  */
 bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
+	/* Only check for release sequences if there are no cycles */
+	if (mo_graph->checkForCycles())
+		return false;
+
 	while (rf) {
 		ASSERT(rf->is_write());
 
@@ -1161,7 +1185,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 		bool future_ordered = false;
 
 		ModelAction *last = get_last_action(int_to_id(i));
-		if (last && rf->happens_before(last))
+		if (last && (rf->happens_before(last) ||
+				last->get_type() == THREAD_FINISH))
 			future_ordered = true;
 
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -1258,8 +1283,10 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		complete = release_seq_head(rf, &release_heads);
 		for (unsigned int i = 0; i < release_heads.size(); i++) {
 			if (!act->has_synchronized_with(release_heads[i])) {
-				updated = true;
-				act->synchronize_with(release_heads[i]);
+				if (act->synchronize_with(release_heads[i]))
+					updated = true;
+				else
+					set_bad_synchronization();
 			}
 		}
 
@@ -1268,9 +1295,9 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 			work_queue->push_back(MOEdgeWorkEntry(act));
 
 			/* propagate synchronization to later actions */
-			action_list_t::reverse_iterator it = action_trace->rbegin();
-			for (; (*it) != act; it++) {
-				ModelAction *propagate = *it;
+			action_list_t::reverse_iterator rit = action_trace->rbegin();
+			for (; (*rit) != act; rit++) {
+				ModelAction *propagate = *rit;
 				if (act->happens_before(propagate)) {
 					propagate->synchronize_with(act);
 					/* Re-check 'propagate' for mo_graph edges */
@@ -1402,16 +1429,19 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
 			ModelAction *read = promise->get_action();
-			read->read_from(write);
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
+			read->read_from(write);
 			//First fix up the modification order for actions that happened
 			//before the read
 			r_modification_order(read, write);
 			//Next fix up the modification order for actions that happened
 			//after the read.
 			post_r_modification_order(read, write);
+			//Make sure the promise's value matches the write's value
+			ASSERT(promise->get_value() == write->get_value());
+
 			promises->erase(promises->begin() + promise_index);
 			resolved = true;
 		} else
@@ -1617,6 +1647,7 @@ bool ModelChecker::take_step() {
 
 			priv->nextThread = check_current_action(priv->current_action);
 			priv->current_action = NULL;
+
 			if (curr->is_blocked() || curr->is_complete())
 				scheduler->remove_thread(curr);
 		} else {