X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=da982d0db415395ed2be39e9dfcf3b34f74c1efe;hp=1ec72738ba3d0622bb27c8dedb3eab4c875aa90c;hb=c2d7fa973e562c194eb732d8dc58ab7659b7a2ee;hpb=202542965363285e68bb33654a62fe816c69b176

diff --git a/model.cc b/model.cc
index 1ec7273..da982d0 100644
--- a/model.cc
+++ b/model.cc
@@ -1388,7 +1388,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 {
 	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
 	unsigned int i;
-
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
 		const ModelAction *write_after_read = NULL;
@@ -1403,7 +1402,7 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 				break;
 			else if (act->is_write())
 				write_after_read = act;
-			else if (act->is_read()&&act->get_reads_from()!=NULL) {
+			else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
 				write_after_read = act->get_reads_from();
 			}
 		}
@@ -1411,7 +1410,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 		if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
 			return false;
 	}
-
 	return true;
 }
 
@@ -1839,7 +1837,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 				!act->same_thread(curr) &&
 				act->get_location() == curr->get_location() &&
 				promise->get_value() == curr->get_value()) {
-			curr->get_node()->set_promise(i);
+			curr->get_node()->set_promise(i, act->is_rmw());
 		}
 	}
 }