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
*/
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;
/**
* @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.
thread_blocking_check_promises(blocking, get_thread(curr));
return false;
}
+ } else if (params->yieldblock && curr->is_yield()) {
+ return false;
}
return true;
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");