Merge remote-tracking branch 'origin/makefile'
authorBrian Norris <banorris@uci.edu>
Thu, 13 Sep 2012 16:21:08 +0000 (09:21 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 13 Sep 2012 16:21:08 +0000 (09:21 -0700)
1  2 
cyclegraph.cc
model.cc

diff --combined cyclegraph.cc
index 0a3d8858e795849f16ab1cae667b2e34bb1367cc,f134822f2d72a8b8bed600a53ef765a4cb8b61f2..26235d651e10ecb5e2178d281048ea6ce5007893
@@@ -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 50317d07daa539d8f6643f16c3892c89aaddf60e,2a2d7760f24512ac11072ac48f646481476f4f0a..fb2423f3dfe12a29090ae647194b8a2adbc5bfc6
+++ 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.
   * @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;
                        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);
  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() ||
        }
  }
  
  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