From 50e0465f724dc182d5d7504004e93f1a1b4644b9 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 18 Apr 2013 14:53:58 -0700
Subject: [PATCH 1/1] Add yield block support.  The idea is to not generate
 executions with yield actions.

While preventing yields doesn't preserve livelock, under the CHESS assumptions, it does allow us to reach all states.
---
 execution.cc | 17 +++++++++++++++++
 execution.h  |  1 +
 main.cc      | 10 ++++++++--
 params.h     |  1 +
 4 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/execution.cc b/execution.cc
index 47a6ebb..57ce6fe 100644
--- a/execution.cc
+++ b/execution.cc
@@ -264,6 +264,17 @@ bool ModelExecution::is_deadlocked() const
 	return blocking_threads;
 }
 
+bool ModelExecution::is_yieldblocked() const
+{
+	for (unsigned int i = 0; i < get_num_threads(); i++) {
+		thread_id_t tid = int_to_id(i);
+		Thread *t = get_thread(tid);
+		if (t->get_pending() && t->get_pending()->is_yield())
+			return true;
+	}
+	return false;
+}
+
 /**
  * Check if this is a complete execution. That is, have all thread completed
  * execution (rather than exiting because sleep sets have forced a redundant
@@ -273,6 +284,8 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
+	if (params->yieldblock && is_yieldblocked())
+		return false;
 	for (unsigned int i = 0; i < get_num_threads(); i++)
 		if (is_enabled(int_to_id(i)))
 			return false;
@@ -1200,6 +1213,8 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
 			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
+	} else if (params->yieldblock && curr->is_yield()) {
+		return false;
 	}
 
 	return true;
@@ -2659,6 +2674,8 @@ void ModelExecution::print_summary() const
 
 	model_print("Execution %d:", get_execution_number());
 	if (isfeasibleprefix()) {
+		if (params->yieldblock && is_yieldblocked())
+			model_print(" YIELD BLOCKED");
 		if (scheduler->all_threads_sleeping())
 			model_print(" SLEEP-SET REDUNDANT");
 		model_print("\n");
diff --git a/execution.h b/execution.h
index 1ba030b..7f63e6d 100644
--- a/execution.h
+++ b/execution.h
@@ -109,6 +109,7 @@ public:
 	bool is_feasible_prefix_ignore_relseq() const;
 	bool is_infeasible() const;
 	bool is_deadlocked() const;
+	bool is_yieldblocked() const;
 	bool too_many_steps() const;
 
 	ModelAction * get_next_backtrack();
diff --git a/main.cc b/main.cc
index 56eb311..1373e67 100644
--- a/main.cc
+++ b/main.cc
@@ -21,6 +21,7 @@ static void param_defaults(struct model_params *params)
 	params->maxfuturedelay = 6;
 	params->fairwindow = 0;
 	params->yieldon = false;
+	params->yieldblock = false;
 	params->sc_trace_analysis = false;
 	params->enabledcount = 1;
 	params->bound = 0;
@@ -57,19 +58,21 @@ static void print_usage(struct model_params *params)
 "                      priority for execution. Default: %d\n"
 "-y                    Turn on CHESS yield-based fairness support.\n"
 "                      Default: %d\n"
+"-Y                    Prohibit an execution from running a yield.\n"
+"                      Default: %d\n"
 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
 "-v                    Print verbose execution information.\n"
 "-u                    Value for uninitialized reads. Default: %u\n"
 "-c                    Use SC Trace Analysis.\n"
 "--                    Program arguments follow.\n\n",
-params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue);
+params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->yieldblock, params->enabledcount, params->bound, params->uninitvalue);
 	exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
-	const char *shortopts = "hycm:M:s:S:f:e:b:u:v";
+	const char *shortopts = "hyYcm:M:s:S:f:e:b:u:v";
 	int opt;
 	bool error = false;
 	while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {
@@ -110,6 +113,9 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 		case 'y':
 			params->yieldon = true;
 			break;
+		case 'Y':
+			params->yieldblock = true;
+			break;
 		default: /* '?' */
 			error = true;
 			break;
diff --git a/params.h b/params.h
index 946c801..043b2a5 100644
--- a/params.h
+++ b/params.h
@@ -9,6 +9,7 @@ struct model_params {
 	int maxreads;
 	int maxfuturedelay;
 	bool yieldon;
+	bool yieldblock;
 	bool sc_trace_analysis;
 	unsigned int fairwindow;
 	unsigned int enabledcount;
-- 
2.34.1