From: Brian Norris <banorris@uci.edu>
Date: Thu, 4 Apr 2013 08:00:17 +0000 (-0700)
Subject: model: proactively build/prune is_enabled() set
X-Git-Tag: oopsla2013~99
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=1ad7373e04c1b94a927f4b8735bffe2c62af55f3;hp=2b493dff916099b11e559243b117ffd5eabe8f3b

model: proactively build/prune is_enabled() set

We should proactively check whether threads are enabled, as this allows
the model-checker to more accurately reason about backtracking, fairness
(particularly, assigning thread priorities), and sleep sets.

This commit causes changes in observed executions for many test
programs. Often, this occurs for programs where the main thread
performs a JOIN on a child thread. Previously, we would only discover
that this thread should be disabled once the scheduler attempts to
execute the JOIN ModelAction. For the period of the trace in which this
disabling isn't discovered, we may try to set backtracking points for
the main thread. These executions just turn into infeasible or
sleep-set-redundant executions anyway.

This can also affect the assertion of thread priority when assigning
backtracking points. If a thread is supposedly "enabled" (but in fact is
not), then we may prevent other threads from running because this thread has
priority. But that thread cannot run, so instead we were doing some
funky things with the remaining ("low-priority") threads.

This fix remedies these sorts of issues by precisely computing the set
of threads which are disabled, waiting on other threads/locks.
---

diff --git a/model.cc b/model.cc
index 37417d6..feda416 100644
--- a/model.cc
+++ b/model.cc
@@ -3068,23 +3068,14 @@ Thread * ModelChecker::take_step(ModelAction *curr)
 	Thread *curr_thrd = get_thread(curr);
 	ASSERT(curr_thrd->get_state() == THREAD_READY);
 
-	if (!check_action_enabled(curr)) {
-		/* Make the execution look like we chose to run this action
-		 * much later, when a lock/join can succeed */
-		get_thread(curr)->set_pending(curr);
-		scheduler->sleep(curr_thrd);
-		curr = NULL;
-	} else {
-		curr = check_current_action(curr);
-		ASSERT(curr);
-	}
+	ASSERT(check_action_enabled(curr)); /* May have side effects? */
+	curr = check_current_action(curr);
+	ASSERT(curr);
 
 	if (curr_thrd->is_blocked() || curr_thrd->is_complete())
 		scheduler->remove_thread(curr_thrd);
 
-	if (curr)
-		return action_select_next_thread(curr);
-	return NULL;
+	return action_select_next_thread(curr);
 }
 
 /** Wrapper to run the user's main function, with appropriate arguments */
@@ -3133,6 +3124,15 @@ void ModelChecker::run()
 				}
 			}
 
+			/* Don't schedule threads which should be disabled */
+			for (unsigned int i = 0; i < get_num_threads(); i++) {
+				Thread *th = get_thread(int_to_id(i));
+				ModelAction *act = th->get_pending();
+				if (act && is_enabled(th) && !check_action_enabled(act)) {
+					scheduler->sleep(th);
+				}
+			}
+
 			/* Catch assertions from prior take_step or from
 			 * between-ModelAction bugs (e.g., data races) */
 			if (has_asserted())