Merge branch 'norris'

Primary change: push 'add_action_to_lists()' before main work in
'check_current_action()'

diff --combined model.cc
index 38c5d4a9396f82bde9b8341fac00f8b2d8dc63a6,483e83232ffb2ec7272e1eae1c7283af3b4eac84..9faf4e2a28eb26b7c7891114f86592aee80480b9
--- 1/model.cc
--- 2/model.cc
+++ b/model.cc
@@@ -281,7 -281,7 +281,7 @@@ bool ModelChecker::process_read(ModelAc
                        bool r_status = false;
  
                        if (!second_part_of_rmw) {
-                               check_recency(curr,false);
+                               check_recency(curr);
                                r_status = r_modification_order(curr, reads_from);
                        }
  
@@@ -420,6 -420,10 +420,10 @@@ Thread * ModelChecker::check_current_ac
                break;
        }
  
+       /* Add current action to lists before work_queue loop */
+       if (!second_part_of_rmw)
+               add_action_to_lists(curr);
+ 
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
  
        while (!work_queue.empty()) {
@@@ -451,10 -455,6 +455,6 @@@
                }
        }
  
-       /* Add action to list.  */
-       if (!second_part_of_rmw)
-               add_action_to_lists(curr);
- 
        check_curr_backtracking(curr);
  
        set_backtracking(curr);
@@@ -500,24 -500,11 +500,24 @@@ bool ModelChecker::isfeasible() 
  /** @returns whether the current partial trace is feasible other than
   * multiple RMW reading from the same store. */
  bool ModelChecker::isfeasibleotherthanRMW() {
 +      if (DBG_ENABLED()) {
 +              if (mo_graph->checkForCycles())
 +                      DEBUG("Infeasible: modification order cycles\n");
 +              if (failed_promise)
 +                      DEBUG("Infeasible: failed promise\n");
 +              if (too_many_reads)
 +                      DEBUG("Infeasible: too many reads\n");
 +              if (promises_expired())
 +                      DEBUG("Infeasible: promises expired\n");
 +      }
        return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
  }
  
  /** Returns whether the current completed trace is feasible. */
  bool ModelChecker::isfinalfeasible() {
 +      if (DBG_ENABLED() && promises->size() != 0)
 +              DEBUG("Infeasible: unrevolved promises\n");
 +
        return isfeasible() && promises->size() == 0;
  }
  
@@@ -544,7 -531,7 +544,7 @@@ ModelAction * ModelChecker::process_rmw
   *
   * If so, we decide that the execution is no longer feasible.
   */
- void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+ void ModelChecker::check_recency(ModelAction *curr) {
        if (params.maxreads != 0) {
                if (curr->get_node()->get_read_from_size() <= 1)
                        return;
@@@ -565,12 -552,10 +565,10 @@@
  
                action_list_t::reverse_iterator rit = list->rbegin();
                /* Skip past curr */
-               if (already_added) {
-                       for (; (*rit) != curr; rit++)
-                               ;
-                       /* go past curr now */
-                       rit++;
-               }
+               for (; (*rit) != curr; rit++)
+                       ;
+               /* go past curr now */
+               rit++;
  
                action_list_t::reverse_iterator ritcopy = rit;
                //See if we have enough reads from the same value
@@@ -661,10 -646,13 +659,13 @@@ bool ModelChecker::r_modification_order
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
  
-                       /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr)) {
+                       /*
+                        * Include at most one act per-thread that "happens
+                        * before" curr. Don't consider reflexively.
+                        */
+                       if (act->happens_before(curr) && act != curr) {
                                if (act->is_write()) {
-                                       if (rf != act && act != curr) {
+                                       if (rf != act) {
                                                mo_graph->addEdge(act, rf);
                                                added = true;
                                        }
@@@ -675,7 -663,6 +676,6 @@@
                                                added = true;
                                        }
                                }
- 
                                break;
                        }
                }
@@@ -768,7 -755,7 +768,7 @@@ bool ModelChecker::w_modification_order
        if (curr->is_seqcst()) {
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
-               ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
+               ModelAction *last_seq_cst = get_last_seq_cst(curr);
                if (last_seq_cst != NULL) {
                        mo_graph->addEdge(last_seq_cst, curr);
                        added = true;
@@@ -782,8 -769,23 +782,23 @@@
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
+                       if (act == curr) {
+                               /*
+                                * If RMW, we already have all relevant edges,
+                                * so just skip to next thread.
+                                * If normal write, we need to look at earlier
+                                * actions, so continue processing list.
+                                */
+                               if (curr->is_rmw())
+                                       break;
+                               else
+                                       continue;
+                       }
  
-                       /* Include at most one act per-thread that "happens before" curr */
+                       /*
+                        * Include at most one act per-thread that "happens
+                        * before" curr
+                        */
                        if (act->happens_before(curr)) {
                                /*
                                 * Note: if act is RMW, just add edge:
@@@ -791,11 -793,9 +806,9 @@@
                                 * The following edge should be handled elsewhere:
                                 *   readfrom(act) --mo--> act
                                 */
-                               if (act->is_write()) {
-                                       //RMW shouldn't have an edge to themselves
-                                       if (act!=curr)
-                                               mo_graph->addEdge(act, curr);
-                               } else if (act->is_read() && act->get_reads_from() != NULL)
+                               if (act->is_write())
+                                       mo_graph->addEdge(act, curr);
+                               else if (act->is_read() && act->get_reads_from() != NULL)
                                        mo_graph->addEdge(act->get_reads_from(), curr);
                                added = true;
                                break;
@@@ -1085,18 -1085,21 +1098,21 @@@ ModelAction * ModelChecker::get_last_ac
  }
  
  /**
-  * Gets the last memory_order_seq_cst action (in the total global sequence)
-  * performed on a particular object (i.e., memory location).
-  * @param location The object location to check
-  * @return The last seq_cst action performed
+  * Gets the last memory_order_seq_cst write (in the total global sequence)
+  * performed on a particular object (i.e., memory location), not including the
+  * current action.
+  * @param curr The current ModelAction; also denotes the object location to
+  * check
+  * @return The last seq_cst write
   */
- ModelAction * ModelChecker::get_last_seq_cst(const void *location)
+ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
  {
+       void *location = curr->get_location();
        action_list_t *list = obj_map->get_safe_ptr(location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if ((*rit)->is_write() && (*rit)->is_seqcst())
+               if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
                        return *rit;
        return NULL;
  }
@@@ -1210,7 -1213,7 +1226,7 @@@ void ModelChecker::build_reads_from_pas
        bool initialized = false;
  
        if (curr->is_seqcst()) {
-               last_seq_cst = get_last_seq_cst(curr->get_location());
+               last_seq_cst = get_last_seq_cst(curr);
                /* We have to at least see the last sequentially consistent write,
                         so we are initialized. */
                if (last_seq_cst != NULL)