Merge branch 'norris'

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index e4757bc6f0d0b919417e60ed9018e0bcd0e86301..d082d8358b8d2a1da69f94cec113bc6982335ceb 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>()),
@@ -275,6 +275,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;
@@ -1067,24 +1081,32 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  */
 bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
-       if (!rf) {
-               /* read from future: need to settle this later */
-               return false; /* incomplete */
-       }
+       while (rf) {
+               ASSERT(rf->is_write());
 
-       ASSERT(rf->is_write());
+               if (rf->is_release())
+                       release_heads->push_back(rf);
+               if (!rf->is_rmw())
+                       break; /* End of RMW chain */
 
-       if (rf->is_release())
-               release_heads->push_back(rf);
-       if (rf->is_rmw()) {
-               /* We need a RMW action that is both an acquire and release to stop */
                /** @todo Need to be smarter here...  In the linux lock
                 * example, this will run to the beginning of the program for
                 * every acquire. */
+               /** @todo The way to be smarter here is to keep going until 1
+                * thread has a release preceded by an acquire and you've seen
+                *       both. */
+
+               /* acq_rel RMW is a sufficient stopping condition */
                if (rf->is_acquire() && rf->is_release())
                        return true; /* complete */
-               return release_seq_head(rf->get_reads_from(), release_heads);
+
+               rf = rf->get_reads_from();
+       };
+       if (!rf) {
+               /* read from future: need to settle this later */
+               return false; /* incomplete */
        }
+
        if (rf->is_release())
                return true; /* complete */