X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=d9ff365e6808494c4c667272f7dd9b7c4f9d5a5f;hb=bee1e27429b9a66e414eb83cf14e2089dd40a79e;hp=bf602246b5f83be35e924a772a874949dcf0ba56;hpb=5ea8e3d5d861ed363e5ac5f3b20b8181dd197efb;p=model-checker.git

diff --git a/model.cc b/model.cc
index bf60224..d9ff365 100644
--- a/model.cc
+++ b/model.cc
@@ -1812,6 +1812,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++) {
@@ -1831,7 +1834,18 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
-			if (act->is_write() && !act->equals(rf) && act != curr) {
+			/* Skip curr */
+			if (act == curr)
+				continue;
+			/* Don't want to add reflexive edges on 'rf' */
+			if (act->equals(rf)) {
+				if (act->happens_before(curr))
+					break;
+				else
+					continue;
+			}
+
+			if (act->is_write()) {
 				/* C++, Section 29.3 statement 5 */
 				if (curr->is_seqcst() && last_sc_fence_thread_local &&
 						*act < *last_sc_fence_thread_local) {
@@ -1852,15 +1866,19 @@ 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. Don't consider reflexively.
+			 * before" curr
 			 */
-			if (act->happens_before(curr) && act != curr) {
+			if (act->happens_before(curr)) {
 				if (act->is_write()) {
-					if (!act->equals(rf)) {
-						added = mo_graph->addEdge(act, rf) || added;
-					}
+					added = mo_graph->addEdge(act, rf) || added;
 				} else {
 					const ModelAction *prevrf = act->get_reads_from();
 					const Promise *prevrf_promise = act->get_reads_from_promise();
@@ -2454,8 +2472,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;
 }
@@ -2933,15 +2954,6 @@ void ModelChecker::add_thread(Thread *t)
 	scheduler->add_thread(t);
 }
 
-/**
- * Removes a thread from the scheduler.
- * @param the thread to remove.
- */
-void ModelChecker::remove_thread(Thread *t)
-{
-	scheduler->remove_thread(t);
-}
-
 /**
  * @brief Get a Thread reference by its ID
  * @param tid The Thread's ID
@@ -3030,6 +3042,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
 	DBG();
 	Thread *old = thread_current();
+	scheduler->set_current_thread(NULL);
 	ASSERT(!old->get_pending());
 	old->set_pending(act);
 	if (Thread::swap(old, &system_context) < 0) {