X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=9c3b4afa2986fac9ecce604e9de9394ebca6f3eb;hb=f269c2a1c390e82ae189bc690a750601f874283f;hp=48c73cfbeca2db10dd19148062bded4bfd9858e7;hpb=8b57ab066a2b74a81c4261482ba9030465eb0dbe;p=c11tester.git diff --git a/execution.cc b/execution.cc index 48c73cfb..9c3b4afa 100644 --- a/execution.cc +++ b/execution.cc @@ -118,6 +118,16 @@ static SnapVector * get_safe_ptr_vect_action(HashTable * hash, void * ptr) +{ + simple_action_list_t *tmp = hash->get(ptr); + if (tmp == NULL) { + tmp = new simple_action_list_t(); + hash->put(ptr, tmp); + } + return tmp; +} + /** @return a thread ID for a new Thread */ thread_id_t ModelExecution::get_next_id() { @@ -329,6 +339,10 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * read_from(curr, rf); get_thread(curr)->set_return_value(curr->get_return_value()); delete priorset; + //Update acquire fence clock vector + ClockVector * hbcv = get_hb_from_write(curr->get_reads_from()); + if (hbcv != NULL) + get_thread(curr)->get_acq_fence_cv()->merge(hbcv); return canprune && (curr->get_type() == ATOMIC_READ); } priorset->clear(); @@ -402,7 +416,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) state->locked = NULL; /* remove old wait action and disable this thread */ - action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); for (sllnode * it = waiters->begin(); it != NULL; it = it->getNext()) { ModelAction * wait = it->getVal(); if (wait->get_tid() == curr->get_tid()) { @@ -442,7 +456,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) break; } case ATOMIC_NOTIFY_ALL: { - action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); //activate all the waiting threads for (sllnode * rit = waiters->begin();rit != NULL;rit=rit->getNext()) { scheduler->wake(get_thread(rit->getVal())); @@ -451,7 +465,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) break; } case ATOMIC_NOTIFY_ONE: { - action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); if (waiters->size() != 0) { Thread * thread = fuzzer->selectNotify(waiters); scheduler->wake(thread); @@ -481,7 +495,7 @@ void ModelExecution::process_write(ModelAction *curr) * @param curr The ModelAction to process * @return True if synchronization was updated */ -bool ModelExecution::process_fence(ModelAction *curr) +void ModelExecution::process_fence(ModelAction *curr) { /* * fence-relaxed: no-op @@ -491,36 +505,9 @@ bool ModelExecution::process_fence(ModelAction *curr) * sequences * fence-seq-cst: MO constraints formed in {r,w}_modification_order */ - bool updated = false; if (curr->is_acquire()) { - action_list_t *list = &action_trace; - sllnode * rit; - /* Find X : is_read(X) && X --sb-> curr */ - for (rit = list->end();rit != NULL;rit=rit->getPrev()) { - ModelAction *act = rit->getVal(); - if (act == curr) - continue; - if (act->get_tid() != curr->get_tid()) - continue; - /* Stop at the beginning of the thread */ - if (act->is_thread_start()) - break; - /* Stop once we reach a prior fence-acquire */ - if (act->is_fence() && act->is_acquire()) - break; - if (!act->is_read()) - continue; - /* read-acquire will find its own release sequences */ - if (act->is_acquire()) - continue; - - /* Establish hypothetical release sequences */ - ClockVector *cv = get_hb_from_write(act->get_reads_from()); - if (cv != NULL && curr->get_cv()->merge(cv)) - updated = true; - } + curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv()); } - return updated; } /** @@ -1148,11 +1135,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) int tid = id_to_int(act->get_tid()); if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - act->setActionRef(list->add_back(act)); + list->addAction(act); } // Update action trace, a total order of all actions - act->setTraceRef(action_trace.add_back(act)); + action_trace.addAction(act); // Update obj_thrd_map, a per location, per thread, order of actions @@ -1164,7 +1151,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) new (&(*vec)[i]) action_list_t(); } if (!canprune && (act->is_read() || act->is_write())) - act->setThrdMapRef((*vec)[tid].add_back(act)); + (*vec)[tid].addAction(act); // Update thrd_last_action, the last action taken by each thread if ((int)thrd_last_action.size() <= tid) @@ -1180,43 +1167,17 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act)); + get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act); } } -sllnode* insertIntoActionList(action_list_t *list, ModelAction *act) { - sllnode * rit = list->end(); - modelclock_t next_seq = act->get_seq_number(); - if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq)) - return list->add_back(act); - else { - for(;rit != NULL;rit=rit->getPrev()) { - if (rit->getVal()->get_seq_number() <= next_seq) { - return list->insertAfter(rit, act); - } - } - return list->add_front(act); - } +void insertIntoActionList(action_list_t *list, ModelAction *act) { + list->addAction(act); } -sllnode* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { - sllnode * rit = list->end(); - modelclock_t next_seq = act->get_seq_number(); - if (rit == NULL) { - act->create_cv(NULL); - return list->add_back(act); - } else if (rit->getVal()->get_seq_number() <= next_seq) { - act->create_cv(rit->getVal()); - return list->add_back(act); - } else { - for(;rit != NULL;rit=rit->getPrev()) { - if (rit->getVal()->get_seq_number() <= next_seq) { - act->create_cv(rit->getVal()); - return list->insertAfter(rit, act); - } - } - return list->add_front(act); - } +void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { + act->create_cv(NULL); + list->addAction(act); } /** @@ -1230,7 +1191,7 @@ sllnode* insertIntoActionListAndSetCV(action_list_t *list, ModelA void ModelExecution::add_normal_write_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act)); + insertIntoActionListAndSetCV(&action_trace, act); // Update obj_thrd_map, a per location, per thread, order of actions SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); @@ -1240,7 +1201,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act)); + insertIntoActionList(&(*vec)[tid],act); ModelAction * lastact = thrd_last_action[tid]; // Update thrd_last_action, the last action taken by each thrad @@ -1258,7 +1219,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) { for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - write->setActionRef((*vec)[tid].add_back(write)); + (*vec)[tid].addAction(write); } /** @@ -1561,7 +1522,7 @@ void ModelExecution::print_tail() int length = 25; int counter = 0; SnapList list; - for (it = action_trace.end(); it != NULL; it = it->getPrev()) { + for (it = action_trace.end();it != NULL;it = it->getPrev()) { if (counter > length) break; @@ -1716,36 +1677,22 @@ Thread * ModelExecution::take_step(ModelAction *curr) void ModelExecution::removeAction(ModelAction *act) { { - sllnode * listref = act->getTraceRef(); - if (listref != NULL) { - action_trace.erase(listref); - } + action_trace.removeAction(act); } { - sllnode * listref = act->getThrdMapRef(); - if (listref != NULL) { - SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); - (*vec)[act->get_tid()].erase(listref); - } + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + (*vec)[act->get_tid()].removeAction(act); } if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - list->erase(listref); - } + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + list->removeAction(act); } else if (act->is_wait()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref); - } + void *mutex_loc = (void *) act->get_value(); + get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act); } else if (act->is_free()) { - sllnode * listref = act->getActionRef(); - if (listref != NULL) { - SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); - (*vec)[act->get_tid()].erase(listref); - } + SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); + (*vec)[act->get_tid()].removeAction(act); + //Clear it from last_sc_map if (obj_last_sc_map.get(act->get_location()) == act) { obj_last_sc_map.remove(act->get_location());