From f82a95581e303d67ea57de4ae9e888be10558866 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 14 Sep 2012 09:52:49 -0700 Subject: [PATCH] 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. --- model.cc | 34 +++++++++++++++++++++++++++------- model.h | 1 + 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/model.cc b/model.cc index 79c52d01..7aed29b6 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 248e1648..cf1770b7 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; -- 2.34.1