From: Brian Norris Date: Tue, 16 Apr 2013 03:08:41 +0000 (-0700) Subject: execution: move execution number back to ModelChecker class X-Git-Tag: oopsla2013~61 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7bfea91f33595532cf618fe3d090e8021f578795;hp=f9fe0087091f88deeb814d0768eecdfb1b51a94d;p=model-checker.git execution: move execution number back to ModelChecker class --- diff --git a/execution.cc b/execution.cc index f0288d2..c09f74b 100644 --- a/execution.cc +++ b/execution.cc @@ -4,6 +4,7 @@ #include #include +#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()), 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 * 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(¶ms, scheduler, node_stack)), + execution(new ModelExecution(this, ¶ms, 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();