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

diff --combined model.cc
index 0006fd63d66e172336df1296c417a787fe559d2a,744fec5e17a27ef75b07a2bca068ff344e951ee8..4f600a91f5eab4bb65420974e78651f0e53cfcfb
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -139,9 -139,6 +139,9 @@@ Thread * ModelChecker::get_next_thread(
        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()) {
@@@ -161,12 -158,8 +161,12 @@@
                        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();
@@@ -191,7 -184,7 +191,7 @@@ bool ModelChecker::next_execution(
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
-                       earliest_diverge->print();
+                       earliest_diverge->print(false);
                else
                        printf("(Not set)\n");
  
@@@ -205,6 -198,9 +205,6 @@@
        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();
@@@ -430,7 -426,7 +430,7 @@@ bool ModelChecker::process_mutex(ModelA
                action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
                //activate all the waiting threads
                for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-                       scheduler->add_thread(get_thread((*rit)->get_tid()));
+                       scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
                break;
@@@ -488,26 -484,17 +488,17 @@@ bool ModelChecker::process_thread_actio
                break;
        }
        case THREAD_JOIN: {
-               Thread *waiting, *blocking;
-               waiting = get_thread(curr);
-               blocking = (Thread *)curr->get_location();
-               if (!blocking->is_complete()) {
-                       blocking->push_wait_list(curr);
-                       scheduler->sleep(waiting);
-               } else {
-                       do_complete_join(curr);
-                       synchronized = true;
-               }
+               Thread *blocking = (Thread *)curr->get_location();
+               ModelAction *act = get_last_action(blocking->get_id());
+               curr->synchronize_with(act);
+               synchronized = true;
                break;
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                while (!th->wait_list_empty()) {
                        ModelAction *act = th->pop_wait_list();
-                       Thread *wake = get_thread(act);
-                       scheduler->wake(wake);
-                       do_complete_join(act);
-                       synchronized = true;
+                       scheduler->wake(get_thread(act));
                }
                th->complete();
                break;
@@@ -547,6 -534,8 +538,8 @@@ ModelAction * ModelChecker::initialize_
                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 */
@@@ -577,9 -566,12 +570,12 @@@
  }
  
  /**
-  * This method checks whether a model action is enabled at the given point.
-  * At this point, it checks whether a lock operation would be successful at this point.
-  * If not, it puts the thread in a waiter list.
+  * @brief Check whether a model action is enabled.
+  *
+  * Checks whether a lock or join operation would be successful (i.e., is the
+  * lock already locked, or is the joined thread already complete). If not, put
+  * the action in a waiter list.
+  *
   * @param curr is the ModelAction to check whether it is enabled.
   * @return a bool that indicates whether the action is enabled.
   */
@@@ -592,6 -584,12 +588,12 @@@ bool ModelChecker::check_action_enabled
                        lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
                        return false;
                }
+       } else if (curr->get_type() == THREAD_JOIN) {
+               Thread *blocking = (Thread *)curr->get_location();
+               if (!blocking->is_complete()) {
+                       blocking->push_wait_list(curr);
+                       return false;
+               }
        }
  
        return true;
@@@ -617,9 -615,9 +619,9 @@@ Thread * ModelChecker::check_current_ac
  
        if (!check_action_enabled(curr)) {
                /* Make the execution look like we chose to run this action
-                * much later, when a lock is actually available to release */
+                * much later, when a lock/join can succeed */
                get_current_thread()->set_pending(curr);
-               remove_thread(get_current_thread());
+               scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
        }
  
@@@ -701,19 -699,6 +703,6 @@@
        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();