Remove the code that checks store visibility, not being used at this time

diff --git a/execution.cc b/execution.cc
index 39abc039377504405fd9e7417684317b53d3450a..addaa7afbfc5dc207284799dc22fee6ba8d35657 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -289,6 +289,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        }
 
        // Remove writes that violate read modification order
        }
 
        // Remove writes that violate read modification order

+       /*

        uint i = 0;
        while (i < rf_set->size()) {
                ModelAction * rf = (*rf_set)[i];
        uint i = 0;
        while (i < rf_set->size()) {
                ModelAction * rf = (*rf_set)[i];


@@ -297,7 +298,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        rf_set->pop_back();
                } else
                        i++;
                        rf_set->pop_back();
                } else
                        i++;

-       }
+       }*/

 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);


@@ -319,9 +320,6 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                        }
                        return true;
                }
                        }
                        return true;
                }

-
-               ASSERT(false);
-               /* TODO: Following code not needed anymore */

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

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 29961990e5b70d8e6e5c78033e24e5ec27dc608d..6d90f5fd62c460e0946c5e0c9c6034aa0636a62f 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -82,7 +82,30 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                thrd_last_func_inst[thread_id] = read_inst;
        }
 
                thrd_last_func_inst[thread_id] = read_inst;
        }
 

-       ASSERT(rf_set->size() != 0);
+       // The chosen branch fails, reselect new branches
+       while ( rf_set->size() == 0 ) {
+               Predicate * selected_branch = get_selected_child_branch(tid);
+               failed_predicates.put(selected_branch, true);
+
+               //model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
+
+               SnapVector<ModelAction *> * pruned_writes = thrd_pruned_writes[thread_id];
+               for (uint i = 0; i < pruned_writes->size(); i++) {
+                       rf_set->push_back( (*pruned_writes)[i] );
+               }
+
+               // Reselect a predicate and prune writes
+               Predicate * curr_pred = selected_branch->get_parent();
+               FuncInst * read_inst = thrd_last_func_inst[thread_id];
+               selected_branch = selectBranch(tid, curr_pred, read_inst);
+
+               FuncNode * func_node = history->get_curr_func_node(tid);
+               inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
+               prune_writes(tid, selected_branch, rf_set, inst_act_map);
+
+               ASSERT(selected_branch);
+       }
+

        int random_index = random() % rf_set->size();
 
        return random_index;
        int random_index = random() % rf_set->size();
 
        return random_index;


@@ -112,32 +135,8 @@ inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
 
                /* The children predicates may have different FuncInsts */
                if (branch->get_func_inst() == read_inst) {
 
                /* The children predicates may have different FuncInsts */
                if (branch->get_func_inst() == read_inst) {

-                       PredExprSet * pred_expressions = branch->get_pred_expressions();

                        any_child_match = true;
                        any_child_match = true;

-
-                       branch->incr_total_checking_count();
-
-                       if (pred_expressions->isEmpty()) {
-                               /* Do not check predicate expression of unset predicates */
-                               available_branches_tmp_storage.push_back(branch);
-                               branch->incr_store_visible_count();
-                               continue;
-                       }
-
-                       /* Iterate over all write actions */
-                       for (uint j = 0;j < rf_set->size();j++) {
-                               ModelAction * write_act = (*rf_set)[j];
-                               uint64_t write_val = write_act->get_write_value();
-                               bool dummy = true;
-                               bool satisfy_predicate = check_predicate_expressions(pred_expressions, inst_act_map, write_val, &dummy);
-
-                               /* If one write value satisfies the predicate, go to check the next predicate */
-                               if (satisfy_predicate) {
-                                       branch->incr_store_visible_count();
-                                       available_branches_tmp_storage.push_back(branch);
-                                       break;
-                               }
-                       }
+                       available_branches_tmp_storage.push_back(branch);

                }
        }
 
                }
        }
 


@@ -164,17 +163,22 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func
                return NULL;
        }
 
                return NULL;
        }
 

-       int index = choose_index(&available_branches_tmp_storage);
+       int index = choose_branch_index(&available_branches_tmp_storage);

        Predicate * random_branch = available_branches_tmp_storage[ index ];
        thrd_selected_child_branch[thread_id] = random_branch;
 
        Predicate * random_branch = available_branches_tmp_storage[ index ];
        thrd_selected_child_branch[thread_id] = random_branch;
 

+       /* Remove the chosen branch from vec in case that this
+        * branch fails and need to choose another one */
+       available_branches_tmp_storage[index] = available_branches_tmp_storage.back();
+       available_branches_tmp_storage.pop_back();
+

        return random_branch;
 }
 
 /**
  * @brief Select a branch from the given predicate branch
  */
        return random_branch;
 }
 
 /**
  * @brief Select a branch from the given predicate branch
  */

-int NewFuzzer::choose_index(SnapVector<Predicate *> * branches)
+int NewFuzzer::choose_branch_index(SnapVector<Predicate *> * branches)

 {
        if (branches->size() == 1)
                return 0;
 {
        if (branches->size() == 1)
                return 0;

diff --git a/newfuzzer.h b/newfuzzer.h
index fedd047d29f4adf766747c0ab2b43f1a7fa9fae2..d3fc460e63eba02a67b2284bd9a67de8ef0db19c 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -52,7 +52,7 @@ private:
        bool check_store_visibility(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set);
        Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
        bool check_store_visibility(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set);
        Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);

-       int choose_index(SnapVector<Predicate *> * branches);
+       int choose_branch_index(SnapVector<Predicate *> * branches);

 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
         */
 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
         */