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);
* 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<ModelAction *> * rf_set)
{
}
// Remove writes that violate read modification order
- uint i = 0;
- while (i < rf_set->size()) {
- ModelAction * rf = (*rf_set)[i];
- if (!r_modification_order(curr, rf, NULL, NULL, true)) {
- (*rf_set)[i] = rf_set->back();
- rf_set->pop_back();
- } else
- i++;
- }
+ /*
+ uint i = 0;
+ while (i < rf_set->size()) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
+ } else
+ i++;
+ }*/
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
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);
}
-
- ASSERT(false);
- /* TODO: Following code not needed anymore */
priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
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);
SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
- unsigned int i;
ASSERT(curr->is_read());
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
int tid = curr->get_tid();
+
+ /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet. */
+ if ((int)thrd_lists->size() <= tid) {
+ uint oldsize = thrd_lists->size();
+ thrd_lists->resize(priv->next_thread_id);
+ for(uint i = oldsize;i < priv->next_thread_id;i++)
+ new (&(*thrd_lists)[i]) action_list_t();
+ }
+
ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
+ for (unsigned int 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 (i != 0)
*
* @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()) {
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)
}
act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
+ ModelAction * lastact = thrd_last_action[tid];
// Update thrd_last_action, the last action taken by each thrad
- if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+ if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
thrd_last_action[tid] = act;
}
SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++) {
- /* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- sllnode<ModelAction *> * rit;
- for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
- ModelAction *act = rit->getVal();
-
- if (act == curr)
- continue;
+ if (thrd_lists != NULL)
+ for (i = 0;i < thrd_lists->size();i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ sllnode<ModelAction *> * rit;
+ for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+ ModelAction *act = rit->getVal();
+
+ if (act == curr)
+ continue;
- /* Don't consider more than one seq_cst write if we are a seq_cst read. */
- bool allow_read = true;
-
- if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
- allow_read = false;
-
- /* Need to check whether we will have two RMW reading from the same value */
- if (curr->is_rmwr()) {
- /* It is okay if we have a failing CAS */
- if (!curr->is_rmwrcas() ||
- valequals(curr->get_value(), act->get_value(), curr->getSize())) {
- //Need to make sure we aren't the second RMW
- CycleNode * node = mo_graph->getNode_noCreate(act);
- if (node != NULL && node->getRMW() != NULL) {
- //we are the second RMW
- allow_read = false;
+ /* Don't consider more than one seq_cst write if we are a seq_cst read. */
+ bool allow_read = true;
+
+ if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+ allow_read = false;
+
+ /* Need to check whether we will have two RMW reading from the same value */
+ if (curr->is_rmwr()) {
+ /* It is okay if we have a failing CAS */
+ if (!curr->is_rmwrcas() ||
+ valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+ //Need to make sure we aren't the second RMW
+ CycleNode * node = mo_graph->getNode_noCreate(act);
+ if (node != NULL && node->getRMW() != NULL) {
+ //we are the second RMW
+ allow_read = false;
+ }
}
}
- }
- if (allow_read) {
- /* Only add feasible reads */
- rf_set->push_back(act);
- }
+ if (allow_read) {
+ /* Only add feasible reads */
+ rf_set->push_back(act);
+ }
- /* Include at most one act per-thread that "happens before" curr */
- if (act->happens_before(curr))
- break;
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr))
+ break;
+ }
}
- }
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
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<ModelAction *> * listref = act->getActionRef();
if (listref != NULL) {
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
ClockVector * ModelExecution::computeMinimalCV() {
ClockVector *cvmin = NULL;
- for(unsigned int i = 0;i < thread_map.size();i++) {
+ //Thread 0 isn't a real thread, so skip it..
+ for(unsigned int i = 1;i < thread_map.size();i++) {
Thread * t = thread_map[i];
if (t->get_state() == THREAD_COMPLETED)
continue;
void ModelExecution::collectActions() {
//Compute minimal clock vector for all live threads
ClockVector *cvmin = computeMinimalCV();
+ cvmin->print();
SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
//Mark everything earlier in MO graph to be freed
CycleNode * cn = mo_graph->getNode_noCreate(write);
- queue->push_back(cn);
- while(!queue->empty()) {
- CycleNode * node = queue->back();
- queue->pop_back();
- for(unsigned int i=0;i<node->getNumInEdges();i++) {
- CycleNode * prevnode = node->getInEdge(i);
- ModelAction * prevact = prevnode->getAction();
- if (prevact->get_type() != READY_FREE) {
- prevact->set_free();
- queue->push_back(prevnode);
+ if (cn != NULL) {
+ queue->push_back(cn);
+ while(!queue->empty()) {
+ CycleNode * node = queue->back();
+ queue->pop_back();
+ for(unsigned int i=0;i<node->getNumInEdges();i++) {
+ CycleNode * prevnode = node->getInEdge(i);
+ ModelAction * prevact = prevnode->getAction();
+ if (prevact->get_type() != READY_FREE) {
+ prevact->set_free();
+ queue->push_back(prevnode);
+ }
}
}
}
}
}
- for (;it != NULL;it=it->getPrev()) {
+ for (;it != NULL;) {
ModelAction *act = it->getVal();
- if (act->is_free()) {
- removeAction(act);
- delete act;
- } else if (act->is_read()) {
- if (act->get_reads_from()->is_free()) {
+ //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 (islastact) {
+ act->set_read_from(NULL);
+ continue;
+ } else if (act->get_reads_from()->is_free()) {
removeAction(act);
delete act;
} else {
act->set_last_fence_release(NULL);
}
}
+ } else if (islastact) {
+ continue;
+ } else if (act->is_free()) {
+ removeAction(act);
+ delete act;
+ } else if (act->is_write()) {
+ //Do nothing with write that hasn't been marked to be freed
} else if (act->is_fence()) {
//Note that acquire fences can always be safely
//removed, but could incur extra overheads in
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;
projects / c11tester.git / blobdiff