From: Brian Norris <banorris@uci.edu>
Date: Thu, 4 Oct 2012 19:42:13 +0000 (-0700)
Subject: model: assign "pending" return values in release_seq_heads()
X-Git-Tag: pldi2013~102^2~2
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=2c830a91c32a55de67c21e03f36529f994d9139d;ds=sidebyside

model: assign "pending" return values in release_seq_heads()

Now that the lazy pending release sequences list is improved, return
more information from release_seq_heads().

Note that this change also affects the behavior of the last double loop;
now, even after discovering write(s) from one thread that might break the
release sequence, I continue exploring other threads. This has some pros
and cons:

Con:
* may cause more work in exploring many threads without gaining any
  extra information

Pro:
* may help discover a write that *certainly* breaks the sequence,
  whereas previously, we might have exited with an uncertain status
* builds a more thorough, complete set of writes that might break the
  release sequence

The last point is the main intention, since we will require a complete
set for end-of-execution fixups. The others balance out to a net benefit
(and possibly a bugfix).
---

diff --git a/model.cc b/model.cc
index 59b9f0b..e8b860c 100644
--- a/model.cc
+++ b/model.cc
@@ -1174,13 +1174,19 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  * @todo Finish lazy updating, when promises are fulfilled in the future
  * @param rf The action that might be part of a release sequence. Must be a
  * write.
- * @param release_heads A pass-by-reference style return parameter.  After
+ * @param release_heads A pass-by-reference style return parameter. After
  * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists
+ * relevant release sequences, if any exists with certainty
+ * @param pending A pass-by-reference style return parameter which is only used
+ * when returning false (i.e., uncertain). Returns most information regarding
+ * an uncertain release sequence, including any write operations that might
+ * break the sequence.
  * @return true, if the ModelChecker is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf,
+		rel_heads_list_t *release_heads,
+		struct release_seq *pending) const
 {
 	/* Only check for release sequences if there are no cycles */
 	if (mo_graph->checkForCycles())
@@ -1209,6 +1215,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
 	};
 	if (!rf) {
 		/* read from future: need to settle this later */
+		pending->rf = NULL;
 		return false; /* incomplete */
 	}
 
@@ -1238,6 +1245,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
 
 	ASSERT(rf->same_thread(release));
 
+	pending->writes.clear();
+
 	bool certain = true;
 	for (unsigned int i = 0; i < thrd_lists->size(); i++) {
 		if (id_to_int(rf->get_tid()) == (int)i)
@@ -1281,14 +1290,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *re
 				/* release --mo-> act --mo--> rf */
 				return true; /* complete */
 			}
+			/* act may break release sequence */
+			pending->writes.push_back(act);
 			certain = false;
 		}
 		if (!future_ordered)
-			return false; /* This thread is uncertain */
+			certain = false; /* This thread is uncertain */
 	}
 
-	if (certain)
+	if (certain) {
 		release_heads->push_back(release);
+		pending->writes.clear();
+	} else {
+		pending->release = release;
+		pending->rf = rf;
+	}
 	return certain;
 }
 
@@ -1310,7 +1326,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
 	struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
 	sequence->acquire = act;
 
-	if (!release_seq_heads(rf, release_heads)) {
+	if (!release_seq_heads(rf, release_heads, sequence)) {
 		/* add act to 'lazy checking' list */
 		pending_rel_seqs->push_back(sequence);
 	} else {
@@ -1348,7 +1364,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 		const ModelAction *rf = act->get_reads_from();
 		rel_heads_list_t release_heads;
 		bool complete;
-		complete = release_seq_heads(rf, &release_heads);
+		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]))
diff --git a/model.h b/model.h
index 6d892cb..d5dc422 100644
--- a/model.h
+++ b/model.h
@@ -163,7 +163,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);
-	bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+	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);
 	void do_complete_join(ModelAction *join);