model: bugfix - missing SC mo_graph edge
authorBrian Norris <banorris@uci.edu>
Tue, 12 Mar 2013 17:47:41 +0000 (10:47 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 12 Mar 2013 17:54:15 +0000 (10:54 -0700)
We must enforce a rule such as the following, derived from C++ Section
29.3, statement 3 (second subpoint):

if is_store(X) && is_seq_cst(X) && is_store(Y) && is_load(Z) &&
   is_seq_cst(Z) &&
   X --sc-> Z && Y --rf-> Z && X != Y
then
   X --mo-> Y

This has been checked (via manual test-case) to fix a bug which allowed
an inconsistent mo/sc/rf relationship.

model.cc

index a03ea46..d9ff365 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1812,6 +1812,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 +1866,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 +2472,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;
 }