/**
* Processes a read or rmw model action.
* @param curr is the read model action to process.
- * @param th is the thread
* @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
* @return True if processing this read updates the mo_graph.
*/
-bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
+bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+{
uint64_t value;
bool updated = false;
while (true) {
Promise *valuepromise = new Promise(curr, value, expiration);
promises->push_back(valuepromise);
}
- th->set_return_value(value);
+ get_thread(curr)->set_return_value(value);
return updated;
}
}
+/**
+ * Process a write ModelAction
+ * @param curr The ModelAction to process
+ * @return True if the mo_graph was updated or promises were resolved
+ */
+bool ModelChecker::process_write(ModelAction *curr)
+{
+ bool updated_mod_order = w_modification_order(curr);
+ bool updated_promises = resolve_promises(curr);
+
+ if (promises->size() == 0) {
+ for (unsigned int i = 0; i<futurevalues->size(); i++) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+ (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
+ priv->next_backtrack = pfv.act;
+ }
+ futurevalues->resize(0);
+ }
+
+ mo_graph->commitChanges();
+ get_thread(curr)->set_return_value(VALUE_NONE);
+ return updated_mod_order || updated_promises;
+}
+
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
break;
}
- bool updated = false;
+ work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
- if (curr->is_read()) {
- updated = process_read(curr, get_thread(curr), second_part_of_rmw);
- }
+ while (!work_queue.empty()) {
+ WorkQueueEntry work = work_queue.front();
+ work_queue.pop_front();
- if (curr->is_write()) {
- bool updated_mod_order = w_modification_order(curr);
- bool updated_promises = resolve_promises(curr);
- updated = updated || updated_mod_order || updated_promises;
-
- if (promises->size()==0) {
- for (unsigned int i = 0; i<futurevalues->size(); i++) {
- struct PendingFutureValue pfv=(*futurevalues)[i];
- if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
- (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
- priv->next_backtrack = pfv.act;
- }
- futurevalues->resize(0);
- }
+ 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;
- mo_graph->commitChanges();
- get_thread(curr)->set_return_value(VALUE_NONE);
- }
+ 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, &work_queue);
+ 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)
*
* @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);
}
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) {
--- /dev/null
+/**
+ * @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__ */
projects / model-checker.git / commitdiff