From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 16:52:49 +0000 (-0700)
Subject: model: add work queue loop
X-Git-Tag: pldi2013~190^2~1
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=f82a95581e303d67ea57de4ae9e888be10558866;p=model-checker.git

model: add work queue loop

This commit does not change the actual computations performed yet. It only
prepares a loop structure in which we could perform many different Work items,
queueing them up as they are generated.
---

diff --git a/model.cc b/model.cc
index 79c52d0..7aed29b 100644
--- a/model.cc
+++ b/model.cc
@@ -417,16 +417,36 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		break;
 	}
 
-	bool updated = false;
+	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
+
+	while (!work_queue.empty()) {
+		WorkQueueEntry work = work_queue.front();
+		work_queue.pop_front();
 
-	if (curr->is_read() && process_read(curr, second_part_of_rmw))
-		updated = true;
+		switch (work.type) {
+		case WORK_CHECK_CURR_ACTION: {
+			ModelAction *act = work.action;
+			bool updated = false;
+			if (act->is_read() && process_read(act, second_part_of_rmw))
+				updated = true;
 
-	if (curr->is_write() && process_write(curr))
-		updated = true;
+			if (act->is_write() && process_write(act))
+				updated = true;
 
-	if (updated)
-		resolve_release_sequences(curr->get_location());
+			if (updated)
+				work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+			break;
+		}
+		case WORK_CHECK_RELEASE_SEQ:
+			resolve_release_sequences(work.location);
+			break;
+		case WORK_CHECK_MO_EDGES:
+			/** @todo Perform follow-up mo_graph checks */
+		default:
+			ASSERT(false);
+			break;
+		}
+	}
 
 	/* Add action to list.  */
 	if (!second_part_of_rmw)
diff --git a/model.h b/model.h
index 248e164..cf1770b 100644
--- a/model.h
+++ b/model.h
@@ -17,6 +17,7 @@
 #include "action.h"
 #include "clockvector.h"
 #include "hashtable.h"
+#include "workqueue.h"
 
 /* Forward declaration */
 class NodeStack;