- // No write satisfies the selected predicate, so pause this thread.
- while ( rf_set->size() == 0 ) {
- Thread * read_thread = execution->get_thread(tid);
- //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());
-
- if (find_threads(read)) {
- // reset thread pending action and revert sequence numbers
- read_thread->set_pending(read);
- read->reset_seq_number();
- execution->restore_last_seq_num();
-
- conditional_sleep(read_thread);
- // Returning -1 stops the while loop of ModelExecution::process_read
- return -1;
- } else {
- Predicate * selected_branch = get_selected_child_branch(tid);
- selected_branch->incr_fail_count();
- failed_predicates.put(selected_branch, true);
-
- 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] );
+ ASSERT(rf_set->size() != 0);
+ int random_index = random() % rf_set->size();
+
+ return random_index;
+}
+
+/* For children of curr_pred that matches read_inst.
+ * If any store in rf_set satisfies the a child's predicate,
+ * increment the store visibility count for it.
+ *
+ * @return False if no child matches read_inst
+ */
+bool NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_inst,
+inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
+{
+ available_branches_tmp_storage.clear();
+
+ ASSERT(!rf_set->empty());
+ if (curr_pred == NULL || read_inst == NULL)
+ return false;
+
+ ModelVector<Predicate *> * children = curr_pred->get_children();
+ bool any_child_match = false;
+
+ /* Iterate over all predicate children */
+ for (uint i = 0;i < children->size();i++) {
+ Predicate * branch = (*children)[i];
+
+ /* 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;
+
+ /* Do not check unset predicates */
+ if (pred_expressions->isEmpty()) {
+ available_branches_tmp_storage.push_back(branch);
+ continue;