From: Brian Norris <banorris@uci.edu>
Date: Thu, 24 Jan 2013 02:05:28 +0000 (-0800)
Subject: action: record future value
X-Git-Tag: oopsla2013~327
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=75fd45bf45d7ec1ac8db7cb6209106ea4e3fc5ab;p=model-checker.git

action: record future value

Future values don't currently show up in ModelAction (e.g., when
printing). We should set the value when we choose to read from a future
value.
---

diff --git a/action.h b/action.h
index f742ddc..d0f02a3 100644
--- a/action.h
+++ b/action.h
@@ -79,6 +79,7 @@ public:
 	void * get_location() const { return location; }
 	modelclock_t get_seq_number() const { return seq_number; }
 	uint64_t get_value() const { return value; }
+	void set_value(uint64_t v) { value = v; }
 	const ModelAction * get_reads_from() const { return reads_from; }
 
 	Node * get_node() const;
diff --git a/model.cc b/model.cc
index d1496e8..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));
 		}