From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Dec 2012 23:14:29 +0000 (-0800)
Subject: model: distinguish between 'read' and 'acquire' in release sequences
X-Git-Tag: oopsla2013~474
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=20f8e2bc8677046c4bd7cb0bb80696ced41301f2;p=model-checker.git

model: distinguish between 'read' and 'acquire' in release sequences

When using fences, we may have a fence-acquire preceded by a non-acquire
load, where the load takes part in a "hypothetical release sequence" (as
named by Mathematizing C++). So, I add a parameter to
get_release_seq_heads() and to struct release_seq so that we record the
'acquire' operation separately from the 'read'.

For our traditional release sequences, 'acquire' and 'read' will be the
same ModelAction. But fence-acquire support will utilize distinct
actions.
---

diff --git a/model.cc b/model.cc
index a9ea7b0..dbca58e 100644
--- a/model.cc
+++ b/model.cc
@@ -1063,7 +1063,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])) {
@@ -1935,18 +1935,25 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
  * 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 */
@@ -1975,21 +1982,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();
@@ -1999,15 +2007,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));
 				}
diff --git a/model.h b/model.h
index a2bbab2..b078939 100644
--- a/model.h
+++ b/model.h
@@ -75,7 +75,11 @@ struct PendingFutureValue {
 struct release_seq {
 	/** @brief The acquire operation */
 	ModelAction *acquire;
-	/** @brief The head of the RMW chain from which 'acquire' reads; may be
+	/** @brief The read operation that may read from a release sequence;
+	 *  may be the same as acquire, or else an earlier action in the same
+	 *  thread (i.e., when 'acquire' is a fence-acquire) */
+	const ModelAction *read;
+	/** @brief The head of the RMW chain from which 'read' reads; may be
 	 *  equal to 'release' */
 	const ModelAction *rf;
 	/** @brief The head of the potential longest release sequence chain */
@@ -178,7 +182,7 @@ private:
 	void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
 	bool r_modification_order(ModelAction *curr, const ModelAction *rf);
 	bool w_modification_order(ModelAction *curr);
-	void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
+	void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
 	bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
 	bool resolve_release_sequences(void *location, work_queue_t *work_queue);