From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 18:07:22 +0000 (-0700)
Subject: model: release_seq synchronization generates mo_graph edge "work entries"
X-Git-Tag: pldi2013~190^2
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=65a0c0d8d991b2775d15934b07cb51b422a5d20b

model: release_seq synchronization generates mo_graph edge "work entries"

Now, when the synchronization for a ModelAction is updated while resolving
release sequences, the affected ModelAction(s) can be queued to the work_queue
for later processing (i.e., checking for mo_graph edge additions).

Note that the MOEdgeWorkEntry is not yet handled in the work_queue loop.
---

diff --git a/model.cc b/model.cc
index 7aed29b..c7a71cc 100644
--- a/model.cc
+++ b/model.cc
@@ -438,7 +438,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 			break;
 		}
 		case WORK_CHECK_RELEASE_SEQ:
-			resolve_release_sequences(work.location);
+			resolve_release_sequences(work.location, &work_queue);
 			break;
 		case WORK_CHECK_MO_EDGES:
 			/** @todo Perform follow-up mo_graph checks */
@@ -936,9 +936,12 @@ void ModelChecker::get_release_seq_heads(ModelAction *act,
  *
  * @param location The location/object that should be checked for release
  * sequence resolutions
- * @return True if any updates occurred (new synchronization, new mo_graph edges)
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ * @return True if any updates occurred (new synchronization, new mo_graph
+ * edges)
  */
-bool ModelChecker::resolve_release_sequences(void *location)
+bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
 	std::list<ModelAction *> *list;
 	list = lazy_sync_with_release->getptr(location);
@@ -961,14 +964,18 @@ bool ModelChecker::resolve_release_sequences(void *location)
 		}
 
 		if (updated) {
+			/* Re-check act for mo_graph edges */
+			work_queue->push_back(MOEdgeWorkEntry(act));
+
 			/* propagate synchronization to later actions */
 			action_list_t::reverse_iterator it = action_trace->rbegin();
 			while ((*it) != act) {
 				ModelAction *propagate = *it;
-				if (act->happens_before(propagate))
-					/** @todo new mo_graph edges along with
-					 * this synchronization? */
+				if (act->happens_before(propagate)) {
 					propagate->synchronize_with(act);
+					/* Re-check 'propagate' for mo_graph edges */
+					work_queue->push_back(MOEdgeWorkEntry(propagate));
+				}
 			}
 		}
 		if (complete) {
diff --git a/model.h b/model.h
index cf1770b..3d3eba7 100644
--- a/model.h
+++ b/model.h
@@ -136,7 +136,7 @@ private:
 	bool w_modification_order(ModelAction *curr);
 	bool release_seq_head(const ModelAction *rf,
 	                std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
-	bool resolve_release_sequences(void *location);
+	bool resolve_release_sequences(void *location, work_queue_t *work_queue);
 
 	ModelAction *diverge;