From: Brian Norris Date: Fri, 7 Sep 2012 19:58:06 +0000 (-0700) Subject: model: group snapshottable ModelChecker members in struct X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=9cbe08c1b6d700355c43af838dc69799b72b38f3;hp=8c83f796d2930427478e603d64e8410707011007 model: group snapshottable ModelChecker members in struct These items shouldn't be reset individually, but rather should be grouped together and allocated on the snapshotting heap. This puts us a step closer to utilizing partial rollback within executions. --- diff --git a/model.cc b/model.cc index 811cf825..43530fe1 100644 --- a/model.cc +++ b/model.cc @@ -20,14 +20,9 @@ ModelChecker *model; ModelChecker::ModelChecker(struct model_params params) : /* Initialize default scheduler */ scheduler(new Scheduler()), - /* First thread created will have id INITIAL_THREAD_ID */ - next_thread_id(INITIAL_THREAD_ID), - used_sequence_numbers(0), num_executions(0), params(params), - current_action(NULL), diverge(NULL), - nextThread(NULL), action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), @@ -36,11 +31,14 @@ ModelChecker::ModelChecker(struct model_params params) : lazy_sync_with_release(new HashTable, uintptr_t, 4>()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), - next_backtrack(NULL), mo_graph(new CycleGraph()), failed_promise(false), asserted(false) { + /* Allocate this "size" on the snapshotting heap */ + priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); + /* First thread created will have id INITIAL_THREAD_ID */ + priv->next_thread_id = INITIAL_THREAD_ID; } /** @brief Destructor */ @@ -74,11 +72,6 @@ void ModelChecker::reset_to_initial_state() { DEBUG("+++ Resetting to initial state +++\n"); node_stack->reset_execution(); - current_action = NULL; - next_thread_id = INITIAL_THREAD_ID; - used_sequence_numbers = 0; - nextThread = NULL; - next_backtrack = NULL; failed_promise = false; reset_asserted(); snapshotObject->backTrackBeforeStep(0); @@ -87,19 +80,19 @@ void ModelChecker::reset_to_initial_state() /** @returns a thread ID for a new Thread */ thread_id_t ModelChecker::get_next_id() { - return next_thread_id++; + return priv->next_thread_id++; } /** @returns the number of user threads created during this execution */ int ModelChecker::get_num_threads() { - return next_thread_id; + return priv->next_thread_id; } /** @returns a sequence number for a new ModelAction */ modelclock_t ModelChecker::get_next_seq_num() { - return ++used_sequence_numbers; + return ++priv->used_sequence_numbers; } /** @@ -222,8 +215,8 @@ void ModelChecker::set_backtracking(ModelAction *act) return; /* Cache the latest backtracking point */ - if (!next_backtrack || *prev > *next_backtrack) - next_backtrack = prev; + if (!priv->next_backtrack || *prev > *priv->next_backtrack) + priv->next_backtrack = prev; /* If this is a new backtracking point, mark the tree */ if (!node->set_backtrack(t->get_id())) @@ -243,8 +236,8 @@ void ModelChecker::set_backtracking(ModelAction *act) */ ModelAction * ModelChecker::get_next_backtrack() { - ModelAction *next = next_backtrack; - next_backtrack = NULL; + ModelAction *next = priv->next_backtrack; + priv->next_backtrack = NULL; return next; } @@ -362,8 +355,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!parnode->backtrack_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || !currnode->promise_empty()) - if (!next_backtrack || *curr > *next_backtrack) - next_backtrack = curr; + if (!priv->next_backtrack || *curr > *priv->next_backtrack) + priv->next_backtrack = curr; set_backtracking(curr); @@ -531,8 +524,8 @@ bool ModelChecker::w_modification_order(ModelAction *curr) that read could potentially read from our write. */ if (act->get_node()->add_future_value(curr->get_value()) && - (!next_backtrack || *act > *next_backtrack)) - next_backtrack = act; + (!priv->next_backtrack || *act > *priv->next_backtrack)) + priv->next_backtrack = act; } } } @@ -748,7 +741,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act) std::vector *vec = obj_thrd_map->get_safe_ptr(act->get_location()); if (tid >= (int)vec->size()) - vec->resize(next_thread_id); + vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); if ((int)thrd_last_action->size() <= tid) @@ -1009,16 +1002,16 @@ bool ModelChecker::take_step() { curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { - ASSERT(current_action); - nextThread = check_current_action(current_action); - current_action = NULL; + ASSERT(priv->current_action); + priv->nextThread = check_current_action(priv->current_action); + priv->current_action = NULL; if (!curr->is_blocked() && !curr->is_complete()) scheduler->add_thread(curr); } else { ASSERT(false); } } - next = scheduler->next_thread(nextThread); + next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) diff --git a/model.h b/model.h index 74e3b068..9762eb0c 100644 --- a/model.h +++ b/model.h @@ -30,6 +30,17 @@ class Promise; struct model_params { }; +/** + * Structure for holding small ModelChecker members that should be snapshotted + */ +struct model_snapshot_members { + ModelAction *current_action; + int next_thread_id; + modelclock_t used_sequence_numbers; + Thread *nextThread; + ModelAction *next_backtrack; +}; + /** @brief The central structure for model-checking */ class ModelChecker { public: @@ -74,8 +85,6 @@ private: bool has_asserted() {return asserted;} void reset_asserted() {asserted=false;} - int next_thread_id; - modelclock_t used_sequence_numbers; int num_executions; const model_params params; @@ -86,7 +95,7 @@ private: * data between them. * @param act The ModelAction created by the user-thread action */ - void set_current_action(ModelAction *act) { current_action = act; } + void set_current_action(ModelAction *act) { priv->current_action = act; } Thread * check_current_action(ModelAction *curr); bool take_step(); @@ -111,9 +120,7 @@ private: std::vector *release_heads) const; bool resolve_release_sequences(void *location); - ModelAction *current_action; ModelAction *diverge; - Thread *nextThread; ucontext_t system_context; action_list_t *action_trace; @@ -137,7 +144,10 @@ private: std::vector *thrd_last_action; NodeStack *node_stack; - ModelAction *next_backtrack; + + /** Private data members that should be snapshotted. They are grouped + * together for efficiency and maintainability. */ + struct model_snapshot_members *priv; /** * @brief The modification order graph