Merge branch 'new_fuzzer' of ssh://plrg.eecs.uci.edu:/home/git/random-fuzzer into...
authorbdemsky <bdemsky@uci.edu>
Fri, 21 Jun 2019 15:37:40 +0000 (08:37 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 21 Jun 2019 15:37:40 +0000 (08:37 -0700)
execution.cc
execution.h
snapshot.cc

index b500567..c32b628 100644 (file)
@@ -270,14 +270,18 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelActio
 
 
                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();
@@ -764,7 +768,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @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;
@@ -779,7 +783,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
        int tid = curr->get_tid();
        ModelAction *prev_same_thread = NULL;
        /* Iterate over all threads */
-       for (i = 0;i < thrd_lists->size();i++, tid = ((tid+1) == thrd_lists->size()) ? 0: tid + 1) {
+       for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0: tid + 1) {
                /* Last SC fence in thread tid */
                ModelAction *last_sc_fence_thread_local = NULL;
                if (i != 0)
@@ -862,6 +866,11 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                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;
index 990a7a8..20bbfdc 100644 (file)
@@ -143,7 +143,7 @@ private:
        SnapVector<const ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
 
-       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset);
+       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune);
        void w_modification_order(ModelAction *curr);
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
index b4944f4..d736138 100644 (file)
@@ -249,7 +249,7 @@ static void mprot_roll_back(snapshot_id theID)
 
 #else  /* !USE_MPROTECT_SNAPSHOT */
 
-#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20))       // 100mb for the shared memory
+#define SHARED_MEMORY_DEFAULT  (200 * ((size_t)1 << 20))       // 100mb for the shared memory
 #define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)       // 20 mb out of the above 100 mb for my stack
 
 struct fork_snapshotter {