From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 00:19:10 +0000 (-0800)
Subject: model: fixes for future value passing
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=237f94a977b3c09f8b3b2f551e0057a4ed36b06d;p=c11tester.git

model: fixes for future value passing

For one, we don't want to 'add_future_value()' when w_modification_order
is called anywhere besides process_write(). Also, we want to filter out
potential future values based on the existence of a Promise that this
write must resolve. So pass a vector parameter to w_modification_order
for recording future values only when (and where) we want them.
---

diff --git a/model.cc b/model.cc
index 618b37e0..129f6c02 100644
--- a/model.cc
+++ b/model.cc
@@ -1044,12 +1044,26 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
  */
 bool ModelChecker::process_write(ModelAction *curr)
 {
-	bool updated_mod_order = w_modification_order(curr);
+	/* Readers to which we may send our future value */
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+
+	bool updated_mod_order = w_modification_order(curr, &send_fv);
 	int promise_idx = get_promise_to_resolve(curr);
+	const ModelAction *earliest_promise_reader;
 	bool updated_promises = false;
 
-	if (promise_idx >= 0)
+	if (promise_idx >= 0) {
+		earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
 		updated_promises = resolve_promise(curr, promise_idx);
+	} else
+		earliest_promise_reader = NULL;
+
+	/* Don't send future values to reads after the Promise we resolve */
+	for (unsigned int i = 0; i < send_fv.size(); i++) {
+		ModelAction *read = send_fv[i];
+		if (!earliest_promise_reader || *read < *earliest_promise_reader)
+			futurevalues->push_back(PendingFutureValue(curr, read));
+	}
 
 	if (promises->size() == 0) {
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
@@ -1506,7 +1520,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 				}
 			}
 			if (act->is_write()) {
-				if (w_modification_order(act))
+				if (w_modification_order(act, NULL))
 					updated = true;
 			}
 			mo_graph->commitChanges();
@@ -1837,9 +1851,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
  * (II) Sending the write back to non-synchronizing reads.
  *
  * @param curr The current action. Must be a write.
+ * @param send_fv A vector for stashing reads to which we may pass our future
+ * value. If NULL, then don't record any future values.
  * @return True if modification order edges were added; false otherwise
  */
-bool ModelChecker::w_modification_order(ModelAction *curr)
+bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
 {
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
@@ -1932,9 +1948,9 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				   pendingfuturevalue.
 
 				 */
-				if (thin_air_constraint_may_allow(curr, act)) {
+				if (send_fv && thin_air_constraint_may_allow(curr, act)) {
 					if (!is_infeasible())
-						futurevalues->push_back(PendingFutureValue(curr, act));
+						send_fv->push_back(act);
 					else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
 						add_future_value(curr, act);
 				}
diff --git a/model.h b/model.h
index fe76d7f9..412543db 100644
--- a/model.h
+++ b/model.h
@@ -196,7 +196,7 @@ private:
 	template <typename rf_type>
 	bool r_modification_order(ModelAction *curr, const rf_type *rf);
 
-	bool w_modification_order(ModelAction *curr);
+	bool w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv);
 	void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
 	bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
 	bool resolve_release_sequences(void *location, work_queue_t *work_queue);