model: record last fence-release from each thread

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index fc86d5c7e9955d3b5e4ccd17cc25ccc5e2e38fa6..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)),
        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())
        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 pending_rel_seqs;
 
        delete thrd_last_action;

+       delete thrd_last_fence_release;

        delete node_stack;
        delete scheduler;
        delete mo_graph;
        delete node_stack;
        delete scheduler;
        delete mo_graph;


@@ -521,6 +523,7 @@ bool ModelChecker::next_execution()
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        switch (act->get_type()) {
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        switch (act->get_type()) {

+       case ATOMIC_FENCE:

        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {
        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {


@@ -1023,6 +1026,10 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
 
                /* Always compute new clock vector */
                newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 
                /* 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
                /*
                 * Perform one-time actions when pushing new ModelAction onto
                 * NodeStack


@@ -1402,14 +1409,48 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
        bool added = false;
        ASSERT(curr->is_read());
 
        bool added = false;
        ASSERT(curr->is_read());
 

+       /* Last SC fence in the current thread */
+       ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+

        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {

+               /* Last SC fence in thread i */
+               ModelAction *last_sc_fence_thread_local = NULL;
+               if (int_to_id((int)i) != curr->get_tid())
+                       last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+
+               /* Last SC fence in thread i, before last SC fence in current thread */
+               ModelAction *last_sc_fence_thread_before = NULL;
+               if (last_sc_fence_local)
+                       last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+

                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 

+                       if (act->is_write() && act != rf && act != curr) {
+                               /* C++, Section 29.3 statement 5 */
+                               if (curr->is_seqcst() && last_sc_fence_thread_local &&
+                                               *act < *last_sc_fence_thread_local) {
+                                       mo_graph->addEdge(act, rf);
+                                       added = true;
+                               }
+                               /* C++, Section 29.3 statement 4 */
+                               else if (act->is_seqcst() && last_sc_fence_local &&
+                                               *act < *last_sc_fence_local) {
+                                       mo_graph->addEdge(act, rf);
+                                       added = true;
+                               }
+                               /* C++, Section 29.3 statement 6 */
+                               else if (last_sc_fence_thread_before &&
+                                               *act < *last_sc_fence_thread_before) {
+                                       mo_graph->addEdge(act, rf);
+                                       added = true;
+                               }
+                       }
+

                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr. Don't consider reflexively.
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr. Don't consider reflexively.


@@ -1542,8 +1583,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                }
        }
 
                }
        }
 

+       /* Last SC fence in the current thread */
+       ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+

        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {

+               /* Last SC fence in thread i, before last SC fence in current thread */
+               ModelAction *last_sc_fence_thread_before = NULL;
+               if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
+                       last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+

                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;


@@ -1570,6 +1619,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                        continue;
                        }
 
                                        continue;
                        }
 

+                       /* C++, Section 29.3 statement 7 */
+                       if (last_sc_fence_thread_before && act->is_write() &&
+                                       *act < *last_sc_fence_thread_before) {
+                               mo_graph->addEdge(act, curr);
+                               added = true;
+                       }
+

                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr


@@ -1948,6 +2004,12 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
                thrd_last_action->resize(get_num_threads());
        (*thrd_last_action)[tid] = 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);
        if (act->is_wait()) {
                void *mutex_loc=(void *) act->get_value();
                get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);


@@ -1956,10 +2018,6 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
                if (tid >= (int)vec->size())
                        vec->resize(priv->next_thread_id);
                (*vec)[tid].push_back(act);
                if (tid >= (int)vec->size())
                        vec->resize(priv->next_thread_id);
                (*vec)[tid].push_back(act);

-
-               if ((int)thrd_last_action->size() <= tid)
-                       thrd_last_action->resize(get_num_threads());
-               (*thrd_last_action)[tid] = act;

        }
 }
 
        }
 }
 


@@ -1977,6 +2035,20 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
                return NULL;
 }
 
                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
 /**
  * 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


@@ -2289,15 +2361,20 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                continue;
 
                        /* Don't consider more than one seq_cst write if we are a seq_cst read. */
                                continue;
 
                        /* Don't consider more than one seq_cst write if we are a seq_cst read. */

-                       if (!curr->is_seqcst() || (!act->is_seqcst() && (last_sc_write == NULL || !act->happens_before(last_sc_write))) || act == last_sc_write) {
-                               if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
-                                       DEBUG("Adding action to may_read_from:\n");
-                                       if (DBG_ENABLED()) {
-                                               act->print();
-                                               curr->print();
-                                       }
-                                       curr->get_node()->add_read_from(act);
+                       bool allow_read = true;
+
+                       if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+                               allow_read = false;
+                       else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
+                               allow_read = false;
+
+                       if (allow_read) {
+                               DEBUG("Adding action to may_read_from:\n");
+                               if (DBG_ENABLED()) {
+                                       act->print();
+                                       curr->print();

                                }
                                }

+                               curr->get_node()->add_read_from(act);

                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */