model: maintain a count of the pending lazy synchronizations

lazy_sync_size should be the sum of the size of all the lists in
lazy_sync_with_release.

diff --git a/model.cc b/model.cc
index 43530fe12c25e2ecafa4af78cbb5eb3008b6190d..36b7b4490ffe5bb3c012e3baf3e439f719da2932 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. */
@@ -665,6 +666,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 +713,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++;
        }
 

diff --git a/model.h b/model.h
index 9762eb0c40ef26c5efc92887c6f4f18864e620a0..b2f7897a310f7dc66fa88ce970893c43c252059c 100644 (file)
--- a/model.h
+++ b/model.h
@@ -39,6 +39,9 @@ struct model_snapshot_members {
        modelclock_t used_sequence_numbers;
        Thread *nextThread;
        ModelAction *next_backtrack;
+
+       /** @see ModelChecker::lazy_sync_size */
+       unsigned int lazy_sync_size;
 };
 
 /** @brief The central structure for model-checking */
@@ -142,6 +145,14 @@ private:
         */
        HashTable<void *, std::list<ModelAction *>, uintptr_t, 4> *lazy_sync_with_release;
 
+       /**
+        * Represents the total size of the
+        * ModelChecker::lazy_sync_with_release lists. This count should be
+        * snapshotted, so it is actually a pointer to a location within
+        * ModelChecker::priv
+        */
+       unsigned int *lazy_sync_size;
+
        std::vector<ModelAction *> *thrd_last_action;
        NodeStack *node_stack;