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.

diff --git a/execution.cc b/execution.cc
index 47a6ebbff7b76dfbbd7f0ec9898606e4f469d29e..57ce6fef4cc62b8ff8aff79970bdfe2de786f4b3 100644 (file)
--- 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 1ba030b6d93a2d61fc97009dcf869db4c634e6ce..7f63e6d99812c98f5732d35c52a1e04f8691ac17 100644 (file)
--- 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 56eb311dd86f755d45989972d1fe165be74c60a2..1373e672b6492b9a05dadacd15c92c34620b1fd0 100644 (file)
--- 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 946c801e4cce5aac707d0b1c3c7e9a204401ade5..043b2a5c530bd8a4ed1d78b7f1f81007757c1cb2 100644 (file)
--- 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;