X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=fa4dcc6fd3976281633317152bd4450d636fcc0c;hp=94bc58b6c5a010254ac34a509afe1a135fa1247d;hb=2daff868a7ef4f6235c2776b746cec9947a87b13;hpb=dbee0c57f6edff31aafb79d6e956f1408bbb8fb8

diff --git a/model.cc b/model.cc
index 94bc58b..fa4dcc6 100644
--- a/model.cc
+++ b/model.cc
@@ -263,10 +263,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			/* The next node will read from a different value. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_future_value()) {
-			/* The next node will try to read from a different future value. */
-			tid = next->get_tid();
-			node_stack->pop_restofstack(2);
 		} else if (nextnode->increment_relseq_break()) {
 			/* The next node will try to resolve a release sequence differently */
 			tid = next->get_tid();
@@ -487,8 +483,10 @@ void ModelChecker::record_stats()
 		stats.num_buggy_executions++;
 	else if (is_complete_execution())
 		stats.num_complete++;
-	else
+	else if (scheduler->all_threads_sleeping())
 		stats.num_redundant++;
+	else
+		ASSERT(false);
 }
 
 /** @brief Print execution stats */
@@ -842,42 +840,52 @@ ModelAction * ModelChecker::get_next_backtrack()
 }
 
 /**
- * Processes a read or rmw model action.
+ * Processes a read model action.
  * @param curr is the read model action to process.
- * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+bool ModelChecker::process_read(ModelAction *curr)
 {
+	Node *node = curr->get_node();
 	uint64_t value = VALUE_NONE;
 	bool updated = false;
 	while (true) {
-		const ModelAction *reads_from = curr->get_node()->get_read_from();
-		if (reads_from != NULL) {
-			mo_graph->startChanges();
-
-			value = reads_from->get_value();
-			bool r_status = false;
+		switch (node->get_read_from_status()) {
+		case READ_FROM_PAST: {
+			const ModelAction *rf = node->get_read_from_past();
+			ASSERT(rf);
 
-			if (!second_part_of_rmw) {
-				check_recency(curr, reads_from);
-				r_status = r_modification_order(curr, reads_from);
-			}
+			mo_graph->startChanges();
+			value = rf->get_value();
+			check_recency(curr, rf);
+			bool r_status = r_modification_order(curr, rf);
 
-			if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+			if (is_infeasible() && node->increment_read_from()) {
 				mo_graph->rollbackChanges();
 				priv->too_many_reads = false;
 				continue;
 			}
 
-			read_from(curr, reads_from);
+			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
 
 			updated |= r_status;
-		} else if (!second_part_of_rmw) {
+			break;
+		}
+		case READ_FROM_PROMISE: {
+			Promise *promise = curr->get_node()->get_read_from_promise();
+			promise->add_reader(curr);
+			value = promise->get_value();
+			curr->set_read_from_promise(promise);
+			mo_graph->startChanges();
+			updated = r_modification_order(curr, promise);
+			mo_graph->commitChanges();
+			break;
+		}
+		case READ_FROM_FUTURE: {
 			/* Read from future value */
-			struct future_value fv = curr->get_node()->get_future_value();
+			struct future_value fv = node->get_future_value();
 			Promise *promise = new Promise(curr, fv);
 			value = fv.value;
 			curr->set_read_from_promise(promise);
@@ -885,6 +893,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			mo_graph->startChanges();
 			updated = r_modification_order(curr, promise);
 			mo_graph->commitChanges();
+			break;
+		}
+		default:
+			ASSERT(false);
 		}
 		get_thread(curr)->set_return_value(value);
 		return updated;
@@ -1339,14 +1351,19 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		ModelAction *reader = promise->get_action();
-		if (reader->get_tid() != blocker->get_id())
-			continue;
 		if (!promise->thread_is_available(waiting->get_id()))
 			continue;
-		if (promise->eliminate_thread(waiting->get_id())) {
-			/* Promise has failed */
-			priv->failed_promise = true;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			ModelAction *reader = promise->get_reader(j);
+			if (reader->get_tid() != blocker->get_id())
+				continue;
+			if (promise->eliminate_thread(waiting->get_id())) {
+				/* Promise has failed */
+				priv->failed_promise = true;
+			} else {
+				/* Only eliminate the 'waiting' thread once */
+				return;
+			}
 		}
 	}
 }
