more bugs
[c11tester.git] / execution.cc
index 54e14c30fd03cb924ccc300cb3bfd84388c6a550..05591751b14a8db61ba0a7e3ff6619c311260e1d 100644 (file)
@@ -1168,15 +1168,15 @@ 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);
                        }
                }
-               return NULL;
+               return list->add_front(act);
        }
 }
 
@@ -1185,18 +1185,18 @@ sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelA
        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) {
+               return list->add_back(act);
+       } 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);
                        }
                }
-               return NULL;
+               return list->add_front(act);
        }
 }
 
@@ -1660,6 +1660,8 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        return action_select_next_thread(curr);
 }
 
+/** This method removes references to an Action before we delete it. */
+
 void ModelExecution::removeAction(ModelAction *act) {
        {
                sllnode<ModelAction *> * listref = act->getTraceRef();
@@ -1692,11 +1694,18 @@ void ModelExecution::removeAction(ModelAction *act) {
                        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
                        (*vec)[act->get_tid()].erase(listref);
                }
+               //Clear it from last_sc_map
+               if (obj_last_sc_map.get(act->get_location()) == act) {
+                       obj_last_sc_map.remove(act->get_location());
+               }
+
                //Remove from Cyclegraph
                mo_graph->freeAction(act);
        }
 }
 
+/** Computes clock vector that all running threads have already synchronized to.  */
+
 ClockVector * ModelExecution::computeMinimalCV() {
        ClockVector *cvmin = NULL;
        //Thread 0 isn't a real thread, so skip it..
@@ -1714,15 +1723,22 @@ 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
+
+/** 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()));
+       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);
+}
+
+/** Compute which actions to free.  */
 
 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;
 
@@ -1741,6 +1757,8 @@ void ModelExecution::collectActions() {
 
                thread_id_t act_tid = act->get_tid();
                modelclock_t tid_clock = cvmin->getClock(act_tid);
+
+               //Free if it is invisible or we have set a flag to remove visible actions.
                if (actseq <= tid_clock || params->removevisible) {
                        ModelAction * write;
                        if (act->is_write()) {
@@ -1769,6 +1787,48 @@ void ModelExecution::collectActions() {
                        }
                }
        }
+
+       //We may need to remove read actions in the window we don't delete to preserve correctness.
+
+       for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
+               ModelAction *act = it2->getVal();
+               //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 a RMW from a freed store to a write
+                                       act->set_type(ATOMIC_WRITE);
+                               } else {
+                                       removeAction(act);
+                                       if (islastact) {
+                                               fixupLastAct(act);
+                                       }
+                                       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);
+               }
+       }
+       //Now we are in the window of old actions that we remove if possible
        for (;it != NULL;) {
                ModelAction *act = it->getVal();
                //Do iteration early since we may delete node...
@@ -1781,30 +1841,29 @@ void ModelExecution::collectActions() {
                }
 
                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);
+                       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
@@ -1824,9 +1883,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()) {
@@ -1834,16 +1894,31 @@ 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;
+                       }
+
+                       //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);
                        }
+
                }
        }
 
@@ -1851,8 +1926,6 @@ void ModelExecution::collectActions() {
        delete queue;
 }
 
-
-
 Fuzzer * ModelExecution::getFuzzer() {
        return fuzzer;
 }