From 495dd308fe91920ea85719d8380d9cf28ee85274 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 5 Oct 2012 19:18:13 -0700 Subject: [PATCH] model: add special model-checker Thread to ModelChecker Note the change in take_step(), so that we base the "current thread" off of the provided ModelAction, rather than thread_current() (i.e., the Scheduler). This is because the Scheduler will never run the model-checker thread. --- model.cc | 6 +++++- model.h | 4 ++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index c5e41ab..c1818ad 100644 --- a/model.cc +++ b/model.cc @@ -47,6 +47,10 @@ ModelChecker::ModelChecker(struct model_params params) : priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); /* First thread created will have id INITIAL_THREAD_ID */ priv->next_thread_id = INITIAL_THREAD_ID; + + /* Initialize a model-checker thread, for special ModelActions */ + model_thread = new Thread(get_next_id()); + thread_map->put(id_to_int(model_thread->get_id()), model_thread); } /** @brief Destructor */ @@ -1944,7 +1948,7 @@ bool ModelChecker::take_step() { if (has_asserted()) return false; - Thread *curr = thread_current(); + Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL; if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); diff --git a/model.h b/model.h index 4032ef1..68831b8 100644 --- a/model.h +++ b/model.h @@ -203,6 +203,10 @@ private: * together for efficiency and maintainability. */ struct model_snapshot_members *priv; + /** A special model-checker Thread; used for associating with + * model-checker-related ModelAcitons */ + Thread *model_thread; + /** * @brief The modification order graph * -- 2.34.1