model: record last fence-release from each thread

diff --git a/model.cc b/model.cc
index 82b90601048845f32a9af77d57e938e8fb11450f..f96249fcb9cf9ceeb9eb0b97b5a13c9b74b96b60 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -91,6 +91,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
        pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
        thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
+       thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
        node_stack(new NodeStack()),
        priv(new struct model_snapshot_members()),
        mo_graph(new CycleGraph())
@@ -120,6 +121,7 @@ ModelChecker::~ModelChecker()
        delete pending_rel_seqs;
 
        delete thrd_last_action;
+       delete thrd_last_fence_release;
        delete node_stack;
        delete scheduler;
        delete mo_graph;
@@ -1024,6 +1026,10 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 
                /* Always compute new clock vector */
                newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+               /* Assign most recent release fence */
+               newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
                /*
                 * Perform one-time actions when pushing new ModelAction onto
                 * NodeStack
@@ -1998,6 +2004,12 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
                thrd_last_action->resize(get_num_threads());
        (*thrd_last_action)[tid] = act;
 
+       if (act->is_fence() && act->is_release()) {
+               if ((int)thrd_last_fence_release->size() <= tid)
+                       thrd_last_fence_release->resize(get_num_threads());
+               (*thrd_last_fence_release)[tid] = act;
+       }
+
        if (act->is_wait()) {
                void *mutex_loc=(void *) act->get_value();
                get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
@@ -2023,6 +2035,20 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
                return NULL;
 }
 
+/**
+ * @brief Get the last fence release performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last fence release in the thread, if one exists; NULL otherwise
+ */
+ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
+{
+       int threadid = id_to_int(tid);
+       if (threadid < (int)thrd_last_fence_release->size())
+               return (*thrd_last_fence_release)[id_to_int(tid)];
+       else
+               return NULL;
+}
+
 /**
  * Gets the last memory_order_seq_cst write (in the total global sequence)
  * performed on a particular object (i.e., memory location), not including the

diff --git a/model.h b/model.h
index 11afba9f66129eb18f85ec34cd29160c4c751622..fd99700a01c35f77ff2d87445ee228b71ae69de5 100644 (file)
--- a/model.h
+++ b/model.h
@@ -170,6 +170,7 @@ private:
        void check_curr_backtracking(ModelAction * curr);
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid) const;
+       ModelAction * get_last_fence_release(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
        ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
        ModelAction * get_last_unlock(ModelAction *curr) const;
@@ -213,6 +214,7 @@ private:
        std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > *pending_rel_seqs;
 
        std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_action;
+       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_fence_release;
        NodeStack *node_stack;
 
        /** Private data members that should be snapshotted. They are grouped