X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=f492af30d35b39ac00fbb080184cb6ec11b523f7;hb=7524803854c2de38c0311fe5037e3c17105ccfaa;hp=0122922d376ca03a742f03729585f3c48db7b09a;hpb=ea4611c1fc3b580020afbc04d531e4bc10fcca9c;p=model-checker.git diff --git a/model.cc b/model.cc index 0122922..f492af3 100644 --- a/model.cc +++ b/model.cc @@ -85,12 +85,12 @@ ModelChecker::ModelChecker(struct model_params params) : obj_map(new HashTable()), lock_waiters_map(new HashTable()), condvar_waiters_map(new HashTable()), - obj_thrd_map(new HashTable *, uintptr_t, 4 >()), - promises(new std::vector< Promise *, SnapshotAlloc >()), - futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), - pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc >()), - thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc >(1)), - thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc >()), + obj_thrd_map(new HashTable *, uintptr_t, 4 >()), + promises(new snap_vector< Promise * >()), + futurevalues(new snap_vector< struct PendingFutureValue >()), + pending_rel_seqs(new snap_vector< struct release_seq * >()), + thrd_last_action(new snap_vector< ModelAction * >(1)), + thrd_last_fence_release(new snap_vector< ModelAction * >()), node_stack(new NodeStack()), priv(new struct model_snapshot_members()), mo_graph(new CycleGraph()) @@ -137,11 +137,11 @@ static action_list_t * get_safe_ptr_action(HashTable * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) +static snap_vector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) { - std::vector *tmp = hash->get(ptr); + snap_vector *tmp = hash->get(ptr); if (tmp == NULL) { - tmp = new std::vector(); + tmp = new snap_vector(); hash->put(ptr, tmp); } return tmp; @@ -1704,7 +1704,7 @@ bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, con if (!mo_graph->checkReachable(rf, other_rf)) return false; - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())]; action_list_t::reverse_iterator rit = list->rbegin(); ASSERT((*rit) == curr); @@ -1747,7 +1747,7 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const curr->get_node()->get_read_from_promise_size() <= 1) return true; - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); ASSERT(tid < (int)thrd_lists->size()); action_list_t *list = &(*thrd_lists)[tid]; @@ -1805,7 +1805,7 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const template bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) { - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_read()); @@ -1913,7 +1913,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf) */ bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc > *send_fv) { - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -2057,7 +2057,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, cons */ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); unsigned int i; /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -2158,7 +2158,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, release_heads->push_back(fence_release); int tid = id_to_int(rf->get_tid()); - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -2301,7 +2301,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *acquire, bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue) { bool updated = false; - std::vector< struct release_seq *, SnapshotAlloc >::iterator it = pending_rel_seqs->begin(); + snap_vector< struct release_seq * >::iterator it = pending_rel_seqs->begin(); while (it != pending_rel_seqs->end()) { struct release_seq *pending = *it; ModelAction *acquire = pending->acquire; @@ -2382,7 +2382,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act) if (uninit) action_trace->push_front(uninit); - std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); + snap_vector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -2405,7 +2405,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act) void *mutex_loc = (void *) act->get_value(); get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); - std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); + snap_vector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -2724,7 +2724,7 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) */ void ModelChecker::build_may_read_from(ModelAction *curr) { - std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); + snap_vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read());