From ba484ecdbd0285d264e70ec6d9c0f3fab57b626f Mon Sep 17 00:00:00 2001
From: weiyu <weiyuluo1232@gmail.com>
Date: Mon, 15 Jul 2019 18:25:06 -0700
Subject: [PATCH] allow the fuzzer to continue if only a few data races are
detected
---
datarace.cc | 4 ++--
execution.cc | 31 +++++++++++++++++++++++++++++++
execution.h | 4 ++++
model.cc | 24 +++++++++++++++++++++++-
model.h | 2 ++
5 files changed, 62 insertions(+), 3 deletions(-)
diff --git a/datarace.cc b/datarace.cc
index 22e473f5..ef9d679d 100644
--- 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 c5c40a91..e0d49808 100644
--- 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 ced21e4c..21b152b5 100644
--- 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 6214e9bc..83df6569 100644
--- 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 be9c86af..a37bd49d 100644
--- 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;
--
2.34.1