X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=715a2584f36a1538528489d60f987142ad0f2a77;hb=84d0cd2f078f4cb15c318a0fef2515feab570375;hp=2f9ec63f00d5e6bf113c18d17386dfc22eeea7cd;hpb=39c0de028fe3b1c1d229ecf715007c751ddab445;p=model-checker.git

diff --git a/model.cc b/model.cc
index 2f9ec63..715a258 100644
--- a/model.cc
+++ b/model.cc
@@ -858,6 +858,56 @@ bool ModelChecker::process_write(ModelAction *curr)
 	return updated_mod_order || updated_promises;
 }
 
+/**
+ * Process a fence ModelAction
+ * @param curr The ModelAction to process
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_fence(ModelAction *curr)
+{
+	/*
+	 * fence-relaxed: no-op
+	 * fence-release: only log the occurence (not in this function), for
+	 *   use in later synchronization
+	 * fence-acquire (this function): search for hypothetical release
+	 *   sequences
+	 */
+	bool updated = false;
+	if (curr->is_acquire()) {
+		action_list_t *list = action_trace;
+		action_list_t::reverse_iterator rit;
+		/* Find X : is_read(X) && X --sb-> curr */
+		for (rit = list->rbegin(); rit != list->rend(); rit++) {
+			ModelAction *act = *rit;
+			if (act == curr)
+				continue;
+			if (act->get_tid() != curr->get_tid())
+				continue;
+			/* Stop at the beginning of the thread */
+			if (act->is_thread_start())
+				break;
+			/* Stop once we reach a prior fence-acquire */
+			if (act->is_fence() && act->is_acquire())
+				break;
+			if (!act->is_read())
+				continue;
+			/* read-acquire will find its own release sequences */
+			if (act->is_acquire())
+				continue;
+
+			/* Establish hypothetical release sequences */
+			rel_heads_list_t release_heads;
+			get_release_seq_heads(curr, act, &release_heads);
+			for (unsigned int i = 0; i < release_heads.size(); i++)
+				if (!curr->synchronize_with(release_heads[i]))
+					set_bad_synchronization();
+			if (release_heads.size() != 0)
+				updated = true;
+		}
+	}
+	return updated;
+}
+
 /**
  * @brief Process the current action for thread-related activity
  *
@@ -1063,7 +1113,7 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 	act->set_read_from(rf);
 	if (rf != NULL && act->is_acquire()) {
 		rel_heads_list_t release_heads;
-		get_release_seq_heads(act, &release_heads);
+		get_release_seq_heads(act, act, &release_heads);
 		int num_heads = release_heads.size();
 		for (unsigned int i = 0; i < release_heads.size(); i++)
 			if (!act->synchronize_with(release_heads[i])) {
@@ -1173,6 +1223,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			if (act->is_write() && process_write(act))
 				update = true;
 
+			if (act->is_fence() && process_fence(act))
+				update_all = true;
+
 			if (act->is_mutex_op() && process_mutex(act))
 				update_all = true;
 
@@ -1464,18 +1517,21 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 						*act < *last_sc_fence_thread_local) {
 					mo_graph->addEdge(act, rf);
 					added = true;
+					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;
+					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;
+					break;
 				}
 			}
 
@@ -1652,6 +1708,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 					*act < *last_sc_fence_thread_before) {
 				mo_graph->addEdge(act, curr);
 				added = true;
+				break;
 			}
 
 			/*
@@ -1797,6 +1854,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 
 		if (rf->is_release())
 			release_heads->push_back(rf);
+		else if (rf->get_last_fence_release())
+			release_heads->push_back(rf->get_last_fence_release());
 		if (!rf->is_rmw())
 			break; /* End of RMW chain */
 
@@ -1822,8 +1881,17 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 	if (rf->is_release())
 		return true; /* complete */
 
-	/* else relaxed write; check modification order for contiguous subsequence
-	 * -> rf must be same thread as release */
+	/* else relaxed write
+	 * - check for fence-release in the same thread (29.8, stmt. 3)
+	 * - check modification order for contiguous subsequence
+	 *   -> rf must be same thread as release */
+
+	const ModelAction *fence_release = rf->get_last_fence_release();
+	/* Synchronize with a fence-release unconditionally; we don't need to
+	 * find any more "contiguous subsequence..." for it */
+	if (fence_release)
+		release_heads->push_back(fence_release);
+
 	int tid = id_to_int(rf->get_tid());
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
 	action_list_t *list = &(*thrd_lists)[tid];
