datarace: make globals static

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index f0c844cdcb019057cf6c110ad64a9d1d74cf4a4a..c0f81ea077c25caf442a6c8117a29158f9adcc7a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -199,11 +199,6 @@ modelclock_t ModelChecker::get_next_seq_num()
        return ++priv->used_sequence_numbers;
 }
 
-Node * ModelChecker::get_curr_node() const
-{
-       return node_stack->get_head();
-}
-
 /**
  * @brief Select the next thread to execute based on the curren action
  *
@@ -246,7 +241,7 @@ Thread * ModelChecker::get_next_thread()
         * scheduler decide
         */
        if (diverge == NULL)
-               return scheduler->select_next_thread();
+               return scheduler->select_next_thread(node_stack->get_head());
 
        /* Else, we are trying to replay an execution */
        ModelAction *next = node_stack->get_next()->get_action();
@@ -1446,11 +1441,12 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
  */
 bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
 {
-       if (!second->synchronize_with(first)) {
+       if (*second < *first) {
                set_bad_synchronization();
                return false;
        }
-       return true;
+       check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+       return second->synchronize_with(first);
 }
 
 /**