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 884ed64d0b30b51ec73954e3797f10a2e70fe793..436ef77cf067983abf5f45d90f8c58517030c76f 100644 (file)
--- 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);
 }
 
 /**