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 d171ad0b83a7a97b86caa6e9aed48ea1c1411378..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);
 }
 
@@ -311,6 +314,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        Thread *wake = th->pop_wait_list();
                        scheduler->wake(wake);
                }
+               th->complete();
        }
 
        /* Deal with new thread */
@@ -338,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;
        }
@@ -369,6 +373,13 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                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;
@@ -699,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;
 }
 
@@ -790,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
        return resolved;
 }
 
@@ -953,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)
@@ -975,18 +989,17 @@ int ModelChecker::switch_to_master(ModelAction *act)
 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;
-                       }
-                       if (!curr->is_blocked())
+                       ASSERT(current_action);
+                       nextThread = check_current_action(current_action);
+                       current_action = NULL;
+                       if (!curr->is_blocked() && !curr->is_complete())
                                scheduler->add_thread(curr);
-               } else if (curr->get_state() == THREAD_RUNNING) {
-                       /* Stopped while running; i.e., completed */
-                       curr->complete();
                } else {
                        ASSERT(false);
                }