Merge remote 'yield' work
authorBrian Norris <banorris@uci.edu>
Wed, 6 Mar 2013 03:04:57 +0000 (19:04 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 6 Mar 2013 03:05:06 +0000 (19:05 -0800)
1  2 
model.cc

diff --combined model.cc
index cd703edf329ef3245b8bcded411c540b3ac3ab22,8e513a3a47c972d70b0e9c3c6a9d72ba3e867171..55d5d0d43cfab46bac7a4d8e51987231526f6c33
+++ b/model.cc
@@@ -822,6 -822,21 +822,21 @@@ void ModelChecker::set_backtracking(Mod
                        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 +1491,11 @@@ ModelAction * ModelChecker::check_curre
  
        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,9 -2834,7 +2834,9 @@@ static void print_list(action_list_t *l
        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);