X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c707ff8771b023d0f4b71b259e42dce77b7105e6;hb=75fd45bf45d7ec1ac8db7cb6209106ea4e3fc5ab;hp=40b25d0d635a32a5fdd2832001c638c3ee1986fc;hpb=ffb2033ac6b31407810703b65ae0fbaeb9c0da59;p=model-checker.git

diff --git a/model.cc b/model.cc
index 40b25d0..c707ff8 100644
--- a/model.cc
+++ b/model.cc
@@ -737,6 +737,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			/* Read from future value */
 			struct future_value fv = curr->get_node()->get_future_value();
 			value = fv.value;
+			curr->set_value(fv.value);
 			curr->set_read_from(NULL);
 			promises->push_back(new Promise(curr, fv));
 		}
@@ -856,11 +857,19 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
 {
 	/* Do more ambitious checks now that mo is more complete */
 	if (mo_may_allow(writer, reader)) {
+		Node *node = reader->get_node();
+
+		/* Find an ancestor thread which exists at the time of the reader */
+		Thread *write_thread = get_thread(writer);
+		while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+			write_thread = write_thread->get_parent();
+
 		struct future_value fv = {
 			writer->get_value(),
 			writer->get_seq_number() + params.maxfuturedelay,
+			write_thread->get_id(),
 		};
-		if (reader->get_node()->add_future_value(fv))
+		if (node->add_future_value(fv))
 			set_latest_backtrack(reader);
 	}
 }