Merge branch 'master' into brian

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 93e06d0262de2b4c4d93bf8c9207f018b710cb3e..d80d1d27be741c749d9f94db4e8c5c9f8c28e6d4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -26,7 +26,7 @@ ModelChecker::ModelChecker()
        diverge(NULL),
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
-       thread_map(new std::map<int, class Thread *>),
+       thread_map(new std::map<int, Thread *>),
        obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
@@ -37,7 +37,7 @@ ModelChecker::ModelChecker()
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-       std::map<int, class Thread *>::iterator it;
+       std::map<int, Thread *>::iterator it;
        for (it = thread_map->begin(); it != thread_map->end(); it++)
                delete (*it).second;
        delete thread_map;
@@ -78,7 +78,7 @@ int ModelChecker::get_num_threads()
 }
 
 /** @returns a sequence number for a new ModelAction */
-int ModelChecker::get_next_seq_num()
+modelclock_t ModelChecker::get_next_seq_num()
 {
        return ++used_sequence_numbers;
 }
@@ -124,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
        next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
-               Node *node = next->get_node();
+               Node *node = next->get_node()->get_parent();
 
                /* Reached divergence point */
                DEBUG("*** Divergence point ***\n");
@@ -196,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (prev == NULL)
                return;
 
-       node = prev->get_node();
+       node = prev->get_node()->get_parent();
 
        while (!node->is_enabled(t))
                t = t->get_parent();
@@ -205,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (node->has_been_explored(t->get_id()))
                return;
 
+       /* Cache the latest backtracking point */
        if (!next_backtrack || *prev > *next_backtrack)
                next_backtrack = prev;
 
@@ -262,7 +263,7 @@ void ModelChecker::check_current_action(void)
 
        nextThread = get_next_replay_thread();
 
-       currnode = curr->get_node();
+       currnode = curr->get_node()->get_parent();
 
        if (!currnode->backtrack_empty())
                if (!next_backtrack || *curr > *next_backtrack)
@@ -271,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);
 }
 
 /**
@@ -282,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)
@@ -308,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"
@@ -322,6 +343,9 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ASSERT(curr->is_read());
 
+       /* Track whether this object has been initialized */
+       bool initialized = false;
+
        for (i = 0; i < thrd_lists->size(); i++) {
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
@@ -339,11 +363,28 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        }
                        curr->get_node()->add_read_from(act);
 
-                       /* Include at most one act that "happens before" curr */
-                       if (act->happens_before(curr))
+                       /* Include at most one act per-thread that "happens before" curr */
+                       if (act->happens_before(curr)) {
+                               initialized = true;
                                break;
+                       }
                }
        }
+
+       if (!initialized) {
+               /* TODO: need a more informative way of reporting errors */
+               printf("ERROR: may read from uninitialized atomic\n");
+       }
+
+       if (DBG_ENABLED() || !initialized) {
+               printf("Reached read action:\n");
+               curr->print();
+               printf("Printing may_read_from\n");
+               curr->get_node()->print_may_read_from();
+               printf("End printing may_read_from\n");
+       }
+
+       ASSERT(initialized);
 }
 
 static void print_list(action_list_t *list)