From: bdemsky <bdemsky@uci.edu>
Date: Fri, 21 Jun 2019 15:37:40 +0000 (-0700)
Subject: Merge branch 'new_fuzzer' of ssh://plrg.eecs.uci.edu:/home/git/random-fuzzer into... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=1b2081fd7a99dd894f75b8606073d3eae57a0013;hp=e9f607873c5e57a4a1823772c9b8606007b5a836

Merge branch 'new_fuzzer' of ssh://plrg.eecs.uci.edu:/home/git/random-fuzzer into new_fuzzer
---

diff --git a/execution.cc b/execution.cc
index b500567c..c32b6288 100644
--- a/execution.cc
+++ b/execution.cc
@@ -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;
diff --git a/execution.h b/execution.h
index 990a7a8a..20bbfdc6 100644
--- a/execution.h
+++ b/execution.h
@@ -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;
diff --git a/snapshot.cc b/snapshot.cc
index b4944f45..d7361383 100644
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -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 {