Merge branch 'master' into brian

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 884ed64d0b30b51ec73954e3797f10a2e70fe793..d80d1d27be741c749d9f94db4e8c5c9f8c28e6d4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -272,6 +272,19 @@ 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();
+               /* Assign reads_from, perform release/acquire synchronization */
+               curr->read_from(reads_from);
+       }
+       th->set_return_value(value);
 }
 
 /**
@@ -283,14 +296,17 @@ void ModelChecker::check_current_action(void)
  */
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
+       int tid = id_to_int(act->get_tid());
        action_trace->push_back(act);
 
        std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
-       if (id_to_int(act->get_tid()) >= (int)vec->size())
+       if (tid >= (int)vec->size())
                vec->resize(next_thread_id);
-       (*vec)[id_to_int(act->get_tid())].push_back(act);
+       (*vec)[tid].push_back(act);
 
-       (*thrd_last_action)[id_to_int(act->get_tid())] = act;
+       if ((int)thrd_last_action->size() <= tid)
+               thrd_last_action->resize(get_num_threads());
+       (*thrd_last_action)[tid] = act;
 }
 
 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
@@ -309,6 +325,10 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
        return parent;
 }
 
+ClockVector * ModelChecker::get_cv(thread_id_t tid) {
+       return get_parent_action(tid)->get_cv();
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"