X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=3e54a001a4541b8d5acada69e76c189ff5e82b36;hp=c77d4e17d4627213d2510774fe9c5d853b91257e;hb=50b95c3747f4fe79b2ab1a1a6fc303224e16e418;hpb=def20b2249cf6902b4170965cd30a8e27ecc24f1

diff --git a/model.cc b/model.cc
index c77d4e1..3e54a00 100644
--- a/model.cc
+++ b/model.cc
@@ -100,16 +100,29 @@ modelclock_t ModelChecker::get_next_seq_num()
 }
 
 /**
- * Choose the next thread in the replay sequence.
+ * @brief Choose the next thread to execute.
  *
- * If the replay sequence has reached the 'diverge' point, returns a thread
- * from the backtracking set. Otherwise, simply returns the next thread in the
- * sequence that is being replayed.
+ * This function chooses the next thread that should execute. It can force the
+ * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
+ * followed by a THREAD_START, or it can enforce execution replay/backtracking.
+ * The model-checker may have no preference regarding the next thread (i.e.,
+ * when exploring a new execution ordering), in which case this will return
+ * NULL.
+ * @param curr The current ModelAction. This action might guide the choice of
+ * next thread.
+ * @return The next thread to run. If the model-checker has no preference, NULL.
  */
-Thread * ModelChecker::get_next_replay_thread()
+Thread * ModelChecker::get_next_thread(ModelAction *curr)
 {
 	thread_id_t tid;
 
+	/* Do not split atomic actions. */
+	if (curr->is_rmwr())
+		return thread_current();
+	/* The THREAD_CREATE action points to the created Thread */
+	else if (curr->get_type() == THREAD_CREATE)
+		return (Thread *)curr->get_location();
+
 	/* Have we completed exploring the preselected path? */
 	if (diverge == NULL)
 		return NULL;
@@ -245,6 +258,49 @@ ModelAction * ModelChecker::get_next_backtrack()
 	return next;
 }
 
+/**
+ * Processes a read or rmw model action.
+ * @param curr is the read model action to process.
+ * @param th is the thread
+ * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
+ * @return True if processing this read updates the mo_graph.
+ */
+
+bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
+	uint64_t value;
+	bool updated=false;
+	while(true) {
+		const ModelAction *reads_from = curr->get_node()->get_read_from();
+		if (reads_from != NULL) {
+			value = reads_from->get_value();
+				/* Assign reads_from, perform release/acquire synchronization */
+			curr->read_from(reads_from);
+			if (!second_part_of_rmw) {
+				check_recency(curr,false);
+			}
+
+			bool r_status=r_modification_order(curr,reads_from);
+
+			if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+				mo_graph->rollbackChanges();
+				too_many_reads=false;
+				continue;
+			}
+
+			mo_graph->commitChanges();
+			updated |= r_status;
+		} else {
+			/* Read from future value */
+			value = curr->get_node()->get_future_value();
+			curr->read_from(NULL);
+			Promise *valuepromise = new Promise(curr, value);
+			promises->push_back(valuepromise);
+		}
+		th->set_return_value(value);
+		return updated;
+	}
+}
+
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
@@ -259,13 +315,13 @@ ModelAction * ModelChecker::get_next_backtrack()
  */
 Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
-	bool already_added = false;
+	bool second_part_of_rmw = false;
 
 	ASSERT(curr);
 
 	if (curr->is_rmwc() || curr->is_rmw()) {
 		ModelAction *tmp = process_rmw(curr);
-		already_added = true;
+		second_part_of_rmw = true;
 		delete curr;
 		curr = tmp;
 	} else {
@@ -296,82 +352,76 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		}
 	}
 
