X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=0c201fd381aa239eeaa060d6e46f22aae9023579;hp=998059e2451e7e652d2493af3fc6785aad9ba542;hb=32b70968c21a1d21a41010f00c5f9a82a9fbdbd1;hpb=d5ec9d02d3ce4a92811a4515f808efcb0a1326b7

diff --git a/model.cc b/model.cc
index 998059e2..0c201fd3 100644
--- a/model.cc
+++ b/model.cc
@@ -259,7 +259,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			/* The next node will try to satisfy a different set of promises. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_read_from()) {
+		} else if (nextnode->increment_read_from_past()) {
 			/* The next node will read from a different value. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
@@ -282,6 +282,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 				earliest_diverge = prevnode->get_action();
 			}
 		}
+		/* Start the round robin scheduler from this thread id */
+		scheduler->set_scheduler_thread(tid);
 		/* The correct sleep set is in the parent node. */
 		execute_sleep_set();
 
@@ -840,40 +842,36 @@ 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)
 {
 	uint64_t value = VALUE_NONE;
 	bool updated = false;
 	while (true) {
-		const ModelAction *reads_from = curr->get_node()->get_read_from();
-		if (reads_from != NULL) {
+		const ModelAction *rf = curr->get_node()->get_read_from_past();
+		if (rf != NULL) {
 			mo_graph->startChanges();
 
-			value = reads_from->get_value();
-			bool r_status = false;
+			value = rf->get_value();
 
-			if (!second_part_of_rmw) {
-				check_recency(curr, reads_from);
-				r_status = r_modification_order(curr, reads_from);
-			}
+			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() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) {
 				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) {
+		} else {
 			/* Read from future value */
 			struct future_value fv = curr->get_node()->get_future_value();
 			Promise *promise = new Promise(curr, fv);
@@ -1111,7 +1109,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
 	case THREAD_CREATE: {
 		thrd_t *thrd = (thrd_t *)curr->get_location();
 		struct thread_params *params = (struct thread_params *)curr->get_value();
-		Thread *th = new Thread(thrd, params->func, params->arg);
+		Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
 		add_thread(th);
 		th->set_creation(curr);
 		/* Promises can be satisfied by children */
@@ -1325,6 +1323,30 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 	return false;
 }
 
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+	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;
+		}
+	}
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1348,6 +1370,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 		Thread *blocking = (Thread *)curr->get_location();
 		if (!blocking->is_complete()) {
 			blocking->push_wait_list(curr);
+			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
 	}
@@ -1393,7 +1416,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
 	/* Build may_read_from set for newly-created actions */
 	if (newly_explored && curr->is_read())
-		build_reads_from_past(curr);
+		build_may_read_from(curr);
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
@@ -1410,7 +1433,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))
@@ -1478,7 +1501,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 
 	if ((parnode && !parnode->backtrack_empty()) ||
 			 !currnode->misc_empty() ||
-			 !currnode->read_from_empty() ||
+			 !currnode->read_from_past_empty() ||
 			 !currnode->future_value_empty() ||
 			 !currnode->promise_empty() ||
 			 !currnode->relseq_break_empty()) {
@@ -1586,7 +1609,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
@@ -1619,12 +1642,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)
@@ -1642,8 +1665,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;
 					}
@@ -1738,13 +1761,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;
@@ -2420,7 +2443,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			read_from(read, write);
 			//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);
@@ -2460,11 +2483,10 @@ 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->is_read() &&
 				!act->could_synchronize_with(curr) &&
-				!act->same_thread(curr) &&
-				act->get_location() == curr->get_location() &&
+				promise->is_compatible(curr) &&
 				promise->get_value() == curr->get_value()) {
 			curr->get_node()->set_promise(i, act->is_rmw());
 		}
@@ -2568,12 +2590,12 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
 
 /**
  * Build up an initial set of all past writes that this 'read' action may read
- * from. This set is determined by the clock vector's "happens before"
- * relationship.
+ * from, as well as any previously-observed future values that must still be valid.
+ *
  * @param curr is the current ModelAction that we are exploring; it must be a
  * 'read' operation.
  */
-void ModelChecker::build_reads_from_past(ModelAction *curr)
+void ModelChecker::build_may_read_from(ModelAction *curr)
 {
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
@@ -2609,7 +2631,7 @@ void ModelChecker::build_reads_from_past(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();
 			}
 
@@ -2618,8 +2640,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 				break;
 		}
 	}
+
+	/* Inherit existing, promised future values */
+	for (i = 0; i < promises->size(); i++) {
+		const Promise *promise = (*promises)[i];
+		const ModelAction *promise_read = promise->get_action();
+		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);
+			}
+			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()) {
+	if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) {
 		priv->no_valid_reads = true;
 		set_assert();
 	}
@@ -2627,9 +2666,9 @@ void ModelChecker::build_reads_from_past(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");
 	}
 }
 
@@ -2871,7 +2910,7 @@ void ModelChecker::run()
 {
 	do {
 		thrd_t user_thread;
-		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
 		add_thread(t);
 
 		do {