From: Brian Norris <banorris@uci.edu>
Date: Thu, 24 Jan 2013 01:33:23 +0000 (-0800)
Subject: future_value: add thread ID parameter
X-Git-Tag: oopsla2013~328
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=9f1ddeb2b2ba0bf52d14456c90b363daa2f09965

future_value: add thread ID parameter

This just records the parameter for now, and makes it a distinction
between future values. Shouldn't affect model-checker behavior, except
for the introduction of extra future values: one for each thread which
writes the same value.

We calculate whether the writing thread exists at the time of the future
value and if not, find an ancestor thread which does.
---

diff --git a/model.cc b/model.cc
index 40b25d0..d1496e8 100644
--- a/model.cc
+++ b/model.cc
@@ -856,11 +856,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);
 	}
 }
diff --git a/nodestack.cc b/nodestack.cc
index 7d703bb..dd2dd85 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -230,9 +230,10 @@ bool Node::add_future_value(struct future_value& fv)
 {
 	uint64_t value = fv.value;
 	modelclock_t expiration = fv.expiration;
+	thread_id_t tid = fv.tid;
 	int idx = -1; /* Highest index where value is found */
 	for (unsigned int i = 0; i < future_values.size(); i++) {
-		if (future_values[i].value == value) {
+		if (future_values[i].value == value && future_values[i].tid == tid) {
 			if (expiration <= future_values[i].expiration)
 				return false;
 			idx = i;
diff --git a/promise.h b/promise.h
index 7e6e396..3c0d5dd 100644
--- a/promise.h
+++ b/promise.h
@@ -16,6 +16,7 @@
 struct future_value {
 	uint64_t value;
 	modelclock_t expiration;
+	thread_id_t tid;
 };
 
 class Promise {