fix bugs

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index fb16def8748dac4c4c9d1825268d38004d3ae7a8..cd3ef4b01d93ff7daf1e4b29e0fc6e521f0f716c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -63,13 +63,17 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
+#ifdef NEWFUZZER
+       fuzzer(new NewFuzzer()),
+#else
        fuzzer(new Fuzzer()),
+#endif
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
        add_thread(model_thread);
-       fuzzer->register_engine(this);
+       fuzzer->register_engine(m, this);
        scheduler->register_engine(this);
 #ifdef TLS
        pthread_key_create(&pthreadkey, tlsdestructor);
@@ -275,7 +279,9 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        add_normal_write_to_lists(act);
        add_write_to_lists(act);
        w_modification_order(act);
+#ifdef NEWFUZZER
        model->get_history()->process_action(act, act->get_tid());
+#endif
        return act;
 }
 
@@ -1135,7 +1141,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       if (!canprune)
+       if (!canprune && (act->is_read() || act->is_write()))
                act->setThrdMapRef((*vec)[tid].add_back(act));
 
        // Update thrd_last_action, the last action taken by each thread
@@ -1153,15 +1159,6 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
                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) {
-                       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();
-               }
-               act->setThrdMapRef((*vec)[tid].add_back(act));
        }
 }
 
@@ -1176,7 +1173,7 @@ sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *a
                                return list->insertAfter(rit, act);
                        }
                }
-               return NULL;
+               return list->add_front(act);
        }
 }
 
@@ -1185,7 +1182,7 @@ 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;
+               return list->add_back(act);
        } else if (rit->getVal()->get_seq_number() <= next_seq) {
                act->create_cv(rit->getVal());
                return list->add_back(act);
@@ -1196,7 +1193,7 @@ sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelA
                                return list->insertAfter(rit, act);
                        }
                }
-               return NULL;
+               return list->add_front(act);
        }
 }
 
@@ -1652,14 +1649,17 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        ASSERT(curr);
 
        /* Process this action in ModelHistory for records */
+#ifdef NEWFUZZER
        model->get_history()->process_action( curr, curr->get_tid() );
-
+#endif
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);
 
        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();
@@ -1697,12 +1697,13 @@ void ModelExecution::removeAction(ModelAction *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..
@@ -1720,15 +1721,19 @@ ClockVector * ModelExecution::computeMinimalCV() {
        return cvmin;
 }
 
+
+/** 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) {
-//Create a standin ModelAction
-       ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid()));
+       ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, 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();
@@ -1750,6 +1755,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()) {
@@ -1778,6 +1785,9 @@ 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
@@ -1792,7 +1802,7 @@ void ModelExecution::collectActions() {
                if (act->is_read()) {
                        if (act->get_reads_from()->is_free()) {
                                if (act->is_rmw()) {
-                                       //weaken to write
+                                       //Weaken a RMW from a freed store to a write
                                        act->set_type(ATOMIC_WRITE);
                                } else {
                                        removeAction(act);
@@ -1804,6 +1814,8 @@ void ModelExecution::collectActions() {
                                }
                        }
                }
+               //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();
@@ -1814,6 +1826,7 @@ void ModelExecution::collectActions() {
                                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...
@@ -1892,6 +1905,8 @@ void ModelExecution::collectActions() {
                                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();
@@ -1909,8 +1924,6 @@ void ModelExecution::collectActions() {
        delete queue;
 }
 
-
-
 Fuzzer * ModelExecution::getFuzzer() {
        return fuzzer;
 }