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

check in my stuff...

Conflicts:
	model.cc
	threads.h

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 56723c7d5660077c3b1e27d484976d5092388bd7..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);
 }
 
@@ -339,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;
        }
@@ -370,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;
@@ -700,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;
 }
 
@@ -791,6 +806,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                } else
                        promise_index++;
        }
+
        return resolved;
 }
 
@@ -973,6 +989,9 @@ 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) {

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: