X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=f2c50c4321c67cd83da4c905ac1bcd652307b4a0;hb=b756884bdc8b22457243b76982cf10dc4598f927;hp=57ce6fef4cc62b8ff8aff79970bdfe2de786f4b3;hpb=50e0465f724dc182d5d7504004e93f1a1b4644b9;p=model-checker.git

diff --git a/execution.cc b/execution.cc
index 57ce6fe..f2c50c4 100644
--- a/execution.cc
+++ b/execution.cc
@@ -264,8 +264,19 @@ 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);
@@ -284,7 +295,7 @@ bool ModelExecution::is_yieldblocked() const
  */
 bool ModelExecution::is_complete_execution() const
 {
-	if (params->yieldblock && is_yieldblocked())
+	if (is_yieldblocked())
 		return false;
 	for (unsigned int i = 0; i < get_num_threads(); i++)
 		if (is_enabled(int_to_id(i)))
@@ -1194,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.
@@ -2631,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);
@@ -2674,7 +2686,7 @@ void ModelExecution::print_summary() const
 
 	model_print("Execution %d:", get_execution_number());
 	if (isfeasibleprefix()) {
-		if (params->yieldblock && is_yieldblocked())
+		if (is_yieldblocked())
 			model_print(" YIELD BLOCKED");
 		if (scheduler->all_threads_sleeping())
 			model_print(" SLEEP-SET REDUNDANT");