*/
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());
*/
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;
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;
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;
+ for(unsigned int i = 0;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;
+}
+
+void ModelExecution::collectActions() {
+ //Compute minimal clock vector for all live threads
+ ClockVector *cvmin = computeMinimalCV();
+ SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
+ //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
+ for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
+ ModelAction *act = it->getVal();
+ 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) {
+ 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
+ queue->push_back(mo_graph->getNode_noCreate(write));
+ 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 (sllnode<ModelAction*>* it = action_trace.end();it != NULL;it=it->getPrev()) {
+ ModelAction *act = it->getVal();
+ if (act->is_free()) {
+ removeAction(act);
+ delete act;
+ } else if (act->is_read()) {
+ 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 (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
+ }
}
+ delete cvmin;
+ delete queue;
}
+
+
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
projects / c11tester.git / blobdiff