execution: move execution number back to ModelChecker class

diff --git a/execution.cc b/execution.cc
index f0288d2e7de1eb2d23bc32c95a3c01fb8c7d1683..c09f74b4cbef071927c1d284c1a838e513fc7288 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -4,6 +4,7 @@
 #include <new>
 #include <stdarg.h>
 
 #include <new>
 #include <stdarg.h>
 

+#include "model.h"

 #include "execution.h"
 #include "action.h"
 #include "nodestack.h"
 #include "execution.h"
 #include "action.h"
 #include "nodestack.h"


@@ -56,7 +57,11 @@ struct model_snapshot_members {
 };
 
 /** @brief Constructor */
 };
 
 /** @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()),
        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()),
        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());
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());


@@ -104,6 +108,11 @@ ModelExecution::~ModelExecution()
        delete priv;
 }
 
        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);
 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];
 {
 #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);
        mo_graph->dumpGraphToFile(buffername);

-       sprintf(buffername, "graph%04u", execution_number);
+       sprintf(buffername, "graph%04u", get_execution_number());

        dumpGraph(buffername);
 #endif
 
        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");
        if (isfeasibleprefix()) {
                if (scheduler->all_threads_sleeping())
                        model_print(" SLEEP-SET REDUNDANT");

diff --git a/execution.h b/execution.h
index 0f1e8aed1e243dc3a05d4b7fa666e33fca400c71..616a47cb47a4e34c182359e0217724b2808e59ad 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -60,7 +60,10 @@ struct release_seq {
 /** @brief The central structure for model-checking */
 class ModelExecution {
 public:
 /** @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);
        ~ModelExecution();
 
        Thread * take_step(ModelAction *curr);


@@ -110,10 +113,12 @@ public:
 
        action_list_t * get_action_trace() const { return action_trace; }
 
 
        action_list_t * get_action_trace() const { return action_trace; }
 

-       void increment_execution_number() { execution_number++; }
-

        MEMALLOC
 private:
        MEMALLOC
 private:

+       int get_execution_number() const;
+
+       ModelChecker *model;
+

        const model_params * const params;
 
        /** The scheduler to use: tracks the running/ready Threads */
        const model_params * const params;
 
        /** The scheduler to use: tracks the running/ready Threads */


@@ -231,8 +236,6 @@ private:
         */
        CycleGraph * const mo_graph;
 
         */
        CycleGraph * const mo_graph;
 

-       int execution_number;
-

        Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 
        Thread * action_select_next_thread(const ModelAction *curr) const;
 };
 

diff --git a/model.cc b/model.cc
index 48fa28acb71cf1b8d49112df717d2ac460dc2e9b..089d88d11ca32c6a5cdaef4e41a4ed886285bf89 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()),
        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()
        diverge(NULL),
        earliest_diverge(NULL),
        trace_analyses()


@@ -319,7 +320,8 @@ bool ModelChecker::next_execution()
                diverge->print();
        }
 
                diverge->print();
        }
 

-       execution->increment_execution_number();
+       execution_number++;
+

        reset_to_initial_state();
        return true;
 }
        reset_to_initial_state();
        return true;
 }

diff --git a/model.h b/model.h
index 7d84f60112c5ef26b8c54cf9e139f016fc05df7b..89d089d1051aafbcd95ae6cd4961c23f764be739 100644 (file)
--- a/model.h
+++ b/model.h
@@ -52,6 +52,8 @@ public:
 
        const ModelExecution * get_execution() const { return execution; }
 
 
        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;
 
        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;
 
        NodeStack * const node_stack;
        ModelExecution *execution;
 

+       int execution_number;
+

        void execute_sleep_set();
 
        bool next_execution();
        void execute_sleep_set();
 
        bool next_execution();