From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 18 Jul 2012 03:36:07 +0000 (-0700)
Subject: Add basic reads from support
X-Git-Tag: pldi2013~343
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=e048b80fa298a5228d71466f4b84c1c64094f2f3

Add basic reads from support

Now we need to use the cyclegraph to eliminate bad executions...
---

diff --git a/model.cc b/model.cc
index a22e17e..e9d1f1d 100644
--- a/model.cc
+++ b/model.cc
@@ -126,13 +126,20 @@ thread_id_t ModelChecker::get_next_replay_thread()
 	next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
-		Node *node = next->get_node()->get_parent();
-
+		Node *nextnode = next->get_node();
 		/* Reached divergence point */
+		if (nextnode->increment_read_from()) {
+			/* The next node will read from a different value */
+			tid = next->get_tid();
+			node_stack->pop_restofstack(2);
+		} else {
+			/* Make a different thread execute for next step */
+			Node *node = nextnode->get_parent();
+			tid = node->get_next_backtrack();
+			node_stack->pop_restofstack(1);
+		}
 		DEBUG("*** Divergence point ***\n");
-		tid = node->get_next_backtrack();
 		diverge = NULL;
-		node_stack->pop_restofstack();
 	} else {
 		tid = next->get_tid();
 	}
@@ -231,8 +238,6 @@ ModelAction * ModelChecker::get_next_backtrack()
 
 void ModelChecker::check_current_action(void)
 {
-	Node *currnode;
-
 	ModelAction *curr = this->current_action;
 	ModelAction *tmp;
 	current_action = NULL;
@@ -265,9 +270,10 @@ void ModelChecker::check_current_action(void)
 
 	nextThread = get_next_replay_thread();
 
-	currnode = curr->get_node()->get_parent();
+	Node *currnode = curr->get_node();
+	Node *parnode = currnode->get_parent();
 
-	if (!currnode->backtrack_empty())
+	if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
 		if (!next_backtrack || *curr > *next_backtrack)
 			next_backtrack = curr;
 
@@ -281,7 +287,7 @@ void ModelChecker::check_current_action(void)
 	Thread *th = get_thread(curr->get_tid());
 	uint64_t value = VALUE_NONE;
 	if (curr->is_read()) {
-		const ModelAction *reads_from = curr->get_node()->get_next_read_from();
+		const ModelAction *reads_from = curr->get_node()->get_read_from();
 		value = reads_from->get_value();
 		/* Assign reads_from, perform release/acquire synchronization */
 		curr->read_from(reads_from);
@@ -361,7 +367,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 {
 	std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
 	unsigned int i;
-
 	ASSERT(curr->is_read());
 
 	ModelAction *last_seq_cst = NULL;
@@ -389,8 +394,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			if (!act->is_write())
 				continue;
 
-			/* Don't consider more than one seq_cst write */
-			if (!act->is_seqcst() || act == last_seq_cst) {
+			/* Don't consider more than one seq_cst write if we are a seq_cst read. */
+			if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
 				DEBUG("Adding action to may_read_from:\n");
 				if (DBG_ENABLED()) {
 					act->print();
diff --git a/nodestack.cc b/nodestack.cc
index 725bc53..5a65821 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -24,7 +24,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
 	explored_children(num_threads),
 	backtrack(num_threads),
 	numBacktracks(0),
-	may_read_from()
+	may_read_from(),
+	read_from_index(0)
 {
 	if (act)
 		act->set_node(this);
@@ -73,7 +74,11 @@ bool Node::has_been_explored(thread_id_t tid)
  */
 bool Node::backtrack_empty()
 {
-	return numBacktracks == 0;
+	return (numBacktracks == 0);
+}
+
+bool Node::readsfrom_empty() {
+	return ((read_from_index+1)>=may_read_from.size());
 }
 
 /**
@@ -138,13 +143,14 @@ void Node::add_read_from(const ModelAction *act)
  * may remove elements from may_read_from
  * @return The first element in may_read_from
  */
-const ModelAction * Node::get_next_read_from() {
-	const ModelAction *act;
-	ASSERT(!may_read_from.empty());
-	act = may_read_from.front();
-	/* TODO: perform reads_from replay properly */
-	/* may_read_from.pop_front(); */
-	return act;
+const ModelAction * Node::get_read_from() {
+	ASSERT(read_from_index<may_read_from.size());
+	return may_read_from[read_from_index];
+}
+
+bool Node::increment_read_from() {
+	read_from_index++;
+	return (read_from_index<may_read_from.size());
 }
 
 void Node::explore(thread_id_t tid)
@@ -215,11 +221,12 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 }
 
 
-void NodeStack::pop_restofstack()
+void NodeStack::pop_restofstack(int numAhead)
 {
 	/* Diverging from previous execution; clear out remainder of list */
 	node_list_t::iterator it = iter;
-	it++;
+	while (numAhead--)
+		it++;
 	clear_node_list(&node_list, it, node_list.end());
 }
 
diff --git a/nodestack.h b/nodestack.h
index ad63d4d..6f7807f 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -13,7 +13,7 @@
 
 class ModelAction;
 
-typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t;
+typedef std::vector< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t;
 
 /**
  * @brief A single node in a NodeStack
@@ -32,6 +32,7 @@ public:
 	bool has_been_explored(thread_id_t tid);
 	/* return true = backtrack set is empty */
 	bool backtrack_empty();
+	bool readsfrom_empty();
 	void explore_child(ModelAction *act);
 	/* return false = thread was already in backtrack */
 	bool set_backtrack(thread_id_t id);
@@ -44,7 +45,8 @@ public:
 	Node * get_parent() const { return parent; }
 
 	void add_read_from(const ModelAction *act);
-	const ModelAction * get_next_read_from();
+	const ModelAction * get_read_from();
+	bool increment_read_from();
 
 	void print();
 	void print_may_read_from();
@@ -63,6 +65,7 @@ private:
 	/** The set of ModelActions that this the action at this Node may read
 	 *  from. Only meaningful if this Node represents a 'read' action. */
 	readfrom_set_t may_read_from;
+	unsigned int read_from_index;
 };
 
 typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
@@ -83,7 +86,7 @@ public:
 	Node * get_head();
 	Node * get_next();
 	void reset_execution();
-	void pop_restofstack();
+	void pop_restofstack(int numAhead);
 	int get_total_nodes() { return total_nodes; }
 
 	void print();