X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=82b90601048845f32a9af77d57e938e8fb11450f;hb=7888740e94be8706a4e09ae216dcf2e378257617;hp=d6ebfe5abc9f4e60920f9b08bed0112746c3afce;hpb=43144df37c0f1bb5b4efc4cf1bd2908b6cf440b9;p=model-checker.git

diff --git a/model.cc b/model.cc
index d6ebfe5..82b9060 100644
--- a/model.cc
+++ b/model.cc
@@ -521,6 +521,7 @@ bool ModelChecker::next_execution()
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
 	switch (act->get_type()) {
+	case ATOMIC_FENCE:
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
@@ -1402,14 +1403,48 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 	bool added = false;
 	ASSERT(curr->is_read());
 
+	/* Last SC fence in the current thread */
+	ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
+		/* Last SC fence in thread i */
+		ModelAction *last_sc_fence_thread_local = NULL;
+		if (int_to_id((int)i) != curr->get_tid())
+			last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+
+		/* Last SC fence in thread i, before last SC fence in current thread */
+		ModelAction *last_sc_fence_thread_before = NULL;
+		if (last_sc_fence_local)
+			last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
 		/* Iterate over actions in thread, starting from most recent */
 		action_list_t *list = &(*thrd_lists)[i];
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *act = *rit;
 
+			if (act->is_write() && act != 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;
+				}
+				/* 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;
+				}
+				/* 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;
+				}
+			}
+
 			/*
 			 * Include at most one act per-thread that "happens
 			 * before" curr. Don't consider reflexively.
@@ -1542,8 +1577,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 		}
 	}
 
+	/* Last SC fence in the current thread */
+	ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
+		/* Last SC fence in thread i, before last SC fence in current thread */
+		ModelAction *last_sc_fence_thread_before = NULL;
+		if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
+			last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
 		/* Iterate over actions in thread, starting from most recent */
 		action_list_t *list = &(*thrd_lists)[i];
 		action_list_t::reverse_iterator rit;
@@ -1570,6 +1613,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 					continue;
 			}
 
+			/* 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;
+			}
+
 			/*
 			 * Include at most one act per-thread that "happens
 			 * before" curr
@@ -1956,10 +2006,6 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
 		if (tid >= (int)vec->size())
 			vec->resize(priv->next_thread_id);
 		(*vec)[tid].push_back(act);
-
-		if ((int)thrd_last_action->size() <= tid)
-			thrd_last_action->resize(get_num_threads());
-		(*thrd_last_action)[tid] = act;
 	}
 }