X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=08096528bddc326b04dbe31b0772b1fcfb6458f6;hp=ef9bed305fc0295af447e25365cccd6a8f2399a3;hb=1cdcdc24156572a63fd8261a7a3dd2f04ca6648c;hpb=76e48f210747b7ef23387ffd7c33ea0009c1d922

diff --git a/model.cc b/model.cc
index ef9bed3..0809652 100644
--- a/model.cc
+++ b/model.cc
@@ -48,6 +48,7 @@ struct model_snapshot_members {
 		stats(),
 		failed_promise(false),
 		too_many_reads(false),
+		no_valid_reads(false),
 		bad_synchronization(false),
 		asserted(false)
 	{ }
@@ -66,6 +67,7 @@ struct model_snapshot_members {
 	struct execution_stats stats;
 	bool failed_promise;
 	bool too_many_reads;
+	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
 	bool bad_synchronization;
 	bool asserted;
@@ -294,7 +296,6 @@ void ModelChecker::execute_sleep_set()
 		thread_id_t tid = int_to_id(i);
 		Thread *thr = get_thread(tid);
 		if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
-			thr->set_state(THREAD_RUNNING);
 			scheduler->next_thread(thr);
 			Thread::swap(&system_context, thr);
 			priv->current_action->set_sleep_flag();
@@ -1387,6 +1388,8 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 		ptr += sprintf(ptr, "[failed promise]");
 	if (priv->too_many_reads)
 		ptr += sprintf(ptr, "[too many reads]");
+	if (priv->no_valid_reads)
+		ptr += sprintf(ptr, "[no valid reads-from]");
 	if (priv->bad_synchronization)
 		ptr += sprintf(ptr, "[bad sw ordering]");
 	if (promises_expired())
@@ -1415,6 +1418,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 bool ModelChecker::is_infeasible() const
 {
 	return mo_graph->checkForCycles() ||
+		priv->no_valid_reads ||
 		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||
@@ -1494,13 +1498,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 				continue;
 
 			/* Test to see whether this is a feasible write to read from */
-			mo_graph->startChanges();
-			r_modification_order(curr, write);
-			bool feasiblereadfrom = !is_infeasible();
-			mo_graph->rollbackChanges();
+			/** NOTE: all members of read-from set should be
+			 *  feasible, so we no longer check it here **/
 
-			if (!feasiblereadfrom)
-				continue;
 			rit = ritcopy;
 
 			bool feasiblewrite = true;
@@ -2473,14 +2473,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
 				allow_read = false;
 
-			if (allow_read)
-				curr->get_node()->add_read_from(act);
+			if (allow_read) {
+				/* Only add feasible reads */
+				mo_graph->startChanges();
+				r_modification_order(curr, act);
+				if (!is_infeasible())
+					curr->get_node()->add_read_from(act);
+				mo_graph->rollbackChanges();
+			}
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr))
 				break;
 		}
 	}
+	/* We may find no valid may-read-from only if the execution is doomed */
+	if (!curr->get_node()->get_read_from_size()) {
+		priv->no_valid_reads = true;
+		set_assert();
+	}
 
 	if (DBG_ENABLED()) {
 		model_print("Reached read action:\n");
@@ -2665,7 +2676,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 	DBG();
 	Thread *old = thread_current();
 	set_current_action(act);
-	old->set_state(THREAD_READY);
 	if (Thread::swap(old, &system_context) < 0) {
 		perror("swap threads");
 		exit(EXIT_FAILURE);
@@ -2733,13 +2743,10 @@ bool ModelChecker::take_step(ModelAction *curr)
 	if (!next_thrd)
 		return false;
 
-	next_thrd->set_state(THREAD_RUNNING);
-
 	if (next_thrd->get_pending() != NULL) {
 		/* restart a pending action */
 		set_current_action(next_thrd->get_pending());
 		next_thrd->set_pending(NULL);
-		next_thrd->set_state(THREAD_READY);
 		return true;
 	}