add test case...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a03ea46224f1d7a4d10f64927b9df9d385eeb21e..3ed2fb24971b3c42908b1b59f243a54a8b786500 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1128,6 +1128,7 @@ bool ModelChecker::process_fence(ModelAction *curr)
         *   use in later synchronization
         * fence-acquire (this function): search for hypothetical release
         *   sequences
+        * fence-seq-cst: MO constraints formed in {r,w}_modification_order
         */
        bool updated = false;
        if (curr->is_acquire()) {
@@ -1812,6 +1813,9 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 
        /* Last SC fence in the current thread */
        ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+       ModelAction *last_sc_write = NULL;
+       if (curr->is_seqcst())
+               last_sc_write = get_last_seq_cst_write(curr);
 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
@@ -1863,6 +1867,12 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                                }
                        }
 
+                       /* C++, Section 29.3 statement 3 (second subpoint) */
+                       if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
+                               added = mo_graph->addEdge(act, rf) || added;
+                               break;
+                       }
+
                        /*
                         * Include at most one act per-thread that "happens
                         * before" curr
@@ -2463,8 +2473,11 @@ ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
        action_list_t *list = get_safe_ptr_action(obj_map, location);
        /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
        action_list_t::reverse_iterator rit;
-       for (rit = list->rbegin(); rit != list->rend(); rit++)
-               if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
+       for (rit = list->rbegin(); (*rit) != curr; rit++)
+               ;
+       rit++; /* Skip past curr */
+       for ( ; rit != list->rend(); rit++)
+               if ((*rit)->is_write() && (*rit)->is_seqcst())
                        return *rit;
        return NULL;
 }