execution: make structure snapshotting

[model-checker.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 0006c66c70a3acf89433bfd4013e03ad3f5b3e1c..c09f74b4cbef071927c1d284c1a838e513fc7288 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -4,19 +4,17 @@
 #include <new>
 #include <stdarg.h>
 
-#include "execution.h"
 #include "model.h"
+#include "execution.h"
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
-#include "snapshot-interface.h"
 #include "common.h"
 #include "clockvector.h"
 #include "cyclegraph.h"
 #include "promise.h"
 #include "datarace.h"
 #include "threads-model.h"
-#include "output.h"
 #include "bugmessage.h"
 
 #define INITIAL_THREAD_ID      0
@@ -31,7 +29,6 @@ struct model_snapshot_members {
                used_sequence_numbers(0),
                next_backtrack(NULL),
                bugs(),
-               stats(),
                failed_promise(false),
                too_many_reads(false),
                no_valid_reads(false),
@@ -49,7 +46,6 @@ struct model_snapshot_members {
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;
        SnapVector<bug_message *> bugs;
-       struct execution_stats stats;
        bool failed_promise;
        bool too_many_reads;
        bool no_valid_reads;
@@ -61,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()),
@@ -76,12 +76,12 @@ 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());
        thread_map->put(id_to_int(model_thread->get_id()), model_thread);
+       scheduler->register_engine(this);
 }
 
 /** @brief Destructor */
@@ -108,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);
@@ -128,7 +133,8 @@ static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, Sn
        return tmp;
 }
 
-action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) {
+action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
+{
        SnapVector<action_list_t> *wrv=obj_thrd_map->get(obj);
        if (wrv==NULL)
                return NULL;
@@ -615,7 +621,7 @@ bool ModelExecution::process_read(ModelAction *curr)
                case READ_FROM_FUTURE: {
                        /* Read from future value */
                        struct future_value fv = node->get_future_value();
-                       Promise *promise = new Promise(curr, fv);
+                       Promise *promise = new Promise(this, curr, fv);
                        curr->set_read_from_promise(promise);
                        promises->push_back(promise);
                        mo_graph->startChanges();
@@ -910,7 +916,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
        case THREAD_CREATE: {
                thrd_t *thrd = (thrd_t *)curr->get_location();
                struct thread_params *params = (struct thread_params *)curr->get_value();
-               Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
+               Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
                add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */
@@ -2646,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");