From: Brian Norris Date: Wed, 19 Sep 2012 02:29:05 +0000 (-0700) Subject: model: replace list type with action_list_t X-Git-Tag: pldi2013~177^2^2 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3bab2ac6bca956b302a62d2ee60e7d2b48e8258b;p=model-checker.git model: replace list type with action_list_t --- diff --git a/model.cc b/model.cc index 52b2e17..ec99b9a 100644 --- a/model.cc +++ b/model.cc @@ -30,7 +30,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, uintptr_t, 4>()), + lazy_sync_with_release(new HashTable()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), mo_graph(new CycleGraph()), @@ -1043,7 +1043,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 */ - std::list *list; + action_list_t *list; list = lazy_sync_with_release->get_safe_ptr(act->get_location()); list->push_back(act); (*lazy_sync_size)++; @@ -1065,13 +1065,13 @@ 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) { - std::list *list; + action_list_t *list; list = lazy_sync_with_release->getptr(location); if (!list) return false; bool updated = false; - std::list::iterator it = list->begin(); + action_list_t::iterator it = list->begin(); while (it != list->end()) { ModelAction *act = *it; const ModelAction *rf = act->get_reads_from(); diff --git a/model.h b/model.h index eb50d37..fd6e6c2 100644 --- a/model.h +++ b/model.h @@ -163,7 +163,7 @@ private: * This structure maps its lists by object location. Each ModelAction * in the lists should be an acquire operation. */ - HashTable, uintptr_t, 4> *lazy_sync_with_release; + HashTable *lazy_sync_with_release; /** * Represents the total size of the