X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=44fba7eabc84839bc71bc64e7b69f18bb123b676;hb=bb168337e93650eddb90df61b109db4e1e8570c9;hp=446137922bbce9b56aa37c092db174a0dc3df71f;hpb=3510b440b186949cbc0760d369da6787f0def7ac;p=c11tester.git

diff --git a/model.cc b/model.cc
index 44613792..44fba7ea 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();
@@ -842,42 +838,51 @@ 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();
+		switch (node->get_read_from_status()) {
+		case READ_FROM_PAST: {
+			const ModelAction *rf = node->get_read_from_past();
+			ASSERT(rf);
 
-			value = reads_from->get_value();
-			bool r_status = false;
-
-			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();
+			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 +890,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;
@@ -1437,7 +1446,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 +1515,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 +1621,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 +1654,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 +1677,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 +1773,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;
@@ -2492,7 +2500,7 @@ void ModelChecker::compute_promises(ModelAction *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());
+			curr->get_node()->set_promise(i);
 		}
 	}
 }
@@ -2635,7 +2643,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();
 			}
 
@@ -2653,16 +2661,14 @@ void ModelChecker::build_may_read_from(ModelAction *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 +2676,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");
 	}
 }