From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 27 Jul 2012 07:25:19 +0000 (-0700)
Subject: okay...known bugs for my trivial test are out of send future values backwards
X-Git-Tag: pldi2013~305
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e4aa586b4bbb1621ff041ddbf2a7ccefb502056d;p=model-checker.git

okay...known bugs for my trivial test are out of send future values backwards
---

diff --git a/action.cc b/action.cc
index 33dbe75..6a8dc60 100644
--- a/action.cc
+++ b/action.cc
@@ -152,7 +152,8 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const
 
 void ModelAction::create_cv(const ModelAction *parent)
 {
-	ASSERT(cv == NULL);
+	if (cv)
+		delete cv;
 
 	if (parent)
 		cv = new ClockVector(parent->cv, this);
@@ -165,7 +166,7 @@ void ModelAction::create_cv(const ModelAction *parent)
 void ModelAction::read_from(const ModelAction *act)
 {
 	ASSERT(cv);
-	if (act->is_release() && this->is_acquire()) {
+	if (act!=NULL && act->is_release() && this->is_acquire()) {
 		synchronized(act);
 		cv->merge(act->cv);
 	}
diff --git a/model.cc b/model.cc
index d8699b0..159dd70 100644
--- a/model.cc
+++ b/model.cc
@@ -173,7 +173,7 @@ bool ModelChecker::next_execution()
 
 	num_executions++;
 
-	if (isfeasible() || DBG_ENABLED())
+	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
 
 	if ((diverge = model->get_next_backtrack()) == NULL)
@@ -279,6 +279,12 @@ void ModelChecker::check_current_action(void)
 			/* First restore type and order in case of RMW operation */
 			if (curr->is_rmwr())
 				tmp->copy_typeandorder(curr);
+
+			/* If we have diverged, we need to reset the clock vector. */
+			if (diverge==NULL) {
+				tmp->create_cv(get_parent_action(tmp->get_tid()));
+			}
+			
 			delete curr;
 			curr = tmp;
 		} else {
@@ -360,6 +366,11 @@ bool ModelChecker::isfeasible() {
 	return !cyclegraph->checkForCycles() && !failed_promise;
 }
 
+/** Returns whether the current trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+	return isfeasible() && promises->size()==0;
+}
+
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction * act) {
 	int tid = id_to_int(act->get_tid());
@@ -445,7 +456,6 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 						 =>
 						 that read could potentially read from our write.
 					*/
-
 					if (act->get_node()->add_future_value(curr->get_value())&&
 							(!next_backtrack || *act > * next_backtrack))
 						next_backtrack = act;
@@ -525,13 +535,15 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 /** Resolve promises. */
 
 void ModelChecker::resolve_promises(ModelAction *write) {
-	for(unsigned int i=0;i<promises->size();i++) {
-		Promise * promise=(*promises)[i];
+	for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
+		Promise * promise=(*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
 			ModelAction * read=promise->get_action();
 			read->read_from(write);
 			r_modification_order(read, write);
-		}
+			promises->erase(promises->begin()+promise_index);
+		} else
+			promise_index++;
 	}
 }
 
@@ -661,7 +673,7 @@ void ModelChecker::print_summary(void)
 
 	scheduler->print();
 
-	if (!isfeasible())
+	if (!isfinalfeasible())
 		printf("INFEASIBLE EXECUTION!\n");
 	print_list(action_trace);
 	printf("\n");
diff --git a/model.h b/model.h
index 574ed21..73605db 100644
--- a/model.h
+++ b/model.h
@@ -57,6 +57,7 @@ public:
 	ClockVector * get_cv(thread_id_t tid);
 	bool next_execution();
 	bool isfeasible();
+	bool isfinalfeasible();
 	void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
 	MEMALLOC
diff --git a/nodestack.cc b/nodestack.cc
index 6eb71dc..4a6a26d 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -27,7 +27,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
 	may_read_from(),
 	read_from_index(0),
 	future_values(),
-	future_index(0)
+	future_index(-1)
 {
 	if (act)
 		act->set_node(this);
@@ -71,11 +71,11 @@ bool Node::increment_promises() {
 	for (unsigned int i=0;i<promises.size();i++) {
 		if (promises[i]==1) {
 			promises[i]=2;
-			do {
+			while (i>0) {
 				i--;
 				if (promises[i]==2)
 					promises[i]=1;
-			} while(i>0);
+			}
 			return true;
 		}
 	}
@@ -98,6 +98,7 @@ bool Node::add_future_value(uint64_t value) {
 	for(unsigned int i=0;i<future_values.size();i++)
 		if (future_values[i]==value)
 			return false;
+
 	future_values.push_back(value);
 	return true;
 }