From: Brian Norris <banorris@uci.edu>
Date: Sat, 7 Jul 2012 01:37:11 +0000 (-0700)
Subject: model: set reads_from "return value" in model-checker
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bc487ada50f22a523e2bf92ff62bacba7db98701;p=cdsspec-compiler.git

model: set reads_from "return value" in model-checker

Previously, values (let alone the reads-from relationship) were not actually
returned from the model-checker to the user. This step sets up the return value
so that the user context can retrieve it rather than using a value stuck in the
snapshotting memory.

There are still several TODOs along with the reads-from relationship, but this
code is stable enough for providing a basis for further work.
---

diff --git a/model.cc b/model.cc
index 884ed64..436ef77 100644
--- a/model.cc
+++ b/model.cc
@@ -272,6 +272,18 @@ void ModelChecker::check_current_action(void)
 	set_backtracking(curr);
 
 	add_action_to_lists(curr);
+
+	/* Assign reads_from values */
+	/* TODO: perform release/acquire synchronization here; include
+	 * reads_from as ModelAction member? */
+	Thread *th = get_thread(curr->get_tid());
+	int value = VALUE_NONE;
+	if (curr->is_read()) {
+		const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+		value = reads_from->get_value();
+		curr->set_value(value);
+	}
+	th->set_return_value(value);
 }
 
 /**