@@ -1437,7 +1454,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 			if (process_thread_action(curr))
 				update_all = true;
 
-			if (act->is_read() && process_read(act, second_part_of_rmw))
+			if (act->is_read() && !second_part_of_rmw && process_read(act))
 				update = true;
 
 			if (act->is_write() && process_write(act))
@@ -1506,7 +1523,6 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 	if ((parnode && !parnode->backtrack_empty()) ||
 			 !currnode->misc_empty() ||
 			 !currnode->read_from_empty() ||
-			 !currnode->future_value_empty() ||
 			 !currnode->promise_empty() ||
 			 !currnode->relseq_break_empty()) {
 		set_latest_backtrack(curr);
@@ -1613,7 +1629,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 {
 	if (params.maxreads != 0) {
-		if (curr->get_node()->get_read_from_size() <= 1)
+		if (curr->get_node()->get_read_from_past_size() <= 1)
 			return;
 		//Must make sure that execution is currently feasible...  We could
 		//accidentally clear by rolling back
@@ -1646,12 +1662,12 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 
 			if (act->get_reads_from() != rf)
 				return;
-			if (act->get_node()->get_read_from_size() <= 1)
+			if (act->get_node()->get_read_from_past_size() <= 1)
 				return;
 		}
-		for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
+		for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
 			/* Get write */
-			const ModelAction *write = curr->get_node()->get_read_from_at(i);
+			const ModelAction *write = curr->get_node()->get_read_from_past(i);
 
 			/* Need a different write */
 			if (write == rf)
@@ -1669,8 +1685,8 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 			for (int loop = count; loop > 0; loop--, rit++) {
 				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(j) == write) {
+				for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
+					if (act->get_node()->get_read_from_past(j) == write) {
 						foundvalue = true;
 						break;
 					}
@@ -1765,13 +1781,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
-					const ModelAction *prevreadfrom = act->get_reads_from();
-					//if the previous read is unresolved, keep going...
-					if (prevreadfrom == NULL)
-						continue;
-
-					if (!prevreadfrom->equals(rf)) {
-						added = mo_graph->addEdge(prevreadfrom, rf) || added;
+					const ModelAction *prevrf = act->get_reads_from();
+					const Promise *prevrf_promise = act->get_reads_from_promise();
+					if (prevrf) {
+						if (!prevrf->equals(rf))
+							added = mo_graph->addEdge(prevrf, rf) || added;
+					} else if (!prevrf_promise->equals(rf)) {
+						added = mo_graph->addEdge(prevrf_promise, rf) || added;
 					}
 				}
 				break;
@@ -2443,15 +2459,17 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
-			ModelAction *read = promise->get_action();
-			read_from(read, write);
+			for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+				ModelAction *read = promise->get_reader(j);
+				read_from(read, write);
+				actions_to_check.push_back(read);
+			}
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->is_compatible(write));
-			mo_graph->resolvePromise(read, write, &mustResolve);
+			mo_graph->resolvePromise(promise, write, &mustResolve);
 
 			resolved.push_back(promise);
 			promises->erase(promises->begin() + promise_index);
-			actions_to_check.push_back(read);
 
 			haveResolved = true;
 		} else
@@ -2486,14 +2504,20 @@ void ModelChecker::compute_promises(ModelAction *curr)
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
-		ASSERT(act->is_read());
-		if (!act->happens_before(curr) &&
-				!act->could_synchronize_with(curr) &&
-				promise->is_compatible(curr) &&
-				promise->get_value() == curr->get_value()) {
-			curr->get_node()->set_promise(i, act->is_rmw());
+		if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+			continue;
+
+		bool satisfy = true;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *act = promise->get_reader(j);
+			if (act->happens_before(curr) ||
+					act->could_synchronize_with(curr)) {
+				satisfy = false;
+				break;
+			}
 		}
+		if (satisfy)
+			curr->get_node()->set_promise(i);
 	}
 }
 
