From 7bfea91f33595532cf618fe3d090e8021f578795 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Mon, 15 Apr 2013 20:08:41 -0700
Subject: [PATCH] execution: move execution number back to ModelChecker class

---
 execution.cc | 21 +++++++++++++++------
 execution.h  | 13 ++++++++-----
 model.cc     |  6 ++++--
 model.h      |  4 ++++
 4 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/execution.cc b/execution.cc
index f0288d2..c09f74b 100644
--- a/execution.cc
+++ b/execution.cc
@@ -4,6 +4,7 @@
 #include <new>
 #include <stdarg.h>
 
+#include "model.h"
 #include "execution.h"
 #include "action.h"
 #include "nodestack.h"
@@ -56,7 +57,11 @@ struct model_snapshot_members {
 };
 
 /** @brief Constructor */
-ModelExecution::ModelExecution(struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m,
+		struct model_params *params,
+		Scheduler *scheduler,
+		NodeStack *node_stack) :
+	model(m),
 	params(params),
 	scheduler(scheduler),
 	action_trace(new action_list_t()),
@@ -71,8 +76,7 @@ ModelExecution::ModelExecution(struct model_params *params, Scheduler *scheduler
 	thrd_last_fence_release(new SnapVector<ModelAction *>()),
 	node_stack(node_stack),
 	priv(new struct model_snapshot_members()),
-	mo_graph(new CycleGraph()),
-	execution_number(1)
+	mo_graph(new CycleGraph())
 {
 	/* Initialize a model-checker thread, for special ModelActions */
 	model_thread = new Thread(get_next_id());
@@ -104,6 +108,11 @@ ModelExecution::~ModelExecution()
 	delete priv;
 }
 
+int ModelExecution::get_execution_number() const
+{
+	return model->get_execution_number();
+}
+
 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
 {
 	action_list_t *tmp = hash->get(ptr);
@@ -2643,13 +2652,13 @@ void ModelExecution::print_summary() const
 {
 #if SUPPORT_MOD_ORDER_DUMP
 	char buffername[100];
-	sprintf(buffername, "exec%04u", execution_number);
+	sprintf(buffername, "exec%04u", get_execution_number());
 	mo_graph->dumpGraphToFile(buffername);
-	sprintf(buffername, "graph%04u", execution_number);
+	sprintf(buffername, "graph%04u", get_execution_number());
 	dumpGraph(buffername);
 #endif
 
-	model_print("Execution %d:", execution_number);
+	model_print("Execution %d:", get_execution_number());
 	if (isfeasibleprefix()) {
 		if (scheduler->all_threads_sleeping())
 			model_print(" SLEEP-SET REDUNDANT");
diff --git a/execution.h b/execution.h
index 0f1e8ae..616a47c 100644
--- a/execution.h
+++ b/execution.h
@@ -60,7 +60,10 @@ struct release_seq {
 /** @brief The central structure for model-checking */
 class ModelExecution {
 public:
-	ModelExecution(struct model_params *params, Scheduler *scheduler, NodeStack *node_stack);
+	ModelExecution(ModelChecker *m,
+			struct model_params *params,
+			Scheduler *scheduler,
+			NodeStack *node_stack);
 	~ModelExecution();
 
 	Thread * take_step(ModelAction *curr);
@@ -110,10 +113,12 @@ public:
 
 	action_list_t * get_action_trace() const { return action_trace; }
 
-	void increment_execution_number() { execution_number++; }
-
 	MEMALLOC
 private:
+	int get_execution_number() const;
+
+	ModelChecker *model;
+
 	const model_params * const params;
 
 	/** The scheduler to use: tracks the running/ready Threads */
@@ -231,8 +236,6 @@ private:
 	 */
 	CycleGraph * const mo_graph;
 
-	int execution_number;
-
 	Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 
diff --git a/model.cc b/model.cc
index 48fa28a..089d88d 100644
--- a/model.cc
+++ b/model.cc
@@ -26,7 +26,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	params(params),
 	scheduler(new Scheduler()),
 	node_stack(new NodeStack()),
-	execution(new ModelExecution(&params, scheduler, node_stack)),
+	execution(new ModelExecution(this, &params, scheduler, node_stack)),
+	execution_number(1),
 	diverge(NULL),
 	earliest_diverge(NULL),
 	trace_analyses()
@@ -319,7 +320,8 @@ bool ModelChecker::next_execution()
 		diverge->print();
 	}
 
-	execution->increment_execution_number();
+	execution_number++;
+
 	reset_to_initial_state();
 	return true;
 }
diff --git a/model.h b/model.h
index 7d84f60..89d089d 100644
--- a/model.h
+++ b/model.h
@@ -52,6 +52,8 @@ public:
 
 	const ModelExecution * get_execution() const { return execution; }
 
+	int get_execution_number() const { return execution_number; }
+
 	Thread * get_thread(thread_id_t tid) const;
 	Thread * get_thread(const ModelAction *act) const;
 
@@ -82,6 +84,8 @@ private:
 	NodeStack * const node_stack;
 	ModelExecution *execution;
 
+	int execution_number;
+
 	void execute_sleep_set();
 
 	bool next_execution();
-- 
2.34.1