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 ()),
mo_graph(new CycleGraph()),
+#ifdef NEWFUZZER
+ fuzzer(new NewFuzzer()),
+#else
fuzzer(new Fuzzer()),
+#endif
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
add_thread(model_thread);
- fuzzer->register_engine(this);
+ fuzzer->register_engine(m, this);
scheduler->register_engine(this);
#ifdef TLS
pthread_key_create(&pthreadkey, tlsdestructor);
add_normal_write_to_lists(act);
add_write_to_lists(act);
w_modification_order(act);
+#ifdef NEWFUZZER
model->get_history()->process_action(act, act->get_tid());
+#endif
return act;
}
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- if (!canprune)
+ if (!canprune && (act->is_read() || act->is_write()))
act->setThrdMapRef((*vec)[tid].add_back(act));
// Update thrd_last_action, the last action taken by each thread
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
-
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
- if ((int)vec->size() <= tid) {
- uint oldsize = vec->size();
- vec->resize(priv->next_thread_id);
- for(uint i = oldsize;i < priv->next_thread_id;i++)
- new (&(*vec)[i]) action_list_t();
- }
- act->setThrdMapRef((*vec)[tid].add_back(act));
}
}
return list->insertAfter(rit, act);
}
}
- return NULL;
+ return list->add_front(act);
}
}
modelclock_t next_seq = act->get_seq_number();
if (rit == NULL) {
act->create_cv(NULL);
- return 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);
return list->insertAfter(rit, act);
}
}
- return NULL;
+ return list->add_front(act);
}
}
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
ASSERT(curr);
/* Process this action in ModelHistory for records */
+#ifdef NEWFUZZER
model->get_history()->process_action( curr, curr->get_tid() );
-
+#endif
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
/** 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());
/** 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 actions being used by ModelHistory, mark the reads_from as being used.
+ if (act->is_read() && act->getFuncActRef() != NULL) {
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(HAS_REFERENCE);
+ }
+
ModelAction * write;
if (act->is_write()) {
write = act;
CycleNode * prevnode = node->getInEdge(i);
ModelAction * prevact = prevnode->getAction();
if (prevact->get_type() != READY_FREE) {
+ if (prevact->getFuncActRef() != NULL) {
+ // Copy the original type if being used by ModelHistory
+ prevact->set_original_type(prevact->get_type());
+ }
prevact->set_free();
queue->push_back(prevnode);
}
}
if (act->is_read()) {
+ // For read actions being used by ModelHistory, mark the reads_from as being used.
+ if (act->getFuncActRef() != NULL) {
+ ModelAction * reads_from = act->get_reads_from();
+ if (reads_from->getFuncActRef() == NULL)
+ reads_from->setFuncActRef(HAS_REFERENCE);
+ }
+
if (act->get_reads_from()->is_free()) {
if (act->is_rmw()) {
+ if (act->getFuncActRef() != NULL) {
+ // Copy the original type if being used by ModelHistory
+ 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()) {
+ if (act->getFuncActRef() != NULL) {
+ // Copy the original type if being used by ModelHistory
+ 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