fairness changes...

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 64c1daa5d8f2b52aa561b50cbd2a07a65853ec84..03a0c689431c90720ec56a1020ef21344920ac08 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -20,10 +20,10 @@ ModelChecker *model;
 /** @brief Constructor */
 ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
+       params(params),
        scheduler(new Scheduler()),
        num_executions(0),
        num_feasible_executions(0),
-       params(params),
        diverge(NULL),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
@@ -277,6 +277,20 @@ void ModelChecker::set_backtracking(ModelAction *act)
                if (node->has_been_explored(tid))
                        continue;
 
+               /* See if fairness allows */
+               if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
+                       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(tother)) {
+                                       unfair=true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+
                /* Cache the latest backtracking point */
                if (!priv->next_backtrack || *prev > *priv->next_backtrack)
                        priv->next_backtrack = prev;
@@ -1233,7 +1247,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 
                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator it = action_trace->rbegin();
-                       while ((*it) != act) {
+                       for (; (*it) != act; it++) {
                                ModelAction *propagate = *it;
                                if (act->happens_before(propagate)) {
                                        propagate->synchronize_with(act);