main: add "maxreads" parameter

[cdsspec-compiler.git] / model.cc

diff --git a/model.cc b/model.cc
index 43530fe12c25e2ecafa4af78cbb5eb3008b6190d..c8af6cc4f5bfb2d2c878e6aa035e2cf712d56e29 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -39,6 +39,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
        /* First thread created will have id INITIAL_THREAD_ID */
        priv->next_thread_id = INITIAL_THREAD_ID;
+
+       lazy_sync_size = &priv->lazy_sync_size;
 }
 
 /** @brief Destructor */
@@ -372,9 +374,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
 /** @returns whether the current partial trace must be a prefix of a
  * feasible trace. */
-
 bool ModelChecker::isfeasibleprefix() {
-       return promises->size()==0;
+       return promises->size() == 0 && *lazy_sync_size == 0;
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -565,7 +566,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
        if (rf->is_release())
                release_heads->push_back(rf);
        if (rf->is_rmw()) {
-               if (rf->is_acquire())
+               /* 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. */
+               if (rf->is_acquire() && rf->is_release())
                        return true; /* complete */
                return release_seq_head(rf->get_reads_from(), release_heads);
        }
@@ -665,6 +670,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act,
                std::list<ModelAction *> *list;
                list = lazy_sync_with_release->get_safe_ptr(act->get_location());
                list->push_back(act);
+               (*lazy_sync_size)++;
        }
 }
 
@@ -711,9 +717,10 @@ bool ModelChecker::resolve_release_sequences(void *location)
                                        propagate->synchronize_with(act);
                        }
                }
-               if (complete)
+               if (complete) {
                        it = list->erase(it);
-               else
+                       (*lazy_sync_size)--;
+               } else
                        it++;
        }