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 ()),
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 */
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
/** 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<CycleNode *> * queue = new SnapVector<CycleNode *>();
//Free if it is invisible or we have set a flag to remove visible actions.
if (actseq <= tid_clock || params->removevisible) {
+ // For read or rmw actions being used by ModelHistory, mark the reads_from as being used.
+ if (act->is_read()) {
+ if (act->is_rmw()) {
+ void * func_act_ref = act->getFuncActRef();
+ if (func_act_ref == WRITE_REFERENCED) {
+ // Only the write part of this rmw is referenced, do nothing
+ } else if (func_act_ref != NULL) {
+ // The read part of rmw is potentially referenced
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(WRITE_REFERENCED);
+ }
+ } else {
+ if (act->getFuncActRef() != NULL) {
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(WRITE_REFERENCED);
+ }
+ }
+ }
+
ModelAction * write;
if (act->is_write()) {
write = act;
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);
}
}
if (act->is_read()) {
+ // For read or rmw actions being used by ModelHistory, mark the reads_from as being used.
+ if (act->is_rmw()) {
+ void * func_act_ref = act->getFuncActRef();
+ if (func_act_ref == WRITE_REFERENCED) {
+ // Only the write part of this rmw is referenced, do nothing
+ } else if (func_act_ref != NULL) {
+ // The read part of rmw is potentially referenced
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(WRITE_REFERENCED);
+ }
+ } else {
+ if (act->getFuncActRef() != NULL) {
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(WRITE_REFERENCED);
+ }
+ }
+
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 {
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->getFuncActRef() == NULL) {
+ delete act;
+ continue;
+ }
}
}
}
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->getFuncActRef() == NULL) {
+ delete act;
+ continue;
+ }
}
}
} else if (act->is_free()) {
if (islastact) {
fixupLastAct(act);
}
- delete act;
- continue;
+ if (act->getFuncActRef() == NULL) {
+ delete act;
+ continue;
+ }
} else if (act->is_write()) {
//Do nothing with write that hasn't been marked to be freed
} else if (islastact) {
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;
}
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);
}
}
projects / c11tester.git / blobdiff