From 10676ed8e2c04c76d410efc9ffe4cb49b9462f57 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Sep 2012 13:08:46 -0700
Subject: [PATCH] model: check_current_action returns its 'nextThread'
To begin some code structure rearrangements, I make check_current_action()
return the 'nextThread' value as a true return value. Eventually, the
nextThread field might not be needed, and the model-checker behavior might make
more sense...
---
model.cc | 31 +++++++++++++------------------
model.h | 2 +-
2 files changed, 14 insertions(+), 19 deletions(-)
diff --git a/model.cc b/model.cc
index c306f0e..866bc94 100644
--- a/model.cc
+++ b/model.cc
@@ -244,15 +244,11 @@ ModelAction * ModelChecker::get_next_backtrack()
return next;
}
-void ModelChecker::check_current_action(void)
+Thread * ModelChecker::check_current_action(ModelAction *curr)
{
- ModelAction *curr = this->current_action;
bool already_added = false;
- this->current_action = NULL;
- if (!curr) {
- DEBUG("trying to push NULL action...\n");
- return;
- }
+
+ ASSERT(curr);
if (curr->is_rmwc() || curr->is_rmw()) {
ModelAction *tmp = process_rmw(curr);
@@ -332,16 +328,6 @@ void ModelChecker::check_current_action(void)
if (!already_added)
add_action_to_lists(curr);
- /** @todo Is there a better interface for setting the next thread rather
- than this field/convoluted approach? Perhaps like just returning
- it or something? */
-
- /* Do not split atomic actions. */
- if (curr->is_rmwr())
- nextThread = thread_current();
- else
- nextThread = get_next_replay_thread();
-
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
@@ -351,6 +337,12 @@ void ModelChecker::check_current_action(void)
next_backtrack = curr;
set_backtracking(curr);
+
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr())
+ return thread_current();
+ else
+ return get_next_replay_thread();
}
/** @returns whether the current partial trace is feasible. */
@@ -962,7 +954,10 @@ bool ModelChecker::take_step() {
curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
- check_current_action();
+ if (current_action) {
+ nextThread = check_current_action(current_action);
+ current_action = NULL;
+ }
scheduler->add_thread(curr);
} else if (curr->get_state() == THREAD_RUNNING) {
/* Stopped while running; i.e., completed */
diff --git a/model.h b/model.h
index bc827fa..e55863d 100644
--- a/model.h
+++ b/model.h
@@ -82,7 +82,7 @@ private:
* @param act The ModelAction created by the user-thread action
*/
void set_current_action(ModelAction *act) { current_action = act; }
- void check_current_action();
+ Thread * check_current_action(ModelAction *curr);
bool take_step();
--
2.34.1