bug fixes

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index cd277c55daa5ad1471380f6450cd72f51c45977c..63c0ac7f23b255858d96e2c5b7f067411b18fa74 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -63,13 +63,13 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
        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);
        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);
        scheduler->register_engine(this);
 #ifdef TLS
        pthread_key_create(&pthreadkey, tlsdestructor);


@@ -283,7 +283,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
  * 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
  * 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)
 {
  */
 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {


@@ -320,12 +320,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        read_from(curr, rf);
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
                        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();
-                               curr->setThrdMapRef(NULL);
-                       }
-                       return true;
+                       return canprune && (curr->get_type() == ATOMIC_READ);

                }
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
                }
                priorset->clear();
                (*rf_set)[index] = rf_set->back();


@@ -728,15 +723,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        if (newly_explored && curr->is_read())
                rf_set = build_may_read_from(curr);
 
        if (newly_explored && curr->is_read())
                rf_set = build_may_read_from(curr);
 

+       bool canprune = false;
+

        if (curr->is_read() && !second_part_of_rmw) {
        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)
                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);
 
        if (curr->is_write())
                add_write_to_lists(curr);


@@ -1118,7 +1115,7 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
  *
  * @param act is the ModelAction to add.
  */
  *
  * @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()) {
 {
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {


@@ -1138,7 +1135,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }

-       act->setThrdMapRef((*vec)[tid].add_back(act));
+       if (!canprune)
+               act->setThrdMapRef((*vec)[tid].add_back(act));

 
        // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)
 
        // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)


@@ -1688,12 +1686,18 @@ void ModelExecution::removeAction(ModelAction *act) {
                        void *mutex_loc = (void *) act->get_value();
                        get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
                }
                        void *mutex_loc = (void *) act->get_value();
                        get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
                }

-       } else if (act->is_write()) {
+       } 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);
                }
                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);
                }

+               //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);
        }
                //Remove from Cyclegraph
                mo_graph->freeAction(act);
        }


@@ -1716,10 +1720,14 @@ ClockVector * ModelExecution::computeMinimalCV() {
        return cvmin;
 }
 
        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
 
 void ModelExecution::collectActions() {
        //Compute minimal clock vector for all live threads


@@ -1771,13 +1779,47 @@ void ModelExecution::collectActions() {
                        }
                }
        }
                        }
                }
        }

+       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() && act->get_reads_from()->is_free()) {
+                       if (act->is_rmw()) {
+                               act->set_type(ATOMIC_WRITE);
+                       }
+                       removeAction(act);
+                       if (islastact) {
+                               fixupLastAct(act);
+                       }
+                       delete act;
+               }
+       }

        for (;it != NULL;) {
                ModelAction *act = it->getVal();
                //Do iteration early since we may delete node...
                it=it->getPrev();
        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 (act->is_read()) {

-                       if (act->get_reads_from()->is_free()) {
+                       if (act->is_rmw()) {
+                               act->set_type(ATOMIC_WRITE);
+                       } else if (act->get_reads_from()->is_free()) {

                                removeAction(act);
                                removeAction(act);

+                               if (islastact) {
+                                       fixupLastAct(act);
+                               }

                                delete act;
                        } else {
                                const ModelAction *rel_fence =act->get_last_fence_release();
                                delete act;
                        } else {
                                const ModelAction *rel_fence =act->get_last_fence_release();


@@ -1792,9 +1834,14 @@ void ModelExecution::collectActions() {
                        }
                } else if (act->is_free()) {
                        removeAction(act);
                        }
                } else if (act->is_free()) {
                        removeAction(act);

+                       if (islastact) {
+                               fixupLastAct(act);
+                       }

                        delete act;
                } else if (act->is_write()) {
                        //Do nothing with write that hasn't been marked to be freed
                        delete act;
                } 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
                } else if (act->is_fence()) {
                        //Note that acquire fences can always be safely
                        //removed, but could incur extra overheads in


@@ -1816,7 +1863,7 @@ void ModelExecution::collectActions() {
                                delete act;
                        }
                } else {
                                delete act;
                        }
                } 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()) {
                        //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()) {


@@ -1825,6 +1872,11 @@ void ModelExecution::collectActions() {
                                        removeAction(act);
                                        delete 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;
                        } else {
                                removeAction(act);
                                delete act;