Fix bug that prevents graph generation from compiling.

[model-checker.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index c8c4b89ac2910abd7024b531ea1bed5e97187faa..f2c50c4321c67cd83da4c905ac1bcd652307b4a0 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,7 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
-               struct model_params *params,
+               const struct model_params *params,
                Scheduler *scheduler,
                NodeStack *node_stack) :
        model(m),
@@ -264,6 +264,28 @@ bool ModelExecution::is_deadlocked() const
        return blocking_threads;
 }
 
+/**
+ * @brief Check if we are yield-blocked
+ *
+ * A program can be "yield-blocked" if all threads are ready to execute a
+ * yield.
+ *
+ * @return True if the program is yield-blocked; false otherwise
+ */
+bool ModelExecution::is_yieldblocked() const
+{
+       if (!params->yieldblock)
+               return false;
+
+       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 +295,8 @@ bool ModelExecution::is_deadlocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
+       if (is_yieldblocked())
+               return false;
        for (unsigned int i = 0; i < get_num_threads(); i++)
                if (is_enabled(int_to_id(i)))
                        return false;
@@ -1181,9 +1205,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai
 /**
  * @brief Check whether a model action is enabled.
  *
- * Checks whether a lock or join operation would be successful (i.e., is the
- * lock already locked, or is the joined thread already complete). If not, put
- * the action in a waiter list.
+ * Checks whether an operation would be successful (i.e., is a lock already
+ * locked, or is the joined thread already complete).
+ *
+ * For yield-blocking, yields are never enabled.
  *
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
@@ -1200,6 +1225,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;
@@ -2616,7 +2643,7 @@ void ModelExecution::dumpGraph(char *filename) const
        mo_graph->dumpNodes(file);
        ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
-       for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) {
+       for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
                ModelAction *act = *it;
                if (act->is_read()) {
                        mo_graph->dot_print_node(file, act);
@@ -2659,6 +2686,8 @@ void ModelExecution::print_summary() const
 
        model_print("Execution %d:", get_execution_number());
        if (isfeasibleprefix()) {
+               if (is_yieldblocked())
+                       model_print(" YIELD BLOCKED");
                if (scheduler->all_threads_sleeping())
                        model_print(" SLEEP-SET REDUNDANT");
                model_print("\n");