Bug fixes
[c11tester.git] / execution.cc
index 40aa6814c84e6bd47d006b47b47eb8e532797cf5..fb16def8748dac4c4c9d1825268d38004d3ae7a8 100644 (file)
@@ -1168,11 +1168,11 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 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))
+       if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
                return list->add_back(act);
        else {
                for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() == next_seq) {
+                       if (rit->getVal()->get_seq_number() <= next_seq) {
                                return list->insertAfter(rit, act);
                        }
                }
@@ -1186,12 +1186,12 @@ sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelA
        if (rit == NULL) {
                act->create_cv(NULL);
                return NULL;
-       } else if (rit->getVal()->get_seq_number() == next_seq) {
+       } else if (rit->getVal()->get_seq_number() <= next_seq) {
                act->create_cv(rit->getVal());
                return list->add_back(act);
        } else {
                for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() == next_seq) {
+                       if (rit->getVal()->get_seq_number() <= next_seq) {
                                act->create_cv(rit->getVal());
                                return list->insertAfter(rit, act);
                        }
@@ -1720,15 +1720,18 @@ ClockVector * ModelExecution::computeMinimalCV() {
        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::fixupLastAct(ModelAction *act) {
+//Create a standin ModelAction
+       ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, 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());
+       add_action_to_lists(newact, false);
+}
 
 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;
 
@@ -1775,10 +1778,40 @@ void ModelExecution::collectActions() {
                        }
                }
        }
-       for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;it2=it2->getPrev()) {
+       for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
                ModelAction *act = it2->getVal();
-               if (act->is_read() && act->get_reads_from()->is_free()) {
-                       act->set_read_from(NULL);
+               //Do iteration early in case we delete the act
+               it2=it2->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 (act->get_reads_from()->is_free()) {
+                               if (act->is_rmw()) {
+                                       //weaken to write
+                                       act->set_type(ATOMIC_WRITE);
+                               } else {
+                                       removeAction(act);
+                                       if (islastact) {
+                                               fixupLastAct(act);
+                                       }
+                                       delete act;
+                                       continue;
+                               }
+                       }
+               }
+               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);
                }
        }
        for (;it != NULL;) {
@@ -1793,31 +1826,29 @@ void ModelExecution::collectActions() {
                }
 
                if (act->is_read()) {
-                       if (!islastact && act->get_reads_from()->is_free()) {
-                               removeAction(act);
-                               delete act;
-                               continue;
-                       }
-                       if (islastact && act->get_reads_from()->is_free()) {
-                               act->set_read_from(NULL);
-                       }
-
-                       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 (act->get_reads_from()->is_free()) {
+                               if (act->is_rmw()) {
+                                       act->set_type(ATOMIC_WRITE);
+                               } else {
+                                       removeAction(act);
+                                       if (islastact) {
+                                               fixupLastAct(act);
+                                       }
+                                       delete act;
+                                       continue;
+                               }
                        }
-               } else if (islastact) {
-                       continue;
                } else if (act->is_free()) {
                        removeAction(act);
+                       if (islastact) {
+                               fixupLastAct(act);
+                       }
                        delete act;
+                       continue;
                } else if (act->is_write()) {
                        //Do nothing with write that hasn't been marked to be freed
+               } else if (islastact) {
+                       //Keep the last action for non-read/write actions
                } else if (act->is_fence()) {
                        //Note that acquire fences can always be safely
                        //removed, but could incur extra overheads in
@@ -1837,9 +1868,10 @@ void ModelExecution::collectActions() {
                        if (actseq <= tid_clock) {
                                removeAction(act);
                                delete act;
+                               continue;
                        }
                } else {
-                       //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish
+                       //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
                        //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()) {
@@ -1847,16 +1879,29 @@ void ModelExecution::collectActions() {
                                if (lastlock != act) {
                                        removeAction(act);
                                        delete act;
+                                       continue;
                                }
                        } else if (act->is_create()) {
                                if (act->get_thread_operand()->is_complete()) {
                                        removeAction(act);
                                        delete act;
+                                       continue;
                                }
                        } else {
                                removeAction(act);
                                delete act;
+                               continue;
+                       }
+                       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);
                        }
+
                }
        }