From 81246ffc197637d7d8c2c42855faee9c4c8ad2ca Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 14 Sep 2012 09:46:56 -0700
Subject: [PATCH] workqueue: add work queue structures

---
 workqueue.h | 107 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 107 insertions(+)
 create mode 100644 workqueue.h

diff --git a/workqueue.h b/workqueue.h
new file mode 100644
index 0000000..71067bb
--- /dev/null
+++ b/workqueue.h
@@ -0,0 +1,107 @@
+/**
+ * @file workqueue.h
+ * @brief Provides structures for queueing ModelChecker actions to be taken
+ */
+
+#ifndef __WORKQUEUE_H__
+#define __WORKQUEUE_H__
+
+#include <list>
+#include "mymemory.h"
+
+class ModelAction;
+
+typedef enum {
+	WORK_NONE = 0,           /**< No work to be done */
+	WORK_CHECK_CURR_ACTION,  /**< Check the current action; used for the
+	                              first action of the work loop */
+	WORK_CHECK_RELEASE_SEQ,  /**< Check if any pending release sequences
+	                              are resolved */
+	WORK_CHECK_MO_EDGES,     /**< Check if new mo_graph edges can be added */
+} model_work_t;
+
+/**
+ */
+class WorkQueueEntry {
+ public:
+	/** @brief Type of work queue entry */
+	model_work_t type;
+
+	/**
+	 * @brief Object affected
+	 * @see CheckRelSeqWorkEntry
+	 */
+	void *location;
+
+	/**
+	 * @brief The ModelAction to work on
+	 * @see MOEdgeWorkEntry
+	 */
+	ModelAction *action;
+};
+
+/**
+ * @brief Work: perform initial promise, mo_graph checks on the current action
+ *
+ * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
+ * that is currently being explored. The current ModelAction (@a action) is the
+ * only relevant parameter to this entry.
+ */
+class CheckCurrWorkEntry : public WorkQueueEntry {
+ public:
+	/**
+	 * @brief Constructor for a "check current action" work entry
+	 * @param curr The current action
+	 */
+	CheckCurrWorkEntry(ModelAction *curr) {
+		type = WORK_CHECK_CURR_ACTION;
+		location = NULL;
+		action = curr;
+	}
+};
+
+/**
+ * @brief Work: check an object location for resolved release sequences
+ *
+ * This WorkQueueEntry checks synchronization and the mo_graph for resolution
+ * of any release sequences. The object @a location is the only relevant
+ * parameter to this entry.
+ */
+class CheckRelSeqWorkEntry : public WorkQueueEntry {
+ public:
+	/**
+	 * @brief Constructor for a "check release sequences" work entry
+	 * @param l The location which must be checked for release sequences
+	 */
+	CheckRelSeqWorkEntry(void *l) {
+		type = WORK_CHECK_RELEASE_SEQ;
+		location = l;
+		action = NULL;
+	}
+};
+
+/**
+ * @brief Work: check a ModelAction for new mo_graph edges
+ *
+ * This WorkQueueEntry checks for new mo_graph edges for a particular
+ * ModelAction (e.g., that was just generated or that updated its
+ * synchronization). The ModelAction @a action is the only relevant parameter
+ * to this entry.
+ */
+class MOEdgeWorkEntry : public WorkQueueEntry {
+ public:
+	/**
+	 * @brief Constructor for a mo_edge work entry
+	 * @param updated The ModelAction which was updated, triggering this work
+	 */
+	MOEdgeWorkEntry(ModelAction *updated) {
+		type = WORK_CHECK_MO_EDGES;
+		location = NULL;
+		action = updated;
+	}
+};
+
+/** @brief typedef for the work queue type */
+typedef std::list< WorkQueueEntry, MyAlloc<WorkQueueEntry> > work_queue_t;
+
+#endif /* __WORKQUEUE_H__ */
-- 
2.34.1