X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=15718e1fe32a498a4d9d1c7b651c35a4c8b5f281;hb=5236e7a4403ccc6d28b3fdc746c5710d6190310a;hp=c9b8460c66daa62f56a4a533bdbad44b3f41c3ba;hpb=80bd54a5423d5977c81f5f6db31a475b1f17ecce;p=model-checker.git

diff --git a/model.cc b/model.cc
index c9b8460..15718e1 100644
--- a/model.cc
+++ b/model.cc
@@ -735,10 +735,13 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 		} else if (!second_part_of_rmw) {
 			/* Read from future value */
 			struct future_value fv = curr->get_node()->get_future_value();
+			Promise *promise = new Promise(curr, fv);
 			value = fv.value;
-			curr->set_value(fv.value);
-			curr->set_read_from(NULL);
-			promises->push_back(new Promise(curr, fv));
+			curr->set_read_from_promise(promise);
+			promises->push_back(promise);
+			mo_graph->startChanges();
+			updated = r_modification_order(curr, promise);
+			mo_graph->commitChanges();
 		}
 		get_thread(curr)->set_return_value(value);
 		return updated;
@@ -1304,8 +1307,14 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
 			if (act->is_read()) {
 				const ModelAction *rf = act->get_reads_from();
-				if (rf != NULL && r_modification_order(act, rf))
-					updated = true;
+				const Promise *promise = act->get_reads_from_promise();
+				if (rf) {
+					if (r_modification_order(act, rf))
+						updated = true;
+				} else if (promise) {
+					if (r_modification_order(act, promise))
+						updated = true;
+				}
 			}
 			if (act->is_write()) {
 				if (w_modification_order(act))
@@ -1416,8 +1425,11 @@ bool ModelChecker::is_infeasible() const
 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	ModelAction *lastread = get_last_action(act->get_tid());
 	lastread->process_rmw(act);
-	if (act->is_rmw() && lastread->get_reads_from() != NULL) {
-		mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+	if (act->is_rmw()) {
+		if (lastread->get_reads_from())
+			mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+		else
+			mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
 		mo_graph->commitChanges();
 	}
 	return lastread;
@@ -1521,7 +1533,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
  * read.
  *
  * Basic idea is the following: Go through each other thread and find
- * the lastest action that happened before our read.  Two cases:
+ * the last action that happened before our read.  Two cases:
  *
  * (1) The action is a write => that write must either occur before
  * the write we read from or be the write we read from.
@@ -1530,10 +1542,11 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
  * must occur before the write we read from or be the same write.
  *
  * @param curr The current action. Must be a read.
- * @param rf The action that curr reads from. Must be a write.
+ * @param rf The ModelAction or Promise that curr reads from. Must be a write.
  * @return True if modification order edges were added; false otherwise
  */
-bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+template <typename rf_type>
+bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 {
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
@@ -1561,26 +1574,23 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
-			if (act->is_write() && act != rf && act != curr) {
+			if (act->is_write() && !act->equals(rf) && act != curr) {
 				/* C++, Section 29.3 statement 5 */
 				if (curr->is_seqcst() && last_sc_fence_thread_local &&
 						*act < *last_sc_fence_thread_local) {
-					mo_graph->addEdge(act, rf);
-					added = true;
+					added = mo_graph->addEdge(act, rf) || added;
 					break;
 				}
 				/* C++, Section 29.3 statement 4 */
 				else if (act->is_seqcst() && last_sc_fence_local &&
 						*act < *last_sc_fence_local) {
-					mo_graph->addEdge(act, rf);
-					added = true;
+					added = mo_graph->addEdge(act, rf) || added;
 					break;
 				}
 				/* C++, Section 29.3 statement 6 */
 				else if (last_sc_fence_thread_before &&
 						*act < *last_sc_fence_thread_before) {
-					mo_graph->addEdge(act, rf);
-					added = true;
+					added = mo_graph->addEdge(act, rf) || added;
 					break;
 				}
 			}
@@ -1591,9 +1601,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 			 */
 			if (act->happens_before(curr) && act != curr) {
 				if (act->is_write()) {
-					if (rf != act) {
-						mo_graph->addEdge(act, rf);
-						added = true;
+					if (!act->equals(rf)) {
+						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
 					const ModelAction *prevreadfrom = act->get_reads_from();
@@ -1601,9 +1610,8 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 					if (prevreadfrom == NULL)
 						continue;
 
-					if (rf != prevreadfrom) {
-						mo_graph->addEdge(prevreadfrom, rf);
-						added = true;
+					if (!prevreadfrom->equals(rf)) {
+						added = mo_graph->addEdge(prevreadfrom, rf) || added;
 					}
 				}
 				break;
@@ -1614,70 +1622,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 	return added;
 }
 
-/** This method fixes up the modification order when we resolve a
- *  promises.  The basic problem is that actions that occur after the
- *  read curr could not property add items to the modification order
- *  for our read.
- *
- *  So for each thread, we find the earliest item that happens after
- *  the read curr.  This is the item we have to fix up with additional
- *  constraints.  If that action is write, we add a MO edge between
- *  the Action rf and that action.  If the action is a read, we add a
- *  MO edge between the Action rf, and whatever the read accessed.
- *
- * @param curr is the read ModelAction that we are fixing up MO edges for.
- * @param rf is the write ModelAction that curr reads from.
- *
- */
-void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
-{
-	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
-	unsigned int i;
-	ASSERT(curr->is_read());
-
-	/* Iterate over all threads */
-	for (i = 0; i < thrd_lists->size(); i++) {
-		/* Iterate over actions in thread, starting from most recent */
-		action_list_t *list = &(*thrd_lists)[i];
-		action_list_t::reverse_iterator rit;
-		ModelAction *lastact = NULL;
-
-		/* Find last action that happens after curr that is either not curr or a rmw */
-		for (rit = list->rbegin(); rit != list->rend(); rit++) {
-			ModelAction *act = *rit;
-			if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
-				lastact = act;
-			} else
-				break;
-		}
-
-			/* Include at most one act per-thread that "happens before" curr */
-		if (lastact != NULL) {
-			if (lastact == curr) {
-				//Case 1: The resolved read is a RMW, and we need to make sure
-				//that the write portion of the RMW mod order after rf
-
-				mo_graph->addEdge(rf, lastact);
-			} else if (lastact->is_read()) {
-				//Case 2: The resolved read is a normal read and the next
-				//operation is a read, and we need to make sure the value read
-				//is mod ordered after rf
-
-				const ModelAction *postreadfrom = lastact->get_reads_from();
-				if (postreadfrom != NULL && rf != postreadfrom)
-					mo_graph->addEdge(rf, postreadfrom);
-			} else {
-				//Case 3: The resolved read is a normal read and the next
-				//operation is a write, and we need to make sure that the
-				//write is mod ordered after rf
-				if (lastact != rf)
-					mo_graph->addEdge(rf, lastact);
-			}
-			break;
-		}
-	}
-}
-
 /**
  * Updates the mo_graph with the constraints imposed from the current write.
  *
@@ -1712,8 +1656,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 			 so we are initialized. */
 		ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
 		if (last_seq_cst != NULL) {
-			mo_graph->addEdge(last_seq_cst, curr);
-			added = true;
+			added = mo_graph->addEdge(last_seq_cst, curr) || added;
 		}
 	}
 
@@ -1756,8 +1699,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 			/* C++, Section 29.3 statement 7 */
 			if (last_sc_fence_thread_before && act->is_write() &&
 					*act < *last_sc_fence_thread_before) {
-				mo_graph->addEdge(act, curr);
-				added = true;
+				added = mo_graph->addEdge(act, curr) || added;
 				break;
 			}
 
@@ -1773,14 +1715,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				 *   readfrom(act) --mo--> act
 				 */
 				if (act->is_write())
-					mo_graph->addEdge(act, curr);
+					added = mo_graph->addEdge(act, curr) || added;
 				else if (act->is_read()) {
 					//if previous read accessed a null, just keep going
 					if (act->get_reads_from() == NULL)
 						continue;
-					mo_graph->addEdge(act->get_reads_from(), curr);
+					added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
 				}
-				added = true;
 				break;
 			} else if (act->is_read() && !act->could_synchronize_with(curr) &&
 			                             !act->same_thread(curr)) {
@@ -1806,6 +1747,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 		}
 	}
 
+	/*
+	 * All compatible, thread-exclusive promises must be ordered after any
+	 * concrete stores to the same thread, or else they can be merged with
+	 * this store later
+	 */
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i]->is_compatible_exclusive(curr))
+			added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
 	return added;
 }
 
