From: weiyu <weiyuluo1232@gmail.com>
Date: Fri, 1 Nov 2019 20:58:16 +0000 (-0700)
Subject: Do not allow a thread to stash the next pending action if its last action was a SLEEP... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=a72579537233ec7d21ac24d895b9cbe7cfe16f2d;hp=cb94be05c3b0f333821bf9fdd840dea82cba4ed8

Do not allow a thread to stash the next pending action if its last action was a SLEEP action. Fix the problem that when all the unfinished threads are sleeping (e.g. nanosleep), this execution is reported as redundant
---

diff --git a/execution.cc b/execution.cc
index e6203cb5..e7ca575d 100644
--- a/execution.cc
+++ b/execution.cc
@@ -161,6 +161,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
 		if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 			return true;
 	}
+	/* The sleep is literally sleeping */
 	if (asleep->is_sleep()) {
 		if (fuzzer->shouldWake(asleep))
 			return true;
@@ -178,7 +179,7 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 				/* Remove this thread from sleep set */
 				scheduler->remove_sleep(thr);
 				if (thr->get_pending()->is_sleep())
-					thr->set_pending(NULL);
+					thr->set_wakeup_state(true);
 			}
 		}
 	}
@@ -827,7 +828,8 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @return True if modification order edges were added; false otherwise
  */
 
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
+	SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
 {
 	SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 	unsigned int i;
diff --git a/model.cc b/model.cc
index 4c4b47ac..1e3dd2de 100644
--- a/model.cc
+++ b/model.cc
@@ -413,7 +413,7 @@ void ModelChecker::run()
 			for (unsigned int i = 0;i < get_num_threads();i++) {
 				thread_id_t tid = int_to_id(i);
 				Thread *thr = get_thread(tid);
-				if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_pending())) {
+				if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
 					switch_from_master(thr);
 					if (thr->is_waiting_on(thr))
 						assert_bug("Deadlock detected (thread %u)", i);
@@ -459,6 +459,11 @@ void ModelChecker::run()
 				t = get_next_thread();
 			if (!t || t->is_model_thread())
 				break;
+			if (t->just_woken_up()) {
+				t->set_wakeup_state(false);
+				t->set_pending(NULL);
+				continue;	// Allow this thread to stash the next pending action
+			}
 
 			/* Consume the next action for a Thread */
 			ModelAction *curr = t->get_pending();
diff --git a/schedule.cc b/schedule.cc
index 4a9752a7..f68786a8 100644
--- a/schedule.cc
+++ b/schedule.cc
@@ -108,7 +108,7 @@ bool Scheduler::is_sleep_set(const Thread *t) const
 /**
  * @brief Check if execution is stuck with no enabled threads and some sleeping
  * thread
- * @return True if no threads are enabled an some thread is in the sleep set;
+ * @return True if no threads are enabled and some thread is in the sleep set;
  * false otherwise
  */
 bool Scheduler::all_threads_sleeping() const
@@ -202,16 +202,31 @@ void Scheduler::wake(Thread *t)
 Thread * Scheduler::select_next_thread()
 {
 	int avail_threads = 0;
-	int thread_list[enabled_len];
-	for (int i = 0;i< enabled_len;i++) {
+	int sleep_threads = 0;
+	int thread_list[enabled_len], sleep_list[enabled_len];
+	Thread * thread;
+
+	for (int i = 0; i < enabled_len; i++) {
 		if (enabled[i] == THREAD_ENABLED)
 			thread_list[avail_threads++] = i;
+		else if (enabled[i] == THREAD_SLEEP_SET)
+			sleep_list[sleep_threads++] = i;
 	}
 
-	if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads())
-		return NULL;	// No threads available
+	if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads()) {
+		if (sleep_threads != 0) {
+			// No threads available, but some threads sleeping. Wake up one of them
+			thread = execution->getFuzzer()->selectThread(sleep_list, sleep_threads);
+			remove_sleep(thread);
+			thread->set_wakeup_state(true);
+		} else {
+			return NULL;	// No threads available and no threads sleeping.
+		}
+	} else {
+		// Some threads are available
+		thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
+	}
 
-	Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
 	curr_thread_index = id_to_int(thread->get_id());
 	return thread;
 }
diff --git a/threads-model.h b/threads-model.h
index e2084abf..f2162a89 100644
--- a/threads-model.h
+++ b/threads-model.h
@@ -93,6 +93,9 @@ public:
 	 *  @see Thread::pending */
 	void set_pending(ModelAction *act) { pending = act; }
 
+	bool just_woken_up() { return wakeup_state; }
+	void set_wakeup_state(bool state) { wakeup_state = state; }
+
 	Thread * waiting_on() const;
 	bool is_waiting_on(const Thread *t) const;
 
@@ -144,6 +147,9 @@ private:
 	 */
 	ModelAction *pending;
 
+	/** @brief True if this thread was just woken up */
+	bool wakeup_state;
+
 	void (*start_routine)(void *);
 	void *(*pstart_routine)(void *);