add our names

[cdsspec-compiler.git] / model.cc

diff --git a/model.cc b/model.cc
index 0cc20794d61f1217163743de2f3147459d5d1466..d9ff365e6808494c4c667272f7dd9b7c4f9d5a5f 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++) {
@@ -1831,7 +1834,18 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
-                       if (act->is_write() && !act->equals(rf) && act != curr) {
+                       /* Skip curr */
+                       if (act == curr)
+                               continue;
+                       /* Don't want to add reflexive edges on 'rf' */
+                       if (act->equals(rf)) {
+                               if (act->happens_before(curr))
+                                       break;
+                               else
+                                       continue;
+                       }
+
+                       if (act->is_write()) {
                                /* C++, Section 29.3 statement 5 */
                                if (curr->is_seqcst() && last_sc_fence_thread_local &&
                                                *act < *last_sc_fence_thread_local) {
@@ -1852,15 +1866,19 @@ 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. Don't consider reflexively.
+                        * before" curr
                         */
-                       if (act->happens_before(curr) && act != curr) {
+                       if (act->happens_before(curr)) {
                                if (act->is_write()) {
-                                       if (!act->equals(rf)) {
-                                               added = mo_graph->addEdge(act, rf) || added;
-                                       }
+                                       added = mo_graph->addEdge(act, rf) || added;
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        const Promise *prevrf_promise = act->get_reads_from_promise();
@@ -2454,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;
 }
@@ -3021,6 +3042,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
        DBG();
        Thread *old = thread_current();
+       scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());
        old->set_pending(act);
        if (Thread::swap(old, &system_context) < 0) {