Merge remote 'yield' work

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index d15a094f7d8049e1a1e81ed8ac78527b6d1ca66a..55d5d0d43cfab46bac7a4d8e51987231526f6c33 100644 (file)
--- 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);
@@ -2814,7 +2834,9 @@ static void print_list(action_list_t *list)
        unsigned int hash = 0;
 
        for (it = list->begin(); it != list->end(); it++) {
-               (*it)->print();
+               const ModelAction *act = *it;
+               if (act->get_seq_number() > 0)
+                       act->print();
                hash = hash^(hash<<3)^((*it)->hash());
        }
        model_print("HASH %u\n", hash);