Merge branch 'branch-weiyu' of /home/git/random-fuzzer into new_fuzzer

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 01125bb2b0910b7e64fa3933afed1f1693e01c2a..de2cace8cecbe61116e74c13837d3dcaedac8c8c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -460,8 +460,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;
                }
        }
@@ -851,7 +851,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;
                                        }
                                }
@@ -909,13 +909,17 @@ 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);
                }
+               //update map for next query
+               obj_last_sc_map.put(curr->get_location(), curr);
        }
 
        /* Last SC fence in the current thread */
@@ -931,7 +935,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) {
@@ -946,7 +949,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;
@@ -959,7 +961,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;
                        }
 
@@ -975,15 +977,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->get_reads_from());
                                }
                                break;
                        }
                }
        }
+       mo_graph->addEdges(&edgeset, curr);
+
 }
 
 /**
@@ -1204,10 +1208,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
 
 void ModelExecution::add_write_to_lists(ModelAction *write) {
-       // Update seq_cst map
-       if (write->is_seqcst())
-               obj_last_sc_map.put(write->get_location(), write);
-
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
        int tid = id_to_int(write->get_tid());
        if (tid >= (int)vec->size())