X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=55d5d0d43cfab46bac7a4d8e51987231526f6c33;hp=cd703edf329ef3245b8bcded411c540b3ac3ab22;hb=90471233ff4dcca9a196152574dca4e7cf183698;hpb=ff3ab0abac18649da161a495781c3925cbcd62a4

diff --git a/model.cc b/model.cc
index cd703ed..55d5d0d 100644
--- a/model.cc
+++ b/model.cc
@@ -822,6 +822,21 @@ void ModelChecker::set_backtracking(ModelAction *act)
 			if (unfair)
 				continue;
 		}
+
+		/* See if CHESS-like yield fairness allows */
+		if (model->params.yieldon) {
+			bool unfair = false;
+			for (int t = 0; t < node->get_num_threads(); t++) {
+				thread_id_t tother = int_to_id(t);
+				if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
+					unfair = true;
+					break;
+				}
+			}
+			if (unfair)
+				continue;
+		}
+		
 		/* Cache the latest backtracking point */
 		set_latest_backtrack(prev);
 
@@ -1476,6 +1491,11 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
 	wake_up_sleeping_actions(curr);
 
+	/* Compute fairness information for CHESS yield algorithm */
+	if (model->params.yieldon) {
+		curr->get_node()->update_yield(scheduler);
+	}
+
 	/* Add the action to lists before any other model-checking tasks */
 	if (!second_part_of_rmw)
 		add_action_to_lists(curr);