Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index ce9e0660ff33021bc53bfaa0ada87cd60b12434f..4f600a91f5eab4bb65420974e78651f0e53cfcfb 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -139,6 +139,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        ModelAction *next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
+               if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+                       earliest_diverge=diverge;
+
                Node *nextnode = next->get_node();
                /* Reached divergence point */
                if (nextnode->increment_promise()) {
@@ -158,8 +161,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        Node *node = nextnode->get_parent();
                        tid = node->get_next_backtrack();
                        node_stack->pop_restofstack(1);
+                       if (diverge==earliest_diverge) {
+                               earliest_diverge=node->get_action();
+                       }
                }
                DEBUG("*** Divergence point ***\n");
+
                diverge = NULL;
        } else {
                tid = next->get_tid();
@@ -198,9 +205,6 @@ bool ModelChecker::next_execution()
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
-       if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-               earliest_diverge=diverge;
-
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();
@@ -534,6 +538,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                return newcurr;
        }
 
+       curr->set_seq_number(get_next_seq_num());
+
        newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
        if (newcurr) {
                /* First restore type and order in case of RMW operation */
@@ -697,19 +703,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
-/**
- * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
- * operation from the Thread it is joining with. Must be called after the
- * completion of the Thread in question.
- * @param join The THREAD_JOIN action
- */
-void ModelChecker::do_complete_join(ModelAction *join)
-{
-       Thread *blocking = (Thread *)join->get_location();
-       ModelAction *act = get_last_action(blocking->get_id());
-       join->synchronize_with(act);
-}
-
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();