model: add seq-cst fence rules

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index d6ebfe5abc9f4e60920f9b08bed0112746c3afce..cd20321bb8c76a4c76adb1b43c29d8c2c7e6b4b5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -521,6 +521,7 @@ bool ModelChecker::next_execution()
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 {
        switch (act->get_type()) {
+       case ATOMIC_FENCE:
        case ATOMIC_READ:
        case ATOMIC_WRITE:
        case ATOMIC_RMW: {
@@ -1402,14 +1403,48 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
        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++) {
+               /* 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;
 
+                       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.
@@ -1542,8 +1577,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++) {
+               /* 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;
@@ -1570,6 +1613,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                        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