From f71cd7c31df98cfc814254da887de9a30c53b31e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 20 Sep 2012 14:00:13 -0700 Subject: [PATCH] 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'. --- model.cc | 38 +++++++++++++++++--------------------- model.h | 22 +++++----------------- 2 files changed, 22 insertions(+), 38 deletions(-) diff --git a/model.cc b/model.cc index 0283911..e4757bc 100644 --- a/model.cc +++ b/model.cc @@ -32,7 +32,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), - lazy_sync_with_release(new HashTable()), + pending_acq_rel_seq(new std::vector()), thrd_last_action(new std::vector(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::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 1370424..47f5139 100644 --- 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 *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 *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 *pending_acq_rel_seq; std::vector *thrd_last_action; NodeStack *node_stack; -- 2.34.1