X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=b08bbcf9f1b76dc574cfa295d74d9241d017bf31;hp=7d38eb43f3f721a99017d2e05d8ce243e9e4efde;hb=f750120c93252f2b677c4b07d003fc71fcdaaa00;hpb=38c72a8748ae74a5bb8b75e713f363a49b48e7af

diff --git a/execution.cc b/execution.cc
index 7d38eb43..b08bbcf9 100644
--- a/execution.cc
+++ b/execution.cc
@@ -14,6 +14,7 @@
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"
+#include "fuzzer.h"
 
 #define INITIAL_THREAD_ID	0
 
@@ -25,10 +26,7 @@ struct model_snapshot_members {
 		/* First thread created will have id INITIAL_THREAD_ID */
 		next_thread_id(INITIAL_THREAD_ID),
 		used_sequence_numbers(0),
-		next_backtrack(NULL),
 		bugs(),
-		too_many_reads(false),
-		no_valid_reads(false),
 		bad_synchronization(false),
 		bad_sc_read(false),
 		asserted(false)
@@ -42,10 +40,7 @@ struct model_snapshot_members {
 
 	unsigned int next_thread_id;
 	modelclock_t used_sequence_numbers;
-	ModelAction *next_backtrack;
 	SnapVector<bug_message *> bugs;
-	bool too_many_reads;
-	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
 	bool bad_synchronization;
 	bool bad_sc_read;
@@ -73,7 +68,8 @@ ModelExecution::ModelExecution(ModelChecker *m,
 	thrd_last_fence_release(),
 	node_stack(node_stack),
 	priv(new struct model_snapshot_members()),
-	mo_graph(new CycleGraph())
+	mo_graph(new CycleGraph()),
+	fuzzer(new Fuzzer())
 {
 	/* Initialize a model-checker thread, for special ModelActions */
 	model_thread = new Thread(get_next_id());
@@ -289,14 +285,13 @@ bool ModelExecution::is_complete_execution() const
  */
 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 {
-	int random_index = random() % rf_set->size();
 	bool updated = false;
 		
-	const ModelAction *rf = (*rf_set)[random_index];
+	const ModelAction *rf = fuzzer->selectWrite(curr, rf_set);
+
 	ASSERT(rf);
 	
 	mo_graph->startChanges();
-	
 	updated = r_modification_order(curr, rf);
 	read_from(curr, rf);
 	mo_graph->commitChanges();
@@ -380,20 +375,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 	}
 	case ATOMIC_NOTIFY_ONE: {
 		action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
-
-		//BCD -- TOFIX FUZZER
-		//THIS SHOULD BE A RANDOM CHOICE
-		//		int wakeupthread = curr->get_node()->get_misc();
-		int wakeupthread = 0;
-		action_list_t::iterator it = waiters->begin();
-
-		// WL
-		if (it == waiters->end())
-			break;
-
-		advance(it, wakeupthread);
-		scheduler->wake(get_thread(*it));
-		waiters->erase(it);
+		Thread * thread = fuzzer->selectNotify(waiters);
+		scheduler->wake(thread);
 		break;
 	}
 
@@ -495,7 +478,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
 		break;
 	}
 	case PTHREAD_CREATE: {
-		(*(pthread_t *)curr->get_location()) = pthread_counter++;	
+	  (*(uint32_t *)curr->get_location()) = pthread_counter++;
 
 		struct pthread_params *params = (struct pthread_params *)curr->get_value();
 		Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
@@ -750,10 +733,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 	char *ptr = buf;
 	if (mo_graph->checkForCycles())
 		ptr += sprintf(ptr, "[mo cycle]");
-	if (priv->too_many_reads)
-		ptr += sprintf(ptr, "[too many reads]");
-	if (priv->no_valid_reads)
-		ptr += sprintf(ptr, "[no valid reads-from]");
 	if (priv->bad_synchronization)
 		ptr += sprintf(ptr, "[bad sw ordering]");
 	if (priv->bad_sc_read)
@@ -771,8 +750,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 bool ModelExecution::is_infeasible() const
 {
 	return mo_graph->checkForCycles() ||
-		priv->no_valid_reads ||
-		priv->too_many_reads ||
 		priv->bad_synchronization ||
 	  priv->bad_sc_read;
 }
@@ -1317,6 +1294,22 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
 	return get_parent_action(tid)->get_cv();
 }
 
+bool valequals(uint64_t val1, uint64_t val2, int size) {
+  switch(size) {
+  case 1:
+    return ((uint8_t)val1) == ((uint8_t)val2);
+  case 2:
+    return ((uint16_t)val1) == ((uint16_t)val2);
+  case 4:
+    return ((uint32_t)val1) == ((uint32_t)val2);
+  case 8:
+    return val1==val2;
+  default:
+    ASSERT(0);
+    return false;
+  }
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from, as well as any previously-observed future values that must still be valid.
@@ -1355,6 +1348,20 @@ ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *c
 			if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
 				allow_read = false;
 
+			/* Need to check whether we will have two RMW reading from the same value */
+			if (curr->is_rmwr()) {
+			  /* It is okay if we have a failing CAS */
+			  if (!curr->is_rmwrcas() ||
+			      valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+				//Need to make sure we aren't the second RMW
+				CycleNode * node = mo_graph->getNode_noCreate(act);
+				if (node != NULL && node->getRMW() != NULL) {
+				  //we are the second RMW
+				  allow_read = false;
+				}
+			      }
+			}
+			
 			if (allow_read) {
 				/* Only add feasible reads */
 				mo_graph->startChanges();
@@ -1522,7 +1529,13 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {
-        if (pid < pthread_counter + 1) return pthread_map[pid];
+  union {
+    pthread_t p;
+    uint32_t v;
+  } x;
+  x.p = pid;
+  uint32_t thread_id = x.v;
+  if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
         else return NULL;
 }
 
@@ -1605,3 +1618,6 @@ Thread * ModelExecution::take_step(ModelAction *curr)
 	return action_select_next_thread(curr);
 }
 
+Fuzzer * ModelExecution::getFuzzer() {
+  return fuzzer;
+}