X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=fc86d5c7e9955d3b5e4ccd17cc25ccc5e2e38fa6;hp=39af266a3d596505ed7bd9fa05cc15f08143df8e;hb=4159ba45e83f6542e3a3320e83bca9fbaf2da3ea;hpb=9875c652986098797f7fc8bee9def1c5b6a54ee5

diff --git a/model.cc b/model.cc
index 39af266a..fc86d5c7 100644
--- a/model.cc
+++ b/model.cc
@@ -1997,6 +1997,35 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
 	return NULL;
 }
 
+/**
+ * Gets the last memory_order_seq_cst fence (in the total global sequence)
+ * performed in a particular thread, prior to a particular fence.
+ * @param tid The ID of the thread to check
+ * @param before_fence The fence from which to begin the search; if NULL, then
+ * search for the most recent fence in the thread.
+ * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
+ */
+ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
+{
+	/* All fences should have NULL location */
+	action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+	action_list_t::reverse_iterator rit = list->rbegin();
+
+	if (before_fence) {
+		for (; rit != list->rend(); rit++)
+			if (*rit == before_fence)
+				break;
+
+		ASSERT(*rit == before_fence);
+		rit++;
+	}
+
+	for (; rit != list->rend(); rit++)
+		if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
+			return *rit;
+	return NULL;
+}
+
 /**
  * Gets the last unlock operation performed on a particular mutex (i.e., memory
  * location). This function identifies the mutex according to the current