From: weiyu <weiyuluo1232@gmail.com>
Date: Fri, 13 Dec 2019 20:51:22 +0000 (-0800)
Subject: Remove the code that checks store visibility, not being used at this time
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=5d3037f7280786b48caa804d92aa360a6dea846d

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

diff --git a/execution.cc b/execution.cc
index 39abc039..addaa7af 100644
--- 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
+	/*
 	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++;
-	}
+	}*/
 
 	while(true) {
 		int index = fuzzer->selectWrite(curr, rf_set);
@@ -319,9 +320,6 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 			}
 			return true;
 		}
-
-		ASSERT(false);
-		/* TODO: Following code not needed anymore */
 		priorset->clear();
 		(*rf_set)[index] = rf_set->back();
 		rf_set->pop_back();
diff --git a/newfuzzer.cc b/newfuzzer.cc
index 29961990..6d90f5fd 100644
--- 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;
 	}
 
-	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;
@@ -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) {
-			PredExprSet * pred_expressions = branch->get_pred_expressions();
 			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;
 	}
 
-	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;
 
+	/* 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
  */
-int NewFuzzer::choose_index(SnapVector<Predicate *> * branches)
+int NewFuzzer::choose_branch_index(SnapVector<Predicate *> * branches)
 {
 	if (branches->size() == 1)
 		return 0;
diff --git a/newfuzzer.h b/newfuzzer.h
index fedd047d..d3fc460e 100644
--- 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);
-	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.
 	 */