model: flatten "pending acquire/release sequence" structure

This structure should just be a simple flat array, so that we can simply
iterate through all acquire operations with pending release sequences. There
probably wasn't much to be saved by organizing this structure as a hash table
of lists; if so, I can add the complexity back in later.

This eliminates the need for a separate 'lazy_sync_size' count and renames
'lazy_sync_with_release' to 'pending_acq_rel_seq'.

diff --git a/model.cc b/model.cc
index 0283911b6eea07e57c7b7266fe3c80fc2d755595..e4757bc6f0d0b919417e60ed9018e0bcd0e86301 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -32,7 +32,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
        promises(new std::vector<Promise *>()),
        futurevalues(new std::vector<struct PendingFutureValue>()),
-       lazy_sync_with_release(new HashTable<void *, action_list_t, uintptr_t, 4>()),
+       pending_acq_rel_seq(new std::vector<ModelAction *>()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
        mo_graph(new CycleGraph()),
@@ -44,8 +44,6 @@ 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 */
@@ -64,7 +62,7 @@ ModelChecker::~ModelChecker()
                delete (*promises)[i];
        delete promises;
 
-       delete lazy_sync_with_release;
+       delete pending_acq_rel_seq;
 
        delete thrd_last_action;
        delete node_stack;
@@ -677,7 +675,7 @@ bool ModelChecker::promises_expired() {
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
-       return promises->size() == 0 && *lazy_sync_size == 0;
+       return promises->size() == 0 && pending_acq_rel_seq->size() == 0;
 }
 
 /** @return whether the current partial trace is feasible. */
@@ -1185,10 +1183,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
        complete = release_seq_head(rf, release_heads);
        if (!complete) {
                /* add act to 'lazy checking' list */
-               action_list_t *list;
-               list = lazy_sync_with_release->get_safe_ptr(act->get_location());
-               list->push_back(act);
-               (*lazy_sync_size)++;
+               pending_acq_rel_seq->push_back(act);
        }
 }
 
@@ -1199,7 +1194,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
  * modification order information is present at the time an action occurs.
  *
  * @param location The location/object that should be checked for release
- * sequence resolutions
+ * sequence resolutions. A NULL value means to check all locations.
  * @param work_queue The work queue to which to add work items as they are
  * generated
  * @return True if any updates occurred (new synchronization, new mo_graph
@@ -1207,15 +1202,17 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
  */
 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
-       action_list_t *list;
-       list = lazy_sync_with_release->getptr(location);
-       if (!list)
-               return false;
-
        bool updated = false;
-       action_list_t::iterator it = list->begin();
-       while (it != list->end()) {
+       std::vector<ModelAction *>::iterator it = pending_acq_rel_seq->begin();
+       while (it != pending_acq_rel_seq->end()) {
                ModelAction *act = *it;
+
+               /* Only resolve sequences on the given location, if provided */
+               if (location && act->get_location() != location) {
+                       it++;
+                       continue;
+               }
+
                const ModelAction *rf = act->get_reads_from();
                rel_heads_list_t release_heads;
                bool complete;
@@ -1242,10 +1239,9 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                                }
                        }
                }
-               if (complete) {
-                       it = list->erase(it);
-                       (*lazy_sync_size)--;
-               } else
+               if (complete)
+                       it = pending_acq_rel_seq->erase(it);
+               else
                        it++;
        }
 

diff --git a/model.h b/model.h
index 13704241a83285dba37651a5e7b8ea699a1d2281..47f5139ba1b82ebe63c804b32945bffd31325bd0 100644 (file)
--- a/model.h
+++ b/model.h
@@ -51,9 +51,6 @@ 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 */
@@ -164,21 +161,12 @@ private:
        std::vector<struct PendingFutureValue> *futurevalues;
 
        /**
-        * Collection of lists of objects that might synchronize with one or
-        * more release sequence. Release sequences might be determined lazily
-        * as promises are fulfilled and modification orders are established.
-        * This structure maps its lists by object location. Each ModelAction
-        * in the lists should be an acquire operation.
-        */
-       HashTable<void *, action_list_t, 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
+        * List of acquire actions that might synchronize with one or more
+        * release sequence. Release sequences might be determined lazily as
+        * promises are fulfilled and modification orders are established. Each
+        * ModelAction in this list must be an acquire operation.
         */
-       unsigned int *lazy_sync_size;
+       std::vector<ModelAction *> *pending_acq_rel_seq;
 
        std::vector<ModelAction *> *thrd_last_action;
        NodeStack *node_stack;