X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=465849afa03b5a0946236528b8aea7f7703940b4;hb=63e202b2db7a90e176db54c864d2e54ec535c03f;hp=15f1831627e0621896fadc3638ec27e6814cfc07;hpb=b3ff4f8b32505a6e44b70ddc754af6ecb2321474;p=model-checker.git

diff --git a/model.cc b/model.cc
index 15f1831..465849a 100644
--- a/model.cc
+++ b/model.cc
@@ -1575,22 +1575,19 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 				/* 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;
 				}
 			}
@@ -1602,8 +1599,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 			if (act->happens_before(curr) && act != curr) {
 				if (act->is_write()) {
 					if (!act->equals(rf)) {
-						mo_graph->addEdge(act, rf);
-						added = true;
+						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
 					const ModelAction *prevreadfrom = act->get_reads_from();
@@ -1612,8 +1608,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 						continue;
 
 					if (!prevreadfrom->equals(rf)) {
-						mo_graph->addEdge(prevreadfrom, rf);
-						added = true;
+						added = mo_graph->addEdge(prevreadfrom, rf) || added;
 					}
 				}
 				break;
@@ -1722,8 +1717,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;
 		}
 	}
 
@@ -1766,8 +1760,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;
 			}
 
@@ -1783,14 +1776,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)) {
@@ -1816,6 +1808,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;
 }
 
@@ -2330,7 +2331,7 @@ 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;
 
 	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
@@ -2348,13 +2349,13 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			//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());
+			ASSERT(promise->is_compatible(write));
 			delete promise;
 
 			promises->erase(promises->begin() + promise_index);
 			actions_to_check.push_back(read);
 
-			resolved = true;
+			haveResolved = true;
 		} else
 			promise_index++;
 	}
@@ -2363,11 +2364,11 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 	//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;
 }
 
 /**