changes

diff --git a/datarace.cc b/datarace.cc
index 5ab52fc49eefa87ea1d2ad4e3c8c1a4b607f15f5..34060faeab2bc2a70515a9f3cc01b5a5d5ebf68e 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -82,14 +82,18 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
        race->isnewwrite=isnewwrite;
        race->address=address;
        unrealizedraces.push_back(race);
-       checkDataRaces();
+
+       /* If the race is realized, bail out now. */
+       if (checkDataRaces()) {
+               model->assert_thread();
+       }
 }
 
 /** This function goes through the list of unrealized data races,
  *     removes the impossible ones, and print the realized ones. */
 
-void checkDataRaces() {
-       if (true) {
+bool checkDataRaces() {
+       if (model->isfeasibleprefix()) {
                /* Prune the non-racing unrealized dataraces */
                unsigned int i,newloc=0;
                for(i=0;i<unrealizedraces.size();i++) {
@@ -100,11 +104,17 @@ void checkDataRaces() {
                }
                if (newloc!=i)
                        unrealizedraces.resize(newloc);
-               for(i=0;i<unrealizedraces.size();i++) {
-                       struct DataRace * race=unrealizedraces[i];
-                       printRace(race);
+
+               if (unrealizedraces.size()!=0) {
+                       /* We have an actual realized race. */
+                       for(i=0;i<unrealizedraces.size();i++) {
+                               struct DataRace * race=unrealizedraces[i];
+                               printRace(race);
+                       }
+                       return true;
                }
        }
+       return false;
 }
 
 void printRace(struct DataRace * race) {

diff --git a/datarace.h b/datarace.h
index b2f709911ecff2274596ed11f7c5338365ee57e7..5bfcb8ad48cc98d007612805c2cc48567dedf984 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -40,7 +40,7 @@ struct DataRace {
 void initRaceDetector();
 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
-void checkDataRaces();
+bool checkDataRaces();
 void printRace(struct DataRace *race);
 
 extern std::vector<struct DataRace *> unrealizedraces;

diff --git a/model.cc b/model.cc
index ec953ef1f2d1a74eae62b1d04e4f288d531458ce..0e2b818cd26487df48b0968484e9533c984a8443 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -357,6 +357,12 @@ 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() {
+}
+
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
        return !mo_graph->checkForCycles() && !failed_promise;
@@ -956,6 +962,14 @@ 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.
@@ -974,6 +988,9 @@ bool ModelChecker::take_step() {
                } 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;
                } else {
                        ASSERT(false);
                }

diff --git a/model.h b/model.h
index 9eb9aa655c0285914c48be1414c17d4061171f64..9235f8f7f306a88a857361e281157148f102bf4f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -53,6 +53,7 @@ public:
        /** @return The currently executing Thread. */
        Thread * get_current_thread() { return scheduler->get_current_thread(); }
 
+       void assert_thread();
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
        ModelAction * get_parent_action(thread_id_t tid);
@@ -64,6 +65,7 @@ public:
                        std::vector<const ModelAction *> *release_heads);
 
        void finish_execution();
+       bool isfeasibleprefix();
 
        MEMALLOC
 private:

diff --git a/threads.h b/threads.h
index e7cd792a134c4b5e223b6f9465af4eaf83753b1e..6872ffa18dcedbdc547242b03b512946cde17c9a 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -27,6 +27,7 @@ typedef enum thread_state {
         * context.
         */
        THREAD_READY,
+       THREAD_ASSERTED,
        /** Thread has completed its execution */
        THREAD_COMPLETED
 } thread_state;