model(m),
params(NULL),
scheduler(scheduler),
- action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
pthread_map(0),
pthread_counter(1),
+ action_trace(),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
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);
return ++priv->used_sequence_numbers;
}
+/** @return a sequence number for a new ModelAction */
+modelclock_t ModelExecution::get_curr_seq_num()
+{
+ return priv->used_sequence_numbers;
+}
+
/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
void ModelExecution::restore_last_seq_num()
{
* 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)
{
- SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
+ SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
if (hasnonatomicstore) {
ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
}
// 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();
- }
- 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();
break;
}
case ATOMIC_WAIT: {
- /* wake up the other threads */
- for (unsigned int i = 0;i < get_num_threads();i++) {
- Thread *t = get_thread(int_to_id(i));
- Thread *curr_thrd = get_thread(curr);
- if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
- scheduler->wake(t);
- }
+ //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
+ if (fuzzer->shouldWait(curr)) {
+ /* wake up the other threads */
+ for (unsigned int i = 0;i < get_num_threads();i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
+ }
- /* unlock the lock - after checking who was waiting on it */
- state->locked = NULL;
+ /* unlock the lock - after checking who was waiting on it */
+ state->locked = NULL;
- if (fuzzer->shouldWait(curr)) {
/* disable this thread */
get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
scheduler->sleep(get_thread(curr));
}
case ATOMIC_TIMEDWAIT:
case ATOMIC_UNLOCK: {
- //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS MUST EVENMTUALLY RELEASE...
+ //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
+ //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
+ //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
+ //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
+ //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
+ //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
+ //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
+ //MUST EVENMTUALLY RELEASE...
/* wake up the other threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
wake_up_sleeping_actions(curr);
- /* Add uninitialized actions to lists */
- if (!second_part_of_rmw)
- add_uninit_action_to_lists(curr);
-
SnapVector<ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
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);
*/
bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
- SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
+ 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)
if (!check_only)
priorset->push_back(act);
} else {
- const ModelAction *prevrf = act->get_reads_from();
+ ModelAction *prevrf = act->get_reads_from();
if (!prevrf->equals(rf)) {
if (mo_graph->checkReachable(rf, prevrf))
return false;
return vec;
}
-/**
- * Performs various bookkeeping operations for the current ModelAction when it is
- * the first atomic action occurred at its memory location.
- *
- * For instance, adds uninitialized action to the per-object, per-thread action vector
- * and to the action trace list of all thread actions.
- *
- * @param act is the ModelAction to process.
- */
-void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
-{
- int tid = id_to_int(act->get_tid());
- ModelAction *uninit = NULL;
- int uninit_id = -1;
- SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
- if (objvec->empty() && act->is_atomic_var()) {
- uninit = get_uninitialized_action(act);
- uninit_id = id_to_int(uninit->get_tid());
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
- if ((int)vec->size() <= uninit_id) {
- int oldsize = (int) vec->size();
- vec->resize(uninit_id + 1);
- for(int i = oldsize;i < uninit_id + 1;i++) {
- new (&(*vec)[i]) action_list_t();
- }
- }
- (*vec)[uninit_id].push_front(uninit);
- }
-
- // Update action trace, a total order of all actions
- if (uninit)
- action_trace.push_front(uninit);
-
- // Update obj_thrd_map, a per location, per thread, order of actions
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
- 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();
- }
- if (uninit)
- (*vec)[uninit_id].push_front(uninit);
-
- // Update thrd_last_action, the last action taken by each thrad
- if ((int)thrd_last_action.size() <= tid)
- thrd_last_action.resize(get_num_threads());
- if (uninit)
- thrd_last_action[uninit_id] = uninit;
-}
-
-
/**
* Performs various bookkeeping operations for the current ModelAction. For
* instance, adds action to the per-object, per-thread action vector and to the
*
* @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()) {
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->push_back(act);
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ act->setActionRef(list->add_back(act));
}
// Update action trace, a total order of all actions
- action_trace.push_back(act);
+ act->setTraceRef(action_trace.add_back(act));
+
// Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(act);
+ if (!canprune)
+ act->setThrdMapRef((*vec)[tid].add_back(act));
- // Update thrd_last_action, the last action taken by each thrad
+ // Update thrd_last_action, the last action taken by each thread
if ((int)thrd_last_action.size() <= tid)
thrd_last_action.resize(get_num_threads());
thrd_last_action[tid] = act;
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
+ 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) {
for(uint i = oldsize;i < priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(act);
+ act->setThrdMapRef((*vec)[tid].add_back(act));
}
}
-void insertIntoActionList(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
sllnode<ModelAction*> * rit = list->end();
modelclock_t next_seq = act->get_seq_number();
if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
- list->push_back(act);
+ return list->add_back(act);
else {
for(;rit != NULL;rit=rit->getPrev()) {
if (rit->getVal()->get_seq_number() == next_seq) {
- list->insertAfter(rit, act);
- break;
+ return list->insertAfter(rit, act);
}
}
+ return NULL;
}
}
-void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
sllnode<ModelAction*> * rit = list->end();
modelclock_t next_seq = act->get_seq_number();
if (rit == NULL) {
act->create_cv(NULL);
+ return NULL;
} else if (rit->getVal()->get_seq_number() == next_seq) {
act->create_cv(rit->getVal());
- list->push_back(act);
+ return list->add_back(act);
} else {
for(;rit != NULL;rit=rit->getPrev()) {
if (rit->getVal()->get_seq_number() == next_seq) {
act->create_cv(rit->getVal());
- list->insertAfter(rit, act);
- break;
+ return list->insertAfter(rit, act);
}
}
+ return NULL;
}
}
void ModelExecution::add_normal_write_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- insertIntoActionListAndSetCV(&action_trace, act);
+ act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
// Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- insertIntoActionList(&(*vec)[tid],act);
+ 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;
}
for(uint i=oldsize;i<priv->next_thread_id;i++)
new (&(*vec)[i]) action_list_t();
}
- (*vec)[tid].push_back(write);
+ write->setActionRef((*vec)[tid].add_back(write));
}
/**
void *location = curr->get_location();
action_list_t *list = obj_map.get(location);
+ if (list == NULL)
+ return NULL;
+
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
sllnode<ModelAction*>* rit;
for (rit = list->end();rit != NULL;rit=rit->getPrev())
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");
return rf_set;
}
-/**
- * @brief Get an action representing an uninitialized atomic
- *
- * This function may create a new one.
- *
- * @param curr The current action, which prompts the creation of an UNINIT action
- * @return A pointer to the UNINIT ModelAction
- */
-ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
-{
- ModelAction *act = curr->get_uninit_action();
- if (!act) {
- act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
- curr->set_uninit_action(act);
- }
- act->create_cv(NULL);
- return act;
-}
-
static void print_list(action_list_t *list)
{
sllnode<ModelAction*> *it;
return action_select_next_thread(curr);
}
+void ModelExecution::removeAction(ModelAction *act) {
+ {
+ sllnode<ModelAction *> * listref = act->getTraceRef();
+ if (listref != NULL) {
+ action_trace.erase(listref);
+ }
+ }
+ {
+ sllnode<ModelAction *> * listref = act->getThrdMapRef();
+ if (listref != NULL) {
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].erase(listref);
+ }
+ }
+ if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->erase(listref);
+ }
+ } else if (act->is_wait()) {
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ void *mutex_loc = (void *) act->get_value();
+ get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
+ }
+ } 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());
+ (*vec)[act->get_tid()].erase(listref);
+ }
+ //Remove from Cyclegraph
+ mo_graph->freeAction(act);
+ }
+}
+
+ClockVector * ModelExecution::computeMinimalCV() {
+ ClockVector *cvmin = NULL;
+ //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;
+ thread_id_t tid = int_to_id(i);
+ ClockVector * cv = get_cv(tid);
+ if (cvmin == NULL)
+ cvmin = new ClockVector(cv, NULL);
+ else
+ cvmin->minmerge(cv);
+ }
+ return cvmin;
+}
+
+//Options...
+//How often to check for memory
+//How much of the trace to always keep
+//Whether to sacrifice completeness...i.e., remove visible writes
+
+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;
+
+ //Next walk action trace... When we hit an action, see if it is
+ //invisible (e.g., earlier than the first before the minimum
+ //clock for the thread... if so erase it and all previous
+ //actions in cyclegraph
+ sllnode<ModelAction*> * it;
+ for (it = action_trace.begin();it != NULL;it=it->getNext()) {
+ ModelAction *act = it->getVal();
+ modelclock_t actseq = act->get_seq_number();
+
+ //See if we are done
+ if (actseq > maxtofree)
+ break;
+
+ thread_id_t act_tid = act->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(act_tid);
+ if (actseq <= tid_clock || params->removevisible) {
+ ModelAction * write;
+ if (act->is_write()) {
+ write = act;
+ } else if (act->is_read()) {
+ write = act->get_reads_from();
+ } else
+ continue;
+
+ //Mark everything earlier in MO graph to be freed
+ CycleNode * cn = mo_graph->getNode_noCreate(write);
+ 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;) {
+ 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 (islastact) {
+ act->set_read_from(NULL);
+ continue;
+ } else if (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);
+ }
+ }
+ } 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
+ //traversals. Removing them before the cvmin seems
+ //like a good compromise.
+
+ //Release fences before the cvmin don't do anything
+ //because everyone has already synchronized.
+
+ //Sequentially fences before cvmin are redundant
+ //because happens-before will enforce same
+ //orderings.
+
+ modelclock_t actseq = act->get_seq_number();
+ thread_id_t act_tid = act->get_tid();
+ modelclock_t tid_clock = cvmin->getClock(act_tid);
+ if (actseq <= tid_clock) {
+ removeAction(act);
+ delete act;
+ }
+ } else {
+ //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish
+ //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
+ //need to keep most recent unlock/wait for each lock
+ if(act->is_unlock() || act->is_wait()) {
+ ModelAction * lastlock = get_last_unlock(act);
+ if (lastlock != act) {
+ 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;
+ }
+ }
+ }
+
+ delete cvmin;
+ delete queue;
+}
+
+
+
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
projects / c11tester.git / blobdiff