From e6789461057e3395ba78575b85c114b553f4ed19 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 6 Mar 2013 18:40:34 -0800 Subject: [PATCH] model, nodestack: bugfix - retain UNINIT actions across executions Previously, we were allocating UNINIT actions as snapshotting memory, just for ease of use. But because they may not immediately trigger a bug (if they are a valid read-from), such actions must have a longer lifetime - in fact, a lifetime similar to normal ModelActions. So, we stash them in NodeStack alongside normal actions. Also, improve a few ASSERT()'s and clarify a push_front() vs. push_back() (the list is empty, so it doesn't matter; but it follows the style of the rest of the lists to use push_front() here). --- model.cc | 25 +++++++++++++++++-------- model.h | 2 +- nodestack.cc | 3 +++ nodestack.h | 7 +++++++ 4 files changed, 28 insertions(+), 9 deletions(-) diff --git a/model.cc b/model.cc index 55d5d0d..d2a2c74 100644 --- a/model.cc +++ b/model.cc @@ -1384,6 +1384,8 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf) { ASSERT(rf); + ASSERT(rf->is_write()); + act->set_read_from(rf); if (act->is_acquire()) { rel_heads_list_t release_heads; @@ -2370,9 +2372,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int uninit_id = -1; action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); if (list->empty() && act->is_atomic_var()) { - uninit = new_uninitialized_action(act->get_location()); + uninit = get_uninitialized_action(act); uninit_id = id_to_int(uninit->get_tid()); - list->push_back(uninit); + list->push_front(uninit); } list->push_back(act); @@ -2813,14 +2815,21 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri } /** - * @brief Create a new action representing an uninitialized atomic - * @param location The memory location of the atomic object - * @return A pointer to a new ModelAction + * @brief Get an action representing an uninitialized atomic + * + * This function may create a new one or try to retrieve one from the NodeStack + * + * @param curr The current action, which prompts the creation of an UNINIT action + * @return A pointer to the UNINIT ModelAction */ -ModelAction * ModelChecker::new_uninitialized_action(void *location) const +ModelAction * ModelChecker::get_uninitialized_action(const ModelAction *curr) const { - ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction)); - act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread); + Node *node = curr->get_node(); + ModelAction *act = node->get_uninit_action(); + if (!act) { + act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), 0, model_thread); + node->set_uninit_action(act); + } act->create_cv(NULL); return act; } diff --git a/model.h b/model.h index 71b8b7a..ae9706b 100644 --- a/model.h +++ b/model.h @@ -209,7 +209,7 @@ private: bool resolve_release_sequences(void *location, work_queue_t *work_queue); void add_future_value(const ModelAction *writer, ModelAction *reader); - ModelAction * new_uninitialized_action(void *location) const; + ModelAction * get_uninitialized_action(const ModelAction *curr) const; ModelAction *diverge; ModelAction *earliest_diverge; diff --git a/nodestack.cc b/nodestack.cc index dbc6307..c757af2 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -27,6 +27,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : read_from_status(READ_FROM_PAST), action(act), + uninit_action(NULL), parent(par), num_threads(nthreads), explored_children(num_threads), @@ -140,6 +141,8 @@ void Node::update_yield(Scheduler * scheduler) { Node::~Node() { delete action; + if (uninit_action) + delete uninit_action; if (enabled_array) model_free(enabled_array); if (yield_data) diff --git a/nodestack.h b/nodestack.h index 0a94225..8ad329e 100644 --- a/nodestack.h +++ b/nodestack.h @@ -64,6 +64,9 @@ public: enabled_type_t enabled_status(thread_id_t tid) const; ModelAction * get_action() const { return action; } + void set_uninit_action(ModelAction *act) { uninit_action = act; } + ModelAction * get_uninit_action() const { return uninit_action; } + bool has_priority(thread_id_t tid) const; void update_yield(Scheduler *); bool has_priority_over(thread_id_t tid, thread_id_t tid2) const; @@ -124,6 +127,10 @@ private: read_from_type_t read_from_status; ModelAction * const action; + + /** @brief ATOMIC_UNINIT action which was created at this Node */ + ModelAction *uninit_action; + Node * const parent; const int num_threads; std::vector< bool, ModelAlloc > explored_children; -- 2.34.1