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

check in my stuff...

Conflicts:
	model.cc
	threads.h

diff --combined model.cc
index 0e2b818cd26487df48b0968484e9533c984a8443,56723c7d5660077c3b1e27d484976d5092388bd7..217d6421ac403e60108ec074c900168bbce67888
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -9,6 -9,6 +9,7 @@@
  #include "clockvector.h"
  #include "cyclegraph.h"
  #include "promise.h"
++#include "datarace.h"
  
  #define INITIAL_THREAD_ID     0
  
@@@ -36,7 -36,7 +37,8 @@@ ModelChecker::ModelChecker(struct model
        node_stack(new NodeStack()),
        next_backtrack(NULL),
        mo_graph(new CycleGraph()),
--      failed_promise(false)
++      failed_promise(false),
++      asserted(false)
  {
  }
  
@@@ -77,6 -77,6 +79,7 @@@ void ModelChecker::reset_to_initial_sta
        nextThread = NULL;
        next_backtrack = NULL;
        failed_promise = false;
++      reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
  }
  
@@@ -299,6 -299,19 +302,19 @@@ Thread * ModelChecker::check_current_ac
        if (curr->get_type() == THREAD_CREATE) {
                Thread *th = (Thread *)curr->get_location();
                th->set_creation(curr);
+       } else if (curr->get_type() == THREAD_JOIN) {
+               Thread *wait, *join;
+               wait = get_thread(curr->get_tid());
+               join = (Thread *)curr->get_location();
+               if (!join->is_complete())
+                       scheduler->wait(wait, join);
+       } else if (curr->get_type() == THREAD_FINISH) {
+               Thread *th = get_thread(curr->get_tid());
+               while (!th->wait_list_empty()) {
+                       Thread *wake = th->pop_wait_list();
+                       scheduler->wake(wake);
+               }
+               th->complete();
        }
  
        /* Deal with new thread */
@@@ -326,7 -339,7 +342,7 @@@
                }
        } else if (curr->is_write()) {
                if (w_modification_order(curr))
--                      updated = true;;
++                      updated = true;
                if (resolve_promises(curr))
                        updated = true;
        }
@@@ -357,12 -370,6 +373,13 @@@
                return get_next_replay_thread();
  }
  
 +/** @returns whether the current partial trace must be a prefix of a
 + * feasible trace. */
 +
 +bool ModelChecker::isfeasibleprefix() {
++      return promises->size()==0;
 +}
 +
  /** @returns whether the current partial trace is feasible. */
  bool ModelChecker::isfeasible() {
        return !mo_graph->checkForCycles() && !failed_promise;
@@@ -693,6 -700,6 +710,11 @@@ bool ModelChecker::resolve_release_sequ
                        it++;
        }
  
++      // If we resolved promises or data races, see if we have realized a data race.
++      if (checkDataRaces()) {
++              model->set_assert();
++      }
++
        return updated;
  }
  
@@@ -784,6 -791,6 +806,7 @@@ bool ModelChecker::resolve_promises(Mod
                } else
                        promise_index++;
        }
++
        return resolved;
  }
  
@@@ -947,10 -954,7 +970,7 @@@ void ModelChecker::remove_thread(Threa
   * context). This switch is made with the intention of exploring a particular
   * model-checking action (described by a ModelAction object). Must be called
   * from a user-thread context.
-  * @param act The current action that will be explored. May be NULL, although
-  * there is little reason to switch to the model-checker without an action to
-  * explore (note: act == NULL is sometimes used as a hack to allow a thread to
-  * yield control without performing any progress; see thrd_join()).
+  * @param act The current action that will be explored. Must not be NULL.
   * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
   */
  int ModelChecker::switch_to_master(ModelAction *act)
@@@ -962,14 -966,6 +982,6 @@@
        return Thread::swap(old, &system_context);
  }
  
- void ModelChecker::assert_thread() {
-       DBG();
-       Thread *old = thread_current();
-       set_current_action(NULL);
-       old->set_state(THREAD_ASSERTED);
-       return Thread::swap(old, &system_context);
- }
- 
  /**
   * Takes the next step in the execution, if possible.
   * @return Returns true (success) if a step was taken and false otherwise.
@@@ -977,20 -973,14 +989,17 @@@
  bool ModelChecker::take_step() {
        Thread *curr, *next;
  
++      if (has_asserted())
++              return false;
++
        curr = thread_current();
        if (curr) {
                if (curr->get_state() == THREAD_READY) {
-                       if (current_action) {
-                               nextThread = check_current_action(current_action);
-                               current_action = NULL;
-                       }
-                       scheduler->add_thread(curr);
-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();
-               } else if (curr->get_state()==THREAD_ASSERTED) {
-                       /* Something bad happened.  Stop taking steps. */
-                       return false;
+                       ASSERT(current_action);
+                       nextThread = check_current_action(current_action);
+                       current_action = NULL;
+                       if (!curr->is_blocked() && !curr->is_complete())
+                               scheduler->add_thread(curr);
                } else {
                        ASSERT(false);
                }