X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=ef9bed305fc0295af447e25365cccd6a8f2399a3;hp=9d7ff51431a1b358914dd3f49e8d8c02ee226a9d;hb=76e48f210747b7ef23387ffd7c33ea0009c1d922;hpb=8d671b5e6a8b29464e0f7c17b696cbd5286f3446

diff --git a/model.cc b/model.cc
index 9d7ff51..ef9bed3 100644
--- a/model.cc
+++ b/model.cc
@@ -729,7 +729,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 
 			read_from(curr, reads_from);
 			mo_graph->commitChanges();
-			mo_check_promises(curr->get_tid(), reads_from, NULL);
+			mo_check_promises(curr, true);
 
 			updated |= r_status;
 		} else if (!second_part_of_rmw) {
@@ -895,7 +895,7 @@ bool ModelChecker::process_write(ModelAction *curr)
 	}
 
 	mo_graph->commitChanges();
-	mo_check_promises(curr->get_tid(), curr, NULL);
+	mo_check_promises(curr, false);
 
 	get_thread(curr)->set_return_value(VALUE_NONE);
 	return updated_mod_order || updated_promises;
@@ -1619,6 +1619,14 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 		}
 	}
 
+	/*
+	 * All compatible, thread-exclusive promises must be ordered after any
+	 * concrete loads from the same thread
+	 */
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i]->is_compatible_exclusive(curr))
+			added = mo_graph->addEdge(rf, (*promises)[i]) || added;
+
 	return added;
 }
 
@@ -2304,7 +2312,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 
 	for (unsigned int i = 0; i < actions_to_check.size(); i++) {
 		ModelAction *read = actions_to_check[i];
-		mo_check_promises(read->get_tid(), write, read);
+		mo_check_promises(read, true);
 	}
 
 	return haveResolved;
@@ -2364,71 +2372,39 @@ void ModelChecker::check_promises_thread_disabled()
  * @brief Checks promises in response to addition to modification order for
  * threads.
  *
- * Definitions:
- *
- * pthread is the thread that performed the read that created the promise
- *
- * pread is the read that created the promise
- *
- * pwrite is either the first write to same location as pread by
- * pthread that is sequenced after pread or the write read by the
- * first read to the same location as pread by pthread that is
- * sequenced after pread.
- *
- * 1. If tid=pthread, then we check what other threads are reachable
- * through the mod order starting with pwrite.  Those threads cannot
- * perform a write that will resolve the promise due to modification
- * order constraints.
- *
- * 2. If the tid is not pthread, we check whether pwrite can reach the
- * action write through the modification order.  If so, that thread
- * cannot perform a future write that will resolve the promise due to
- * modificatin order constraints.
- *
- * @param tid The thread that either read from the model action write, or
- * actually did the model action write.
+ * We test whether threads are still available for satisfying promises after an
+ * addition to our modification order constraints. Those that are unavailable
+ * are "eliminated". Once all threads are eliminated from satisfying a promise,
+ * that promise has failed.
  *
- * @param write The ModelAction representing the relevant write.
- * @param read  The ModelAction that reads a promised write, or NULL otherwise.
+ * @param act The ModelAction which updated the modification order
+ * @param is_read_check Should be true if act is a read and we must check for
+ * updates to the store from which it read (there is a distinction here for
+ * RMW's, which are both a load and a store)
  */
-void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
+void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 {
-	void *location = write->get_location();
+	const ModelAction *write = is_read_check ? act->get_reads_from() : act;
+
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
+		const ModelAction *pread = promise->get_action();
 
 		// Is this promise on the same location?
-		if (act->get_location() != location)
+		if (!pread->same_var(write))
 			continue;
 
-		// same thread as the promise
-		if (act->get_tid() == tid) {
-			// make sure that the reader of this write happens after the promise
-			if ((read == NULL) || (promise->get_action()->happens_before(read))) {
-				// do we have a pwrite for the promise, if not, set it
-				if (promise->get_write() == NULL) {
-					promise->set_write(write);
-					// The pwrite cannot happen before the promise
-					if (write->happens_before(act) && (write != act)) {
-						priv->failed_promise = true;
-						return;
-					}
-				}
-
-				if (mo_graph->checkPromise(write, promise)) {
-					priv->failed_promise = true;
-					return;
-				}
-			}
+		if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
+			priv->failed_promise = true;
+			return;
 		}
 
 		// Don't do any lookups twice for the same thread
-		if (!promise->thread_is_available(tid))
+		if (!promise->thread_is_available(act->get_tid()))
 			continue;
 
-		if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
-			if (promise->eliminate_thread(tid)) {
+		if (mo_graph->checkReachable(promise, write)) {
+			if (mo_graph->checkPromise(write, promise)) {
 				priv->failed_promise = true;
 				return;
 			}
@@ -2577,7 +2553,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());
 		}