@@ -2502,13 +2526,17 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
-		if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
-				merge_cv->synchronized_since(act)) {
-			if (promise->eliminate_thread(tid)) {
-				//Promise has failed
-				priv->failed_promise = true;
-				return;
+		if (!promise->thread_is_available(tid))
+			continue;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *act = promise->get_reader(j);
+			if ((!old_cv || !old_cv->synchronized_since(act)) &&
+					merge_cv->synchronized_since(act)) {
+				if (promise->eliminate_thread(tid)) {
+					/* Promise has failed */
+					priv->failed_promise = true;
+					return;
+				}
 			}
 		}
 	}
@@ -2545,15 +2573,20 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *pread = promise->get_action();
 
 		// Is this promise on the same location?
-		if (!pread->same_var(write))
+		if (promise->get_value() != write->get_value())
 			continue;
 
-		if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
-			priv->failed_promise = true;
-			return;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *pread = promise->get_reader(j);
+			if (!pread->happens_before(act))
+			       continue;
+			if (mo_graph->checkPromise(write, promise)) {
+				priv->failed_promise = true;
+				return;
+			}
+			break;
 		}
 
 		// Don't do any lookups twice for the same thread
@@ -2635,7 +2668,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 				mo_graph->startChanges();
 				r_modification_order(curr, act);
 				if (!is_infeasible())
-					curr->get_node()->add_read_from(act);
+					curr->get_node()->add_read_from_past(act);
 				mo_graph->rollbackChanges();
 			}
 
@@ -2648,21 +2681,19 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 	/* Inherit existing, promised future values */
 	for (i = 0; i < promises->size(); i++) {
 		const Promise *promise = (*promises)[i];
-		const ModelAction *promise_read = promise->get_action();
+		const ModelAction *promise_read = promise->get_reader(0);
 		if (promise_read->same_var(curr)) {
 			/* Only add feasible future-values */
 			mo_graph->startChanges();
 			r_modification_order(curr, promise);
-			if (!is_infeasible()) {
-				const struct future_value fv = promise->get_fv();
-				curr->get_node()->add_future_value(fv);
-			}
+			if (!is_infeasible())
+				curr->get_node()->add_read_from_promise(promise_read);
 			mo_graph->rollbackChanges();
 		}
 	}
 
 	/* We may find no valid may-read-from only if the execution is doomed */
-	if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
+	if (!curr->get_node()->read_from_size()) {
 		priv->no_valid_reads = true;
 		set_assert();
 	}
@@ -2670,9 +2701,9 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 	if (DBG_ENABLED()) {
 		model_print("Reached read action:\n");
 		curr->print();
-		model_print("Printing may_read_from\n");
-		curr->get_node()->print_may_read_from();
-		model_print("End printing may_read_from\n");
+		model_print("Printing read_from_past\n");
+		curr->get_node()->print_read_from_past();
+		model_print("End printing read_from_past\n");
 	}
 }
 
@@ -2763,9 +2794,11 @@ void ModelChecker::print_summary() const
 #endif
 
 	model_print("Execution %d:", stats.num_total);
-	if (isfeasibleprefix())
+	if (isfeasibleprefix()) {
+		if (scheduler->all_threads_sleeping())
+			model_print(" SLEEP-SET REDUNDANT");
 		model_print("\n");
-	else
+	} else
 		print_infeasibility(" INFEASIBLE");
 	print_list(action_trace);
 	model_print("\n");
@@ -2811,6 +2844,26 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const
 	return get_thread(act->get_tid());
 }
 
+/**
+ * @brief Get a Promise's "promise number"
+ *
+ * A "promise number" is an index number that is unique to a promise, valid
+ * only for a specific snapshot of an execution trace. Promises may come and go
+ * as they are generated an resolved, so an index only retains meaning for the
+ * current snapshot.
+ *
+ * @param promise The Promise to check
+ * @return The promise index, if the promise still is valid; otherwise -1
+ */
+int ModelChecker::get_promise_number(const Promise *promise) const
+{
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i] == promise)
+			return i;
+	/* Not found */
+	return -1;
+}
+
 /**
  * @brief Check if a Thread is currently enabled
  * @param t The Thread to check