Add yield block support. The idea is to not generate executions with yield actions.
authorBrian Demsky <bdemsky@uci.edu>
Thu, 18 Apr 2013 21:53:58 +0000 (14:53 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Thu, 18 Apr 2013 21:53:58 +0000 (14:53 -0700)
While preventing yields doesn't preserve livelock, under the CHESS assumptions, it does allow us to reach all states.

execution.cc
execution.h
main.cc
params.h

index 47a6ebb..57ce6fe 100644 (file)
@@ -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");
index 1ba030b..7f63e6d 100644 (file)
@@ -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 (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;
index 946c801..043b2a5 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;