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