improve complexity

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 323c83d36fe4273ddf0d08508af7653abadf3b91..ac3ecbc00e069abd7a53ebbf8d6d70168bf14c97 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -27,7 +27,6 @@ struct model_snapshot_members {
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
                bugs(),
-               dataraces(),
                bad_synchronization(false),
                asserted(false)
        { }
@@ -35,16 +34,12 @@ struct model_snapshot_members {
        ~model_snapshot_members() {
                for (unsigned int i = 0;i < bugs.size();i++)
                        delete bugs[i];
-               for (unsigned int i = 0;i < dataraces.size(); i++) 
-                       delete dataraces[i];
                bugs.clear();
-               dataraces.clear();
        }
 
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        SnapVector<bug_message *> bugs;
-       SnapVector<bug_message *> dataraces;
        /** @brief Incorrectly-ordered synchronization was made */
        bool bad_synchronization;
        bool asserted;
@@ -190,22 +185,6 @@ bool ModelExecution::assert_bug(const char *msg)
        return false;
 }
 
-/* @brief Put data races in a different list from other bugs. The purpose
- *  is to continue the program untill the number of data races exceeds a 
- *  threshold */
-
-/* TODO: check whether set_assert should be called */
-bool ModelExecution::assert_race(const char *msg)
-{
-       priv->dataraces.push_back(new bug_message(msg));
-
-       if (isfeasibleprefix()) {
-               set_assert();
-               return true;
-       }
-       return false;
-}
-
 /** @return True, if any bugs have been reported for this execution */
 bool ModelExecution::have_bug_reports() const
 {
@@ -213,13 +192,13 @@ bool ModelExecution::have_bug_reports() const
 }
 
 /** @return True, if any fatal bugs have been reported for this execution.
- *  Any bug other than a data race is considered a fatal bug. Data races 
+ *  Any bug other than a data race is considered a fatal bug. Data races
  *  are not considered fatal unless the number of races is exceeds
- *  a threshold (temporarily set as 15). 
+ *  a threshold (temporarily set as 15).
  */
 bool ModelExecution::have_fatal_bug_reports() const
 {
-       return priv->bugs.size() != 0 || priv->dataraces.size() >= 15;
+       return priv->bugs.size() != 0;
 }
 
 SnapVector<bug_message *> * ModelExecution::get_bugs() const
@@ -310,8 +289,8 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
        if (hasnonatomicstore) {
-         ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
-         rf_set->push_back(nonatomicstore);
+               ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
+               rf_set->push_back(nonatomicstore);
        }
 
        while(true) {
@@ -482,8 +461,8 @@ bool ModelExecution::process_fence(ModelAction *curr)
                                continue;
 
                        /* Establish hypothetical release sequences */
-                       ClockVector *cv = get_hb_from_write(act);
-                       if (curr->get_cv()->merge(cv))
+                       ClockVector *cv = get_hb_from_write(act->get_reads_from());
+                       if (cv != NULL && curr->get_cv()->merge(cv))
                                updated = true;
                }
        }
@@ -873,7 +852,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                        if (act->happens_before(curr)) {
                                if (i==0) {
                                        if (last_sc_fence_local == NULL ||
-                                                       (*last_sc_fence_local < *prev_same_thread)) {
+                                                       (*last_sc_fence_local < *act)) {
                                                prev_same_thread = act;
                                        }
                                }
@@ -931,12 +910,14 @@ void ModelExecution::w_modification_order(ModelAction *curr)
        unsigned int i;
        ASSERT(curr->is_write());
 
+       SnapList<ModelAction *> edgeset;
+
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
                ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
-                       mo_graph->addEdge(last_seq_cst, curr);
+                       edgeset.push_back(last_seq_cst);
                }
        }
 
@@ -953,7 +934,6 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
-               bool force_edge = false;
                for (rit = list->rbegin();rit != list->rend();rit++) {
                        ModelAction *act = *rit;
                        if (act == curr) {
@@ -968,7 +948,6 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 * 3) If normal write, we need to look at earlier actions, so
                                 * continue processing list.
                                 */
-                               force_edge = true;
                                if (curr->is_rmw()) {
                                        if (curr->get_reads_from() != NULL)
                                                break;
@@ -981,7 +960,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                        /* C++, Section 29.3 statement 7 */
                        if (last_sc_fence_thread_before && act->is_write() &&
                                        *act < *last_sc_fence_thread_before) {
-                               mo_graph->addEdge(act, curr, force_edge);
+                               edgeset.push_back(act);
                                break;
                        }
 
@@ -997,15 +976,17 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 *   readfrom(act) --mo--> act
                                 */
                                if (act->is_write())
-                                       mo_graph->addEdge(act, curr, force_edge);
+                                       edgeset.push_back(act);
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
+                                       edgeset.push_back(act);
                                }
                                break;
                        }
                }
        }
+       mo_graph->addEdges(&edgeset, curr);
+
 }
 
 /**
@@ -1209,7 +1190,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
        insertIntoActionListAndSetCV(&action_trace, act);
-       
+
        action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
        insertIntoActionList(list, act);