-	/* Assign 'creation' parent */
-	if (curr->get_type() == THREAD_CREATE) {
+	/* Thread specific actions */
+	switch(curr->get_type()) {
+	case THREAD_CREATE: {
 		Thread *th = (Thread *)curr->get_location();
 		th->set_creation(curr);
-	} else if (curr->get_type() == THREAD_JOIN) {
+		break;
+	}
+	case THREAD_JOIN: {
 		Thread *wait, *join;
 		wait = get_thread(curr->get_tid());
 		join = (Thread *)curr->get_location();
 		if (!join->is_complete())
 			scheduler->wait(wait, join);
-	} else if (curr->get_type() == THREAD_FINISH) {
+		break;
+	}
+	case THREAD_FINISH: {
 		Thread *th = get_thread(curr->get_tid());
 		while (!th->wait_list_empty()) {
 			Thread *wake = th->pop_wait_list();
 			scheduler->wake(wake);
 		}
 		th->complete();
+		break;
 	}
-
-	/* Deal with new thread */
-	if (curr->get_type() == THREAD_START)
+	case THREAD_START: {
 		check_promises(NULL, curr->get_cv());
+		break;
+	}
+	default:
+		break;
+	}
 
-	/* Assign reads_from values */
 	Thread *th = get_thread(curr->get_tid());
-	uint64_t value = VALUE_NONE;
+
 	bool updated = false;
 	if (curr->is_read()) {
-		const ModelAction *reads_from = curr->get_node()->get_read_from();
-		if (reads_from != NULL) {
-			value = reads_from->get_value();
-			/* Assign reads_from, perform release/acquire synchronization */
-			curr->read_from(reads_from);
-			if (r_modification_order(curr,reads_from))
-				updated = true;
-		} else {
-			/* Read from future value */
-			value = curr->get_node()->get_future_value();
-			curr->read_from(NULL);
-			Promise *valuepromise = new Promise(curr, value);
-			promises->push_back(valuepromise);
-		}
-	} else if (curr->is_write()) {
-		if (w_modification_order(curr))
-			updated = true;
-		if (resolve_promises(curr))
-			updated = true;
+		updated=process_read(curr, th, second_part_of_rmw);
+	}
+
+	if (curr->is_write()) {
+		bool updated_mod_order=w_modification_order(curr);
+		bool updated_promises=resolve_promises(curr);
+		updated=updated_mod_order|updated_promises;
+
+		mo_graph->commitChanges();
+		th->set_return_value(VALUE_NONE);
 	}
 
 	if (updated)
 		resolve_release_sequences(curr->get_location());
 
-	th->set_return_value(value);
-
 	/* Add action to list.  */
-	if (!already_added)
+	if (!second_part_of_rmw)
 		add_action_to_lists(curr);
 
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
-	if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
-	          !currnode->future_value_empty() || !currnode->promise_empty())
-		if (!priv->next_backtrack || *curr > *priv->next_backtrack)
-			priv->next_backtrack = curr;
+	if ((!parnode->backtrack_empty() ||
+	                !currnode->read_from_empty() ||
+	                !currnode->future_value_empty() ||
+	                !currnode->promise_empty())
+	            && (!priv->next_backtrack ||
+	                *curr > *priv->next_backtrack)) {
+		priv->next_backtrack = curr;
+	}
 
 	set_backtracking(curr);
 
-	/* Do not split atomic actions. */
-	if (curr->is_rmwr())
-		return thread_current();
-	/* The THREAD_CREATE action points to the created Thread */
-	else if (curr->get_type() == THREAD_CREATE)
-		return (Thread *)curr->get_location();
-	else
-		return get_next_replay_thread();
+	return get_next_thread(curr);
 }
 
 /** @returns whether the current partial trace must be a prefix of a
@@ -400,6 +450,101 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	return lastread;
 }
 
+/**
+ * Checks whether a thread has read from the same write for too many times
+ * without seeing the effects of a later write.
+ *
+ * Basic idea:
+ * 1) there must a different write that we could read from that would satisfy the modification order,
+ * 2) we must have read from the same value in excess of maxreads times, and
+ * 3) that other write must have been in the reads_from set for maxreads times.
+ *
+ * If so, we decide that the execution is no longer feasible.
+ */
+void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+	if (params.maxreads != 0) {
+		if (curr->get_node()->get_read_from_size() <= 1)
+			return;
+
+		//Must make sure that execution is currently feasible...  We could
+		//accidentally clear by rolling back
+		if (!isfeasible())
+			return;
+
+		std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+		int tid = id_to_int(curr->get_tid());
+
+		/* Skip checks */
+		if ((int)thrd_lists->size() <= tid)
+			return;
+
+		action_list_t *list = &(*thrd_lists)[tid];
+
+		action_list_t::reverse_iterator rit = list->rbegin();
+		/* Skip past curr */
+		if (!already_added) {
+			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
+		int count=0;
+		for (; count < params.maxreads; rit++,count++) {
+			if (rit==list->rend())
+				return;
+			ModelAction *act = *rit;
+			if (!act->is_read())
+				return;
+			if (act->get_reads_from() != curr->get_reads_from())
+				return;
+			if (act->get_node()->get_read_from_size() <= 1)
+				return;
+		}
+
+		for (int i=0;i<curr->get_node()->get_read_from_size();i++) {
+			//Get write
+			const ModelAction * write=curr->get_node()->get_read_from_at(i);
+			//Need a different write
+			if (write==curr->get_reads_from())
+				continue;
+
+			/* Test to see whether this is a feasible write to read from*/
+			r_modification_order(curr, write);
+			bool feasiblereadfrom=isfeasible();
+			mo_graph->rollbackChanges();
+
+			if (!feasiblereadfrom)
+				continue;
+			rit=ritcopy;
+
+			bool feasiblewrite=true;
+			//new we need to see if this write works for everyone
+
+			for (int loop=count;loop>0;loop--,rit++) {
+				ModelAction *act=*rit;
+				bool foundvalue=false;
+				for(int j=0;j<act->get_node()->get_read_from_size();j++) {
+					if (act->get_node()->get_read_from_at(i)==write) {
+						foundvalue=true;
+						break;
+					}
+				}
+				if (!foundvalue) {
+					feasiblewrite=false;
+					break;
+				}
+			}
+			if (feasiblewrite) {
+				too_many_reads = true;
+				return;
+			}
+		}
+	}
+}
+
 /**
  * Updates the mo_graph with the constraints imposed from the current read.
  * @param curr The current action. Must be a read.
@@ -510,10 +655,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
-				if (act->is_read())
-					mo_graph->addEdge(act->get_reads_from(), curr);
-				else
+				/*
+				 * Note: if act is RMW, just add edge:
+				 *   act --mo--> curr
+				 * The following edge should be handled elsewhere:
+				 *   readfrom(act) --mo--> act
+				 */
+				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;
 			} else if (act->is_read() && !act->is_synchronizing(curr) &&