Merge branch 'new_fuzzer' of /home/git/random-fuzzer into new_fuzzer

diff --combined execution.cc
index f17ed53ca76fa83d504ba711e79ed576505a6b42,b500567c459081dba3b7acd54b3c9d55a696c12f..52af5212534d397566b1d7ac2ac90925492ce192
--- 1/execution.cc
--- 2/execution.cc
+++ b/execution.cc
@@@ -270,18 -270,14 +270,18 @@@ void ModelExecution::process_read(Model
  
  
                ASSERT(rf);
 -
 -              if (r_modification_order(curr, rf, priorset)) {
 +              bool canprune = false;
 +              if (r_modification_order(curr, rf, priorset, &canprune)) {
                        for(unsigned int i=0;i<priorset->size();i++) {
                                mo_graph->addEdge((*priorset)[i], rf);
                        }
                        read_from(curr, rf);
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
 +                      if (canprune && curr->get_type() == ATOMIC_READ) {
 +                        int tid = id_to_int(curr->get_tid());
 +                        (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
 +                      }
                        return;
                }
                priorset->clear();
@@@ -768,7 -764,7 +768,7 @@@ ModelAction * ModelExecution::process_r
   * @return True if modification order edges were added; false otherwise
   */
  
 -bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
 +bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
  {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@@ -780,20 -776,29 +780,29 @@@
        if (curr->is_seqcst())
                last_sc_write = get_last_seq_cst_write(curr);
  
+       int tid = curr->get_tid();
+       ModelAction *prev_same_thread = NULL;
        /* Iterate over all threads */
-       for (i = 0;i < thrd_lists->size();i++) {
-               /* Last SC fence in thread i */
+       for (i = 0;i < thrd_lists->size();i++, tid = ((tid+1) == thrd_lists->size()) ? 0: tid + 1) {
+               /* Last SC fence in thread tid */
                ModelAction *last_sc_fence_thread_local = NULL;
-               if (int_to_id((int)i) != curr->get_tid())
-                       last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+               if (i != 0)
+                       last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
  
-               /* Last SC fence in thread i, before last SC fence in current thread */
+               /* Last SC fence in thread tid, before last SC fence in current thread */
                ModelAction *last_sc_fence_thread_before = NULL;
                if (last_sc_fence_local)
-                       last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+                       last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
  
+               //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
+               if (prev_same_thread != NULL &&
+                   (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+                   (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+                     continue;
+               }
+               
                /* Iterate over actions in thread, starting from most recent */
-               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t *list = &(*thrd_lists)[tid];
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin();rit != list->rend();rit++) {
                        ModelAction *act = *rit;
@@@ -841,6 -846,12 +850,12 @@@
                         * before" curr
                         */
                        if (act->happens_before(curr)) {
+                         if (i==0) {
+                           if (last_sc_fence_local == NULL ||
+                               (*last_sc_fence_local < *prev_same_thread)) {
+                             prev_same_thread = act;
+                           }
+                         }
                                if (act->is_write()) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
@@@ -851,11 -862,6 +866,11 @@@
                                                if (mo_graph->checkReachable(rf, prevrf))
                                                        return false;
                                                priorset->push_back(prevrf);
 +                                      } else {
 +                                              if (act->get_tid() == curr->get_tid()) {
 +                                                      //Can prune curr from obj list
 +                                                      *canprune = true;
 +                                              }
                                        }
                                }
                                break;