X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=6739d2c85ee2ca51dd3963c471c811e12f0711b3;hb=ae1340cbd7d2f75d76a4199597f454290badcc8b;hp=4ccdbce2f6700678ce62a684da817c61b4fa8db3;hpb=ed8d4600431acccf43e7ac67ab523fd7486861d0;p=model-checker.git

diff --git a/model.cc b/model.cc
index 4ccdbce..6739d2c 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))
@@ -1372,8 +1381,6 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 {
 	char buf[100];
 	char *ptr = buf;
-	if (mo_graph->checkForRMWViolation())
-		ptr += sprintf(ptr, "[RMW atomicity]");
 	if (mo_graph->checkForCycles())
 		ptr += sprintf(ptr, "[mo cycle]");
 	if (priv->failed_promise)
@@ -1407,21 +1414,10 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
-}
-
-/**
- * Check If the current partial trace is infeasible, while ignoring
- * infeasibility related to 2 RMW's reading from the same store. It does not
- * check end-of-execution feasibility.
- * @see ModelChecker::is_infeasible
- * @return whether the current partial trace is infeasible, ignoring multiple
- * RMWs reading from the same store.
- * */
-bool ModelChecker::is_infeasible_ignoreRMW() const
-{
-	return mo_graph->checkForCycles() || priv->failed_promise ||
-		priv->too_many_reads || priv->bad_synchronization ||
+	return mo_graph->checkForCycles() ||
+		priv->failed_promise ||
+		priv->too_many_reads ||
+		priv->bad_synchronization ||
 		promises_expired();
 }
 
@@ -1534,7 +1530,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.
@@ -1543,10 +1539,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;
@@ -1574,26 +1571,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;
 				}
 			}
@@ -1604,9 +1598,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();
@@ -1614,9 +1607,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;
@@ -1725,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;
 		}
 	}
 
@@ -1769,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;
 			}
 
@@ -1786,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)) {
@@ -2352,7 +2341,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			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);
+			delete promise;
 
 			promises->erase(promises->begin() + promise_index);
 			actions_to_check.push_back(read);
@@ -2660,7 +2649,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);