From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Sep 2012 16:21:08 +0000 (-0700)
Subject: Merge remote-tracking branch 'origin/makefile'
X-Git-Tag: pldi2013~208
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=76205f5d9b62f73ea01f7e55765a043a8333a455;hp=-c;p=model-checker.git

Merge remote-tracking branch 'origin/makefile'
---

76205f5d9b62f73ea01f7e55765a043a8333a455
diff --combined cyclegraph.cc
index 0a3d885,f134822..26235d6
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@@ -55,11 -55,7 +55,11 @@@ void CycleGraph::addEdge(const ModelAct
  	//If the fromnode has a rmwnode that is not the tonode, we
  	//should add an edge between its rmwnode and the tonode
  
 -	if (rmwnode!=NULL&&rmwnode!=tonode) {
 +	//If tonode is also a rmw, don't do this check as the execution is
 +	//doomed and we'll catch the problem elsewhere, but we want to allow
 +	//for the possibility of sending to's write value to rmwnode
 +
 +	if (rmwnode!=NULL&&!to->is_rmw()) {
  		if (!hasCycles) {
  			// Check for Cycles
  			hasCycles=checkReachable(tonode, rmwnode);
@@@ -89,19 -85,17 +89,19 @@@ void CycleGraph::addRMWEdge(const Model
  	}
  
  	/* Transfer all outgoing edges from the from node to the rmw node */
- 	/* This process should not add a cycle because either: 
+ 	/* This process should not add a cycle because either:
  	 * (1) The rmw should not have any incoming edges yet if it is the
  	 * new node or
- 	 * (2) the fromnode is the new node and therefore it should not 
+ 	 * (2) the fromnode is the new node and therefore it should not
  	 * have any outgoing edges.
  	 */
  	std::vector<CycleNode *> * edges=fromnode->getEdges();
  	for(unsigned int i=0;i<edges->size();i++) {
  		CycleNode * tonode=(*edges)[i];
 -		rollbackvector.push_back(rmwnode);
 -		rmwnode->addEdge(tonode);
 +		if (tonode!=rmwnode) {
 +			rollbackvector.push_back(rmwnode);
 +			rmwnode->addEdge(tonode);
 +		}
  	}
  	rollbackvector.push_back(fromnode);
  
diff --combined model.cc
index 50317d0,2a2d776..fb2423f
--- a/model.cc
+++ b/model.cc
@@@ -259,7 -259,6 +259,6 @@@ ModelAction * ModelChecker::get_next_ba
  	return next;
  }
  
- 
  /**
   * Processes a read or rmw model action.
   * @param curr is the read model action to process.
@@@ -267,7 -266,6 +266,6 @@@
   * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
   * @return True if processing this read updates the mo_graph.
   */
- 
  bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
  	uint64_t value;
  	bool updated=false;
@@@ -277,15 -275,14 +275,15 @@@
  			mo_graph->startChanges();
  
  			value = reads_from->get_value();
 +			bool r_status=false;
  
  			if (!second_part_of_rmw) {
  				check_recency(curr,false);
 +				r_status=r_modification_order(curr, reads_from);
  			}
  
 -			bool r_status=r_modification_order(curr,reads_from);
  
 -			if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
 +			if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
  				mo_graph->rollbackChanges();
  				too_many_reads=false;
  				continue;
@@@ -428,7 -425,7 +426,7 @@@ Thread * ModelChecker::check_current_ac
  		add_action_to_lists(curr);
  
  	check_curr_backtracking(curr);
- 	
+ 
  	set_backtracking(curr);
  
  	return get_next_thread(curr);
@@@ -437,7 -434,7 +435,7 @@@
  void ModelChecker::check_curr_backtracking(ModelAction * curr) {
  	Node *currnode = curr->get_node();
  	Node *parnode = currnode->get_parent();
- 	
+ 
  	if ((!parnode->backtrack_empty() ||
  			 !currnode->read_from_empty() ||
  			 !currnode->future_value_empty() ||
@@@ -448,7 -445,6 +446,6 @@@
  	}
  }
  
- 
  bool ModelChecker::promises_expired() {
  	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
  		Promise *promise = (*promises)[promise_index];
@@@ -612,19 -608,16 +609,19 @@@ bool ModelChecker::r_modification_order
  
  			/* Include at most one act per-thread that "happens before" curr */
  			if (act->happens_before(curr)) {
 -				if (act->is_read()) {
 +				if (act->is_write()) {
 +					if (rf != act && act != curr) {
 +						mo_graph->addEdge(act, rf);
 +						added = true;
 +					}
 +				} else {
  					const ModelAction *prevreadfrom = act->get_reads_from();
  					if (prevreadfrom != NULL && rf != prevreadfrom) {
  						mo_graph->addEdge(prevreadfrom, rf);
  						added = true;
  					}
 -				} else if (rf != act) {
 -					mo_graph->addEdge(act, rf);
 -					added = true;
 -				}
 +				} 
 +
  				break;
  			}
  		}
@@@ -762,7 -755,6 +759,6 @@@ bool ModelChecker::thin_air_constraint_
  	return true;
  }
  
- 
  /**
   * Finds the head(s) of the release sequence(s) containing a given ModelAction.
   * The ModelAction under consideration is expected to be taking part in
@@@ -1056,8 -1048,6 +1052,6 @@@ bool ModelChecker::resolve_promises(Mod
  	return resolved;
  }
  
- 
- 
  /**
   * Compute the set of promises that could potentially be satisfied by this
   * action. Note that the set computation actually appears in the Node, not in