@@ -1833,14 +1901,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 	rit = std::find(list->rbegin(), list->rend(), rf);
 	ASSERT(rit != list->rend());
 
-	/* Find the last write/release */
-	for (; rit != list->rend(); rit++)
+	/* Find the last {write,fence}-release */
+	for (; rit != list->rend(); rit++) {
+		if (fence_release && *(*rit) < *fence_release)
+			break;
 		if ((*rit)->is_release())
 			break;
+	}
 	if (rit == list->rend()) {
 		/* No write-release in this thread */
 		return true; /* complete */
-	}
+	} else if (fence_release && *(*rit) < *fence_release) {
+		/* The fence-release is more recent (and so, "stronger") than
+		 * the most recent write-release */
+		return true; /* complete */
+	} /* else, need to establish contiguous release sequence */
 	ModelAction *release = *rit;
 
 	ASSERT(rf->same_thread(release));
@@ -1913,22 +1988,29 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 }
 
 /**
- * A public interface for getting the release sequence head(s) with which a
+ * An interface for getting the release sequence head(s) with which a
  * given ModelAction must synchronize. This function only returns a non-empty
  * result when it can locate a release sequence head with certainty. Otherwise,
  * it may mark the internal state of the ModelChecker so that it will handle
- * the release sequence at a later time, causing @a act to update its
+ * the release sequence at a later time, causing @a acquire to update its
  * synchronization at some later point in execution.
- * @param act The 'acquire' action that may read from a release sequence
+ *
+ * @param acquire The 'acquire' action that may synchronize with a release
+ * sequence
+ * @param read The read action that may read from a release sequence; this may
+ * be the same as acquire, or else an earlier action in the same thread (i.e.,
+ * when 'acquire' is a fence-acquire)
  * @param release_heads A pass-by-reference return parameter. Will be filled
  * with the head(s) of the release sequence(s), if they exists with certainty.
  * @see ModelChecker::release_seq_heads
  */
-void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
+void ModelChecker::get_release_seq_heads(ModelAction *acquire,
+		ModelAction *read, rel_heads_list_t *release_heads)
 {
-	const ModelAction *rf = act->get_reads_from();
+	const ModelAction *rf = read->get_reads_from();
 	struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
-	sequence->acquire = act;
+	sequence->acquire = acquire;
+	sequence->read = read;
 
 	if (!release_seq_heads(rf, release_heads, sequence)) {
 		/* add act to 'lazy checking' list */
@@ -1957,21 +2039,22 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 	std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
 	while (it != pending_rel_seqs->end()) {
 		struct release_seq *pending = *it;
-		ModelAction *act = pending->acquire;
+		ModelAction *acquire = pending->acquire;
+		const ModelAction *read = pending->read;
 
 		/* Only resolve sequences on the given location, if provided */
-		if (location && act->get_location() != location) {
+		if (location && read->get_location() != location) {
 			it++;
 			continue;
 		}
 
-		const ModelAction *rf = act->get_reads_from();
+		const ModelAction *rf = read->get_reads_from();
 		rel_heads_list_t release_heads;
 		bool complete;
 		complete = release_seq_heads(rf, &release_heads, pending);
 		for (unsigned int i = 0; i < release_heads.size(); i++) {
-			if (!act->has_synchronized_with(release_heads[i])) {
-				if (act->synchronize_with(release_heads[i]))
+			if (!acquire->has_synchronized_with(release_heads[i])) {
+				if (acquire->synchronize_with(release_heads[i]))
 					updated = true;
 				else
 					set_bad_synchronization();
@@ -1981,15 +2064,16 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		if (updated) {
 			/* Re-check all pending release sequences */
 			work_queue->push_back(CheckRelSeqWorkEntry(NULL));
-			/* Re-check act for mo_graph edges */
-			work_queue->push_back(MOEdgeWorkEntry(act));
+			/* Re-check read-acquire for mo_graph edges */
+			if (acquire->is_read())
+				work_queue->push_back(MOEdgeWorkEntry(acquire));
 
 			/* propagate synchronization to later actions */
 			action_list_t::reverse_iterator rit = action_trace->rbegin();
-			for (; (*rit) != act; rit++) {
+			for (; (*rit) != acquire; rit++) {
 				ModelAction *propagate = *rit;
-				if (act->happens_before(propagate)) {
-					propagate->synchronize_with(act);
+				if (acquire->happens_before(propagate)) {
+					propagate->synchronize_with(acquire);
 					/* Re-check 'propagate' for mo_graph edges */
 					work_queue->push_back(MOEdgeWorkEntry(propagate));
 				}