From bc487ada50f22a523e2bf92ff62bacba7db98701 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 6 Jul 2012 18:37:11 -0700 Subject: [PATCH] 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. --- model.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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); } /** -- 2.34.1