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

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 0e2b818cd26487df48b0968484e9533c984a8443..217d6421ac403e60108ec074c900168bbce67888 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -9,6 +9,7 @@
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
+#include "datarace.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -36,7 +37,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        node_stack(new NodeStack()),
        next_backtrack(NULL),
        mo_graph(new CycleGraph()),
-       failed_promise(false)
+       failed_promise(false),
+       asserted(false)
 {
 }
 
@@ -77,6 +79,7 @@ void ModelChecker::reset_to_initial_state()
        nextThread = NULL;
        next_backtrack = NULL;
        failed_promise = false;
+       reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -299,6 +302,19 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        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 +342,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                }
        } else if (curr->is_write()) {
                if (w_modification_order(curr))
-                       updated = true;;
+                       updated = true;
                if (resolve_promises(curr))
                        updated = true;
        }
@@ -361,6 +377,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
  * feasible trace. */
 
 bool ModelChecker::isfeasibleprefix() {
+       return promises->size()==0;
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -693,6 +710,11 @@ bool ModelChecker::resolve_release_sequences(void *location)
                        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 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
        return resolved;
 }
 
@@ -947,10 +970,7 @@ void ModelChecker::remove_thread(Thread *t)
  * 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 +982,6 @@ int ModelChecker::switch_to_master(ModelAction *act)
        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 +989,17 @@ void ModelChecker::assert_thread() {
 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);
                }