From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 03:31:10 +0000 (-0800)
Subject: model: pass current action as function argument
X-Git-Tag: oopsla2013~425
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=717ddd114a51764ac33d3d86d6eeb09c7c4aee1b

model: pass current action as function argument

Diminish the use of 'priv->current_action', and instead pass it to
take_step() as an argument. At the same time, it is more obvious that we
do not need to reset priv->current_action to NULL.
---

diff --git a/model.cc b/model.cc
index 42726f0..a566831 100644
--- a/model.cc
+++ b/model.cc
@@ -298,7 +298,6 @@ void ModelChecker::execute_sleep_set()
 			thr->set_pending(priv->current_action);
 		}
 	}
-	priv->current_action = NULL;
 }
 
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
@@ -2697,15 +2696,14 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 
 /**
  * Takes the next step in the execution, if possible.
+ * @param curr The current step to take
  * @return Returns true (success) if a step was taken and false otherwise.
  */
-bool ModelChecker::take_step() {
+bool ModelChecker::take_step(ModelAction *curr)
+{
 	if (has_asserted())
 		return false;
 
-	ModelAction *curr = priv->current_action;
-	priv->current_action = NULL;
-
 	Thread *curr_thrd = get_thread(curr);
 	ASSERT(curr_thrd->get_state() == THREAD_READY);
 
@@ -2791,7 +2789,7 @@ void ModelChecker::run()
 		Thread::swap(&system_context, t);
 
 		/* Wait for all threads to complete */
-		while (take_step());
+		while (take_step(priv->current_action));
 	} while (next_execution());
 
 	print_stats();
diff --git a/model.h b/model.h
index 9b63f0f..76b2aff 100644
--- a/model.h
+++ b/model.h
@@ -159,7 +159,7 @@ private:
 	bool read_from(ModelAction *act, const ModelAction *rf);
 	bool check_action_enabled(ModelAction *curr);
 
-	bool take_step();
+	bool take_step(ModelAction *curr);
 
 	void check_recency(ModelAction *curr, const ModelAction *rf);
 	ModelAction * get_last_conflict(ModelAction *act);