From: weiyu <weiyuluo1232@gmail.com>
Date: Thu, 5 Dec 2019 00:33:31 +0000 (-0800)
Subject: Using a for loop to prune writes that violate modification order is wrong
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=25b12680719a51fc81d1681a280e076920dcaabc;hp=a21f6b6439fd0f52ec5ab316bf6cd46992e94301

Using a for loop to prune writes that violate modification order is wrong
---

diff --git a/execution.cc b/execution.cc
index 21207fef..377cd01c 100644
--- a/execution.cc
+++ b/execution.cc
@@ -288,12 +288,14 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 	}
 
 	// Remove writes that violate read modification order
-	for (uint i = 0; i < rf_set->size(); i++) {
+	uint i = 0;
+	while (i < rf_set->size()) {
 		ModelAction * rf = (*rf_set)[i];
 		if (!r_modification_order(curr, rf, NULL, NULL, true)) {
 			(*rf_set)[i] = rf_set->back();
 			rf_set->pop_back();
-		}
+		} else
+			i++;
 	}
 
 	while(true) {
@@ -318,6 +320,9 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 			}
 			return true;
 		}
+
+		ASSERT(false);
+		/* Following code not needed anymore */
 		priorset->clear();
 		(*rf_set)[index] = rf_set->back();
 		rf_set->pop_back();
diff --git a/predicate.cc b/predicate.cc
index 7fec1a4e..77107051 100644
--- a/predicate.cc
+++ b/predicate.cc
@@ -7,6 +7,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) :
 	entry_predicate(is_entry),
 	exit_predicate(is_exit),
 	does_write(false),
+	depth(0),
 	exploration_count(0),
 	store_visible_count(0),
 	total_checking_count(0),
@@ -53,6 +54,12 @@ void Predicate::add_child(Predicate * child)
 	children.push_back(child);
 }
 
+void Predicate::set_parent(Predicate * parent_pred)
+{
+	parent = parent_pred;
+	depth = parent_pred->get_depth() + 1;
+}
+
 void Predicate::copy_predicate_expr(Predicate * other)
 {
 	PredExprSet * other_pred_expressions = other->get_pred_expressions();
@@ -118,7 +125,7 @@ ConcretePredicate * Predicate::evaluate(inst_act_map_t * inst_act_map, thread_id
 
 void Predicate::print_predicate()
 {
-	model_print("\"%p\" [shape=box, label=\"\n", this);
+	model_print("\"%p\" [shape=box, label=\"", this);
 	if (entry_predicate) {
 		model_print("entry node\"];\n");
 		return;
@@ -129,6 +136,8 @@ void Predicate::print_predicate()
 		return;
 	}
 
+	model_print("depth: %d\n", depth);
+
 	func_inst->print();
 
 	if (pred_expressions.getSize() == 0)
diff --git a/predicate.h b/predicate.h
index 11f46249..97e495de 100644
--- a/predicate.h
+++ b/predicate.h
@@ -5,6 +5,8 @@
 #include "predicatetypes.h"
 #include "classlist.h"
 
+#define MAX_DEPTH 0x7fffffff
+
 unsigned int pred_expr_hash (struct pred_expr *);
 bool pred_expr_equal(struct pred_expr *, struct pred_expr *);
 typedef HashSet<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSet;
@@ -20,7 +22,7 @@ public:
 
 	void add_predicate_expr(token_t token, FuncInst * func_inst, bool value);
 	void add_child(Predicate * child);
-	void set_parent(Predicate * parent_pred) { parent = parent_pred; }
+	void set_parent(Predicate * parent_pred);
 	void set_exit(Predicate * exit_pred) { exit = exit_pred; }
 	void add_backedge(Predicate * back_pred) { backedges.add(back_pred); }
 	void copy_predicate_expr(Predicate * other);
@@ -48,6 +50,9 @@ public:
 	void incr_store_visible_count() { store_visible_count++; }
 	void incr_total_checking_count() { total_checking_count++; }
 
+	uint32_t get_depth() { return depth; }
+	void set_depth(uint32_t depth_) { depth = depth_; }
+
 	void print_predicate();
 	void print_pred_subtree();
 
@@ -58,6 +63,9 @@ private:
 	bool exit_predicate;
 	bool does_write;
 
+	/* Height of this predicate node in the predicate tree */
+	uint32_t depth;
+
 	uint32_t exploration_count;
 	uint32_t store_visible_count;
 	uint32_t total_checking_count;	/* The number of times the store visibility is checked */