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).

diff --git a/model.cc b/model.cc
index 55d5d0d43cfab46bac7a4d8e51987231526f6c33..d2a2c744bea23c0462db61861a6be583f2d50cef 100644 (file)
--- 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 71b8b7ac0b97b2dcf4990de667f2418f29c41d94..ae9706b124067e18e5098e0fbd7e7859fce05d73 100644 (file)
--- 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 dbc630739473bfa2fd0dbd44717ea2873c3c3bfd..c757af25f647339fe7ef590ad1eb989271aff222 100644 (file)
--- 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 0a9422572eb0c4bd3ae6ce18b96757c57281a29f..8ad329eeaf04f09eb4037c6d9dc6931e8cc1524a 100644 (file)
--- 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<bool> > explored_children;