X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=40aa6814c84e6bd47d006b47b47eb8e532797cf5;hp=cd277c55daa5ad1471380f6450cd72f51c45977c;hb=a954c752ac2dd5458564fa75b22ab9f488009733;hpb=9b5fe3ab5dd51f3dbb3926c6887a7c163ec145c7 diff --git a/execution.cc b/execution.cc index cd277c55..40aa6814 100644 --- a/execution.cc +++ b/execution.cc @@ -63,13 +63,13 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_fence_release(), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), - fuzzer(new NewFuzzer()), + fuzzer(new Fuzzer()), isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); add_thread(model_thread); - fuzzer->register_engine(m->get_history(), this); + fuzzer->register_engine(this); scheduler->register_engine(this); #ifdef TLS pthread_key_create(&pthreadkey, tlsdestructor); @@ -283,7 +283,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { * Processes a read model action. * @param curr is the read model action to process. * @param rf_set is the set of model actions we can possibly read from - * @return True if processing this read updates the mo_graph. + * @return True if the read can be pruned from the thread map list. */ bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { @@ -320,12 +320,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * 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(); - curr->setThrdMapRef(NULL); - } - return true; + return canprune && (curr->get_type() == ATOMIC_READ); } priorset->clear(); (*rf_set)[index] = rf_set->back(); @@ -728,15 +723,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (newly_explored && curr->is_read()) rf_set = build_may_read_from(curr); + bool canprune = false; + if (curr->is_read() && !second_part_of_rmw) { - process_read(curr, rf_set); + canprune = process_read(curr, rf_set); delete rf_set; } else ASSERT(rf_set == NULL); /* Add the action to lists */ if (!second_part_of_rmw) - add_action_to_lists(curr); + add_action_to_lists(curr, canprune); if (curr->is_write()) add_write_to_lists(curr); @@ -1118,7 +1115,7 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { * * @param act is the ModelAction to add. */ -void ModelExecution::add_action_to_lists(ModelAction *act) +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()) { @@ -1138,7 +1135,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act) for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - act->setThrdMapRef((*vec)[tid].add_back(act)); + if (!canprune) + act->setThrdMapRef((*vec)[tid].add_back(act)); // Update thrd_last_action, the last action taken by each thread if ((int)thrd_last_action.size() <= tid) @@ -1688,12 +1686,18 @@ void ModelExecution::removeAction(ModelAction *act) { void *mutex_loc = (void *) act->get_value(); get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref); } - } else if (act->is_write()) { + } 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); } + //Clear it from last_sc_map + if (obj_last_sc_map.get(act->get_location()) == act) { + obj_last_sc_map.remove(act->get_location()); + } + + //Remove from Cyclegraph mo_graph->freeAction(act); } @@ -1771,25 +1775,44 @@ void ModelExecution::collectActions() { } } } + for (sllnode * it2 = action_trace.end();it2 != it;it2=it2->getPrev()) { + ModelAction *act = it2->getVal(); + if (act->is_read() && act->get_reads_from()->is_free()) { + act->set_read_from(NULL); + } + } for (;it != NULL;) { ModelAction *act = it->getVal(); //Do iteration early since we may delete node... it=it->getPrev(); + bool islastact = false; + ModelAction *lastact = get_last_action(act->get_tid()); + if (act == lastact) { + Thread * th = get_thread(act); + islastact = !th->is_complete(); + } + if (act->is_read()) { - if (act->get_reads_from()->is_free()) { + if (!islastact && act->get_reads_from()->is_free()) { removeAction(act); delete act; - } else { - const ModelAction *rel_fence =act->get_last_fence_release(); - if (rel_fence != NULL) { - modelclock_t relfenceseq = rel_fence->get_seq_number(); - thread_id_t relfence_tid = rel_fence->get_tid(); - modelclock_t tid_clock = cvmin->getClock(relfence_tid); - //Remove references to irrelevant release fences - if (relfenceseq <= tid_clock) - act->set_last_fence_release(NULL); - } + continue; + } + if (islastact && act->get_reads_from()->is_free()) { + act->set_read_from(NULL); + } + + const ModelAction *rel_fence =act->get_last_fence_release(); + if (rel_fence != NULL) { + modelclock_t relfenceseq = rel_fence->get_seq_number(); + thread_id_t relfence_tid = rel_fence->get_tid(); + modelclock_t tid_clock = cvmin->getClock(relfence_tid); + //Remove references to irrelevant release fences + if (relfenceseq <= tid_clock) + act->set_last_fence_release(NULL); } + } else if (islastact) { + continue; } else if (act->is_free()) { removeAction(act); delete act; @@ -1825,6 +1848,11 @@ void ModelExecution::collectActions() { removeAction(act); delete act; } + } else if (act->is_create()) { + if (act->get_thread_operand()->is_complete()) { + removeAction(act); + delete act; + } } else { removeAction(act); delete act;