X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=f0763cbfca28971b9dfd36a0fe5e76dcae41f8aa;hp=a03ea46224f1d7a4d10f64927b9df9d385eeb21e;hb=c29b803ac6dce04a6531d33e36341eb662124835;hpb=20994240335ce1d54fb6c4b2c8df684182f0a3f9

diff --git a/model.cc b/model.cc
index a03ea462..f0763cbf 100644
--- a/model.cc
+++ b/model.cc
@@ -1082,14 +1082,15 @@ bool ModelChecker::process_write(ModelAction *curr)
 	/* Readers to which we may send our future value */
 	ModelVector<ModelAction *> send_fv;
 
-	bool updated_mod_order = w_modification_order(curr, &send_fv);
-	int promise_idx = get_promise_to_resolve(curr);
 	const ModelAction *earliest_promise_reader;
 	bool updated_promises = false;
 
-	if (promise_idx >= 0) {
-		earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
-		updated_promises = resolve_promise(curr, promise_idx);
+	bool updated_mod_order = w_modification_order(curr, &send_fv);
+	Promise *promise = pop_promise_to_resolve(curr);
+
+	if (promise) {
+		earliest_promise_reader = promise->get_reader(0);
+		updated_promises = resolve_promise(curr, promise);
 	} else
 		earliest_promise_reader = NULL;
 
@@ -1100,10 +1101,10 @@ bool ModelChecker::process_write(ModelAction *curr)
 			futurevalues->push_back(PendingFutureValue(curr, read));
 	}
 
-	if (promises->size() == 0) {
+	if (promises->empty()) {
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
 			struct PendingFutureValue pfv = (*futurevalues)[i];
-			add_future_value(pfv.writer, pfv.act);
+			add_future_value(pfv.writer, pfv.reader);
 		}
 		futurevalues->clear();
 	}
@@ -1128,6 +1129,7 @@ bool ModelChecker::process_fence(ModelAction *curr)
 	 *   use in later synchronization
 	 * fence-acquire (this function): search for hypothetical release
 	 *   sequences
+	 * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 	 */
 	bool updated = false;
 	if (curr->is_acquire()) {
@@ -1812,6 +1814,9 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 
 	/* Last SC fence in the current thread */
 	ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+	ModelAction *last_sc_write = NULL;
+	if (curr->is_seqcst())
+		last_sc_write = get_last_seq_cst_write(curr);
 
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
@@ -1863,6 +1868,12 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 				}
 			}
 
+			/* C++, Section 29.3 statement 3 (second subpoint) */
+			if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
+				added = mo_graph->addEdge(act, rf) || added;
+				break;
+			}
+
 			/*
 			 * Include at most one act per-thread that "happens
 			 * before" curr
@@ -2463,8 +2474,11 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
 	action_list_t *list = get_safe_ptr_action(obj_map, location);
 	/* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
 	action_list_t::reverse_iterator rit;
-	for (rit = list->rbegin(); rit != list->rend(); rit++)
-		if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
+	for (rit = list->rbegin(); (*rit) != curr; rit++)
+		;
+	rit++; /* Skip past curr */
+	for ( ; rit != list->rend(); rit++)
+		if ((*rit)->is_write() && (*rit)->is_seqcst())
 			return *rit;
 	return NULL;
 }
@@ -2537,29 +2551,31 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
 }
 
 /**
- * @brief Find the promise, if any to resolve for the current action
+ * @brief Find the promise (if any) to resolve for the current action and
+ * remove it from the pending promise vector
  * @param curr The current ModelAction. Should be a write.
- * @return The (non-negative) index for the Promise to resolve, if any;
- * otherwise -1
+ * @return The Promise to resolve, if any; otherwise NULL
  */
-int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+Promise * ModelChecker::pop_promise_to_resolve(const ModelAction *curr)
 {
 	for (unsigned int i = 0; i < promises->size(); i++)
-		if (curr->get_node()->get_promise(i))
-			return i;
-	return -1;
+		if (curr->get_node()->get_promise(i)) {
+			Promise *ret = (*promises)[i];
+			promises->erase(promises->begin() + i);
+			return ret;
+		}
+	return NULL;
 }
 
 /**
  * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
- * @param promise_idx The index corresponding to the promise
+ * @param promise The Promise to resolve
  * @return True if the Promise was successfully resolved; false otherwise
  */
-bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
+bool ModelChecker::resolve_promise(ModelAction *write, Promise *promise)
 {
 	ModelVector<ModelAction *> actions_to_check;
-	Promise *promise = (*promises)[promise_idx];
 
 	for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
 		ModelAction *read = promise->get_reader(i);
@@ -2571,7 +2587,6 @@ bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 	if (!mo_graph->resolvePromise(promise, write))
 		priv->failed_promise = true;
 
-	promises->erase(promises->begin() + promise_idx);
 	/**
 	 * @todo  It is possible to end up in an inconsistent state, where a
 	 * "resolved" promise may still be referenced if