X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=2c08711eee0d1a655272bd56f1adf0d900ef599d;hb=bac8bc0661e904fc2b1b9aba07d239679483b2b4;hp=99f86195713523cb02791fb8ae75fcc309a1b0ec;hpb=e9992398715ddf04785b93a5a0e9b60e77a15b21;p=c11tester.git diff --git a/execution.cc b/execution.cc index 99f86195..2c08711e 100644 --- a/execution.cc +++ b/execution.cc @@ -64,7 +64,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack thrd_last_fence_release(), node_stack(node_stack), priv(new struct model_snapshot_members ()), - mo_graph(new CycleGraph()), + mo_graph(new CycleGraph()), fuzzer(new Fuzzer()) { /* Initialize a model-checker thread, for special ModelActions */ @@ -109,18 +109,6 @@ static SnapVector * get_safe_ptr_vect_action(HashTable *wrv = obj_thrd_map.get(obj); - if (wrv==NULL) - return NULL; - unsigned int thread=id_to_int(tid); - if (thread < wrv->size()) - return &(*wrv)[thread]; - else - return NULL; -} - /** @return a thread ID for a new Thread */ thread_id_t ModelExecution::get_next_id() { @@ -272,7 +260,7 @@ bool ModelExecution::is_complete_execution() const * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { SnapVector * priorset = new SnapVector(); while(true) { @@ -282,14 +270,18 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector * ASSERT(rf); - - if (r_modification_order(curr, rf, priorset)) { + bool canprune = false; + if (r_modification_order(curr, rf, priorset, &canprune)) { for(unsigned int i=0;isize();i++) { mo_graph->addEdge((*priorset)[i], rf); } read_from(curr, rf); get_thread(curr)->set_return_value(curr->get_return_value()); delete priorset; + if (canprune && curr->get_type() == ATOMIC_READ) { + int tid = id_to_int(curr->get_tid()); + (*obj_thrd_map.get(curr->get_location()))[tid].pop_back(); + } return; } priorset->clear(); @@ -347,6 +339,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) } case ATOMIC_WAIT: case ATOMIC_UNLOCK: { + //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE... + /* wake up the other threads */ for (unsigned int i = 0;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); @@ -374,8 +368,10 @@ bool ModelExecution::process_mutex(ModelAction *curr) } case ATOMIC_NOTIFY_ONE: { action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); - Thread * thread = fuzzer->selectNotify(waiters); - scheduler->wake(thread); + if (waiters->size() != 0) { + Thread * thread = fuzzer->selectNotify(waiters); + scheduler->wake(thread); + } break; } @@ -685,7 +681,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (!second_part_of_rmw && curr->get_type() != NOOP) add_action_to_lists(curr); - SnapVector * rf_set = NULL; + SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) rf_set = build_may_read_from(curr); @@ -774,7 +770,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { * @return True if modification order edges were added; false otherwise */ -bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset) +bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset, bool * canprune) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -782,24 +778,30 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * /* Last SC fence in the current thread */ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); - ModelAction *last_sc_write = NULL; - if (curr->is_seqcst()) - last_sc_write = get_last_seq_cst_write(curr); + int tid = curr->get_tid(); + ModelAction *prev_same_thread = NULL; /* Iterate over all threads */ - for (i = 0;i < thrd_lists->size();i++) { - /* Last SC fence in thread i */ + for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) { + /* Last SC fence in thread tid */ ModelAction *last_sc_fence_thread_local = NULL; - if (int_to_id((int)i) != curr->get_tid()) - last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL); + if (i != 0) + last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL); - /* Last SC fence in thread i, before last SC fence in current thread */ + /* Last SC fence in thread tid, before last SC fence in current thread */ ModelAction *last_sc_fence_thread_before = NULL; if (last_sc_fence_local) - last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local); + last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local); + + //Only need to iterate if either hb has changed for thread in question or SC fence after last operation... + if (prev_same_thread != NULL && + (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) && + (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) { + continue; + } /* Iterate over actions in thread, starting from most recent */ - action_list_t *list = &(*thrd_lists)[i]; + action_list_t *list = &(*thrd_lists)[tid]; action_list_t::reverse_iterator rit; for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; @@ -847,6 +849,12 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * * before" curr */ if (act->happens_before(curr)) { + if (i==0) { + if (last_sc_fence_local == NULL || + (*last_sc_fence_local < *prev_same_thread)) { + prev_same_thread = act; + } + } if (act->is_write()) { if (mo_graph->checkReachable(rf, act)) return false; @@ -857,6 +865,11 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * if (mo_graph->checkReachable(rf, prevrf)) return false; priorset->push_back(prevrf); + } else { + if (act->get_tid() == curr->get_tid()) { + //Can prune curr from obj list + *canprune = true; + } } } break; @@ -1313,7 +1326,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) { * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) +SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -1324,7 +1337,7 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu if (curr->is_seqcst()) last_sc_write = get_last_seq_cst_write(curr); - SnapVector * rf_set = new SnapVector(); + SnapVector * rf_set = new SnapVector(); /* Iterate over all threads */ for (i = 0;i < thrd_lists->size();i++) { @@ -1332,10 +1345,21 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + const ModelAction *act = *rit; /* Only consider 'write' actions */ - if (!act->is_write() || act == curr) + if (!act->is_write()) { + if (act != curr && act->is_read() && act->happens_before(curr)) { + const ModelAction *tmp = act->get_reads_from(); + if (((unsigned int) id_to_int(tmp->get_tid()))==i) + act = tmp; + else + break; + } else + continue; + } + + if (act == curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */