execution: move execution number back to ModelChecker class
authorBrian Norris <banorris@uci.edu>
Tue, 16 Apr 2013 03:08:41 +0000 (20:08 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 16 Apr 2013 18:38:01 +0000 (11:38 -0700)
execution.cc
execution.h
model.cc
model.h

index f0288d2..c09f74b 100644 (file)
@@ -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");
index 0f1e8ae..616a47c 100644 (file)
@@ -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;
 };
 
index 48fa28a..089d88d 100644 (file)
--- 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 (file)
--- 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();