allow the fuzzer to continue if only a few data races are detected

diff --git a/datarace.cc b/datarace.cc
index 22e473f50b981d41fc2cdcb3bf529b5ca30f4eef..ef9d679d56b3df6f937ec1243e92f95a344c2af6 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -158,7 +158,7 @@ bool checkDataRaces()
  */
 void assert_race(struct DataRace *race)
 {
-       model->assert_bug(
+       model->assert_race(
                "Data race detected @ address %p:\n"
                "    Access 1: %5s in thread %2d @ clock %3u\n"
                "    Access 2: %5s in thread %2d @ clock %3u",
@@ -169,7 +169,7 @@ void assert_race(struct DataRace *race)
                race->isnewwrite ? "write" : "read",
                id_to_int(race->newaction->get_tid()),
                race->newaction->get_seq_number()
-               );
+       );
 }
 
 /** This function does race detection for a write on an expanded record. */

diff --git a/execution.cc b/execution.cc
index c5c40a91f7776d43e98dd3cc027e8b9b05db56b0..e0d49808f2bd14844a5cd9d72f916b1af55c13c7 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -27,6 +27,7 @@ struct model_snapshot_members {
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
                bugs(),
+               dataraces(),
                bad_synchronization(false),
                asserted(false)
        { }
@@ -34,12 +35,16 @@ struct model_snapshot_members {
        ~model_snapshot_members() {
                for (unsigned int i = 0;i < bugs.size();i++)
                        delete bugs[i];
+               for (unsigned int i = 0;i < dataraces.size(); i++) 
+                       delete dataraces[i];
                bugs.clear();
+               dataraces.clear();
        }
 
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        SnapVector<bug_message *> bugs;
+       SnapVector<bug_message *> dataraces;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool asserted;
@@ -185,12 +190,38 @@ bool ModelExecution::assert_bug(const char *msg)
        return false;
 }
 
+/* @brief Put data races in a different list from other bugs. The purpose
+ *  is to continue the program untill the number of data races exceeds a 
+ *  threshold */
+
+/* TODO: check whether set_assert should be called */
+bool ModelExecution::assert_race(const char *msg)
+{
+       priv->dataraces.push_back(new bug_message(msg));
+
+       if (isfeasibleprefix()) {
+               set_assert();
+               return true;
+       }
+       return false;
+}
+
 /** @return True, if any bugs have been reported for this execution */
 bool ModelExecution::have_bug_reports() const
 {
        return priv->bugs.size() != 0;
 }
 
+/** @return True, if any fatal bugs have been reported for this execution.
+ *  Any bug other than a data race is considered a fatal bug. Data races 
+ *  are not considered fatal unless the number of races is exceeds
+ *  a threshold (temporarily set as 15). 
+ */
+bool ModelExecution::have_fatal_bug_reports() const
+{
+       return priv->bugs.size() != 0 || priv->dataraces.size() >= 15;
+}
+
 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 {
        return &priv->bugs;

diff --git a/execution.h b/execution.h
index ced21e4c90f17777c953193a6d412c1b4390242b..21b152b582c2f3ac32164975ecf267b8ebf9489e 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -68,7 +68,11 @@ public:
        bool check_action_enabled(ModelAction *curr);
 
        bool assert_bug(const char *msg);
+       bool assert_race(const char *msg);
+
        bool have_bug_reports() const;
+       bool have_fatal_bug_reports() const;
+
        SnapVector<bug_message *> * get_bugs() const;
 
        bool has_asserted() const;

diff --git a/model.cc b/model.cc
index 6214e9bcfcea73f4668351197820473e0ae0d923..83df6569c2a4781eebf3a8a53b4ba6e3622334a5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -139,6 +139,28 @@ bool ModelChecker::assert_bug(const char *msg, ...)
        return execution->assert_bug(str);
 }
 
+/**
+ * @brief Assert a data race in the executing program.
+ *
+ * Different from assert_bug, the program will not be aborted immediately
+ * upon calling this function, unless the number of data races exceeds
+ * a threshold.
+ *
+ * @param msg Descriptive message for the bug (do not include newline char)
+ * @return True if bug is immediately-feasible
+ */
+bool ModelChecker::assert_race(const char *msg, ...)
+{
+       char str[800];
+
+       va_list ap;
+       va_start(ap, msg);
+       vsnprintf(str, sizeof(str), msg, ap);
+       va_end(ap);
+
+       return execution->assert_race(str);
+}
+
 /**
  * @brief Assert a bug in the executing program, asserted by a user thread
  * @see ModelChecker::assert_bug
@@ -358,7 +380,7 @@ bool ModelChecker::should_terminate_execution()
        /* Infeasible -> don't take any more steps */
        if (execution->is_infeasible())
                return true;
-       else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
+       else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
                execution->set_assert();
                return true;
        }

diff --git a/model.h b/model.h
index be9c86afca6d973b0bec4280654fb6c819268489..a37bd49d5e0deb818cdfa833336140554fa984a8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -59,6 +59,8 @@ public:
        uint64_t switch_to_master(ModelAction *act);
 
        bool assert_bug(const char *msg, ...);
+       bool assert_race(const char *msg, ...);
+
        void assert_user_bug(const char *msg);
 
        model_params params;