X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=bfb93278cfa7b2deb8b7e5ad1bed6a38ad76a170;hp=f5ab21e2e9db74675eb99c643fa13b74137ea0b1;hb=527eb9241e1b39b6ad4125a71b951d445d4e251e;hpb=e137463093ac5dbf0449d8eba9101d57b1fcbdeb diff --git a/execution.cc b/execution.cc index f5ab21e2..bfb93278 100644 --- a/execution.cc +++ b/execution.cc @@ -58,7 +58,10 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : obj_map(), condvar_waiters_map(), obj_thrd_map(), + obj_wr_thrd_map(), + obj_last_sc_map(), mutex_map(), + cond_map(), thrd_last_action(1), thrd_last_fence_release(), priv(new struct model_snapshot_members ()), @@ -1612,7 +1615,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const { /* Do not split atomic RMW */ - if (curr->is_rmwr() && !paused_by_fuzzer(curr)) + if (curr->is_rmwr()) return get_thread(curr); /* Follow CREATE with the created thread */ /* which is not needed, because model.cc takes care of this */ @@ -1624,15 +1627,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons return NULL; } -/** @param act A read atomic action */ -bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const -{ - ASSERT(act->is_read()); - - // Actions paused by fuzzer have their sequence number reset to 0 - return act->get_seq_number() == 0; -} - /** * Takes the next step in the execution, if possible. * @param curr The current step to take @@ -1725,7 +1719,7 @@ ClockVector * ModelExecution::computeMinimalCV() { /** Sometimes we need to remove an action that is the most recent in the thread. This happens if it is mo before action in other threads. In that case we need to create a replacement latest ModelAction */ void ModelExecution::fixupLastAct(ModelAction *act) { - ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid())); + ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid())); newact->set_seq_number(get_next_seq_num()); newact->create_cv(act); newact->set_last_fence_release(act->get_last_fence_release()); @@ -1735,6 +1729,9 @@ void ModelExecution::fixupLastAct(ModelAction *act) { /** Compute which actions to free. */ void ModelExecution::collectActions() { + if (priv->used_sequence_numbers < params->traceminsize) + return; + //Compute minimal clock vector for all live threads ClockVector *cvmin = computeMinimalCV(); SnapVector * queue = new SnapVector(); @@ -1777,6 +1774,8 @@ void ModelExecution::collectActions() { CycleNode * prevnode = node->getInEdge(i); ModelAction * prevact = prevnode->getAction(); if (prevact->get_type() != READY_FREE) { + // Save the original action type + prevact->set_original_type(prevact->get_type()); prevact->set_free(); queue->push_back(prevnode); } @@ -1802,6 +1801,8 @@ void ModelExecution::collectActions() { if (act->is_read()) { if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { + // Save the original action type + act->set_original_type(act->get_type()); //Weaken a RMW from a freed store to a write act->set_type(ATOMIC_WRITE); } else { @@ -1809,8 +1810,13 @@ void ModelExecution::collectActions() { if (islastact) { fixupLastAct(act); } - delete act; - continue; + + // Only delete this action if not being using by ModelHistory. + // Otherwise, the deletion of action is deferred. + if (act->get_func_ref_count() == 0) { + delete act; + continue; + } } } } @@ -1841,14 +1847,18 @@ void ModelExecution::collectActions() { if (act->is_read()) { if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { + // Save the original action type + act->set_original_type(act->get_type()); act->set_type(ATOMIC_WRITE); } else { removeAction(act); if (islastact) { fixupLastAct(act); } - delete act; - continue; + if (act->get_func_ref_count() == 0) { + delete act; + continue; + } } } } else if (act->is_free()) { @@ -1856,8 +1866,10 @@ void ModelExecution::collectActions() { if (islastact) { fixupLastAct(act); } - delete act; - continue; + if (act->get_func_ref_count() == 0) { + delete act; + continue; + } } else if (act->is_write()) { //Do nothing with write that hasn't been marked to be freed } else if (islastact) { @@ -1880,6 +1892,11 @@ void ModelExecution::collectActions() { modelclock_t tid_clock = cvmin->getClock(act_tid); if (actseq <= tid_clock) { removeAction(act); + // Remove reference to act from thrd_last_fence_release + int thread_id = id_to_int( act->get_tid() ); + if (thrd_last_fence_release[thread_id] == act) { + thrd_last_fence_release[thread_id] = NULL; + } delete act; continue; } @@ -1905,18 +1922,17 @@ void ModelExecution::collectActions() { delete act; continue; } + } - //If we don't delete the action, we should remove references to release fences - 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); - } - + //If we don't delete the action, we should remove references to release fences + 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); } }