@@ -2320,44 +2270,44 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
  */
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
-	bool resolved = false;
+	bool haveResolved = false;
 	std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
+	promise_list_t mustResolve, resolved;
 
 	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
 			ModelAction *read = promise->get_action();
-			if (read->is_rmw()) {
-				mo_graph->addRMWEdge(write, read);
-			}
 			read_from(read, write);
-			//First fix up the modification order for actions that happened
-			//before the read
-			r_modification_order(read, write);
-			//Next fix up the modification order for actions that happened
-			//after the read.
-			post_r_modification_order(read, write);
 			//Make sure the promise's value matches the write's value
-			ASSERT(promise->get_value() == write->get_value());
-			delete promise;
+			ASSERT(promise->is_compatible(write));
+			mo_graph->resolvePromise(read, write, &mustResolve);
 
+			resolved.push_back(promise);
 			promises->erase(promises->begin() + promise_index);
 			actions_to_check.push_back(read);
 
-			resolved = true;
+			haveResolved = true;
 		} else
 			promise_index++;
 	}
 
+	for (unsigned int i = 0; i < mustResolve.size(); i++) {
+		if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
+				== resolved.end())
+			priv->failed_promise = true;
+	}
+	for (unsigned int i = 0; i < resolved.size(); i++)
+		delete resolved[i];
 	//Check whether reading these writes has made threads unable to
 	//resolve promises
 
 	for (unsigned int i = 0; i < actions_to_check.size(); i++) {
-		ModelAction *read=actions_to_check[i];
+		ModelAction *read = actions_to_check[i];
 		mo_check_promises(read->get_tid(), write, read);
 	}
 
-	return resolved;
+	return haveResolved;
 }
 
 /**
@@ -2443,13 +2393,12 @@ void ModelChecker::check_promises_thread_disabled()
  */
 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
 {
-	void *location = write->get_location();
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
 		const ModelAction *act = promise->get_action();
 
 		// Is this promise on the same location?
-		if (act->get_location() != location)
+		if (!act->same_var(write))
 			continue;
 
 		// same thread as the promise
@@ -2627,7 +2576,7 @@ void ModelChecker::dumpGraph(char *filename) const
 	for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
 		ModelAction *action = *it;
 		if (action->is_read()) {
-			fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
+			fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
 			if (action->get_reads_from() != NULL)
 				fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
 		}
@@ -2647,7 +2596,6 @@ void ModelChecker::dumpGraph(char *filename) const
 void ModelChecker::print_summary() const
 {
 #if SUPPORT_MOD_ORDER_DUMP
-	scheduler->print();
 	char buffername[100];
 	sprintf(buffername, "exec%04u", stats.num_total);
 	mo_graph->dumpGraphToFile(buffername);