X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=8e513a3a47c972d70b0e9c3c6a9d72ba3e867171;hb=fa36db2da01d7da10e0cd375fda3c2db4ce3a05b;hp=d15a094f7d8049e1a1e81ed8ac78527b6d1ca66a;hpb=56bd79d6fa2953585375f72cf061355fecd2c725;p=model-checker.git

diff --git a/model.cc b/model.cc
index d15a094..8e513a3 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);