model: only include the most recent seq_cst write in may_read_from

diff --git a/model.cc b/model.cc
index 8e6e1b86035e4d27243508a386edbdfe4f648f8f..4cfc0efddd0a491911404454347c0d136960aad5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -363,6 +363,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ASSERT(curr->is_read());
 
 
        ASSERT(curr->is_read());
 

+       ModelAction *last_seq_cst = NULL;
+
+       if (curr->is_seqcst())
+               last_seq_cst = get_last_seq_cst(curr->get_location());
+

        /* Track whether this object has been initialized */
        bool initialized = false;
 
        /* Track whether this object has been initialized */
        bool initialized = false;
 


@@ -376,12 +381,15 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                        if (!act->is_write())
                                continue;
 
                        if (!act->is_write())
                                continue;
 

-                       DEBUG("Adding action to may_read_from:\n");
-                       if (DBG_ENABLED()) {
-                               act->print();
-                               curr->print();
+                       /* Don't consider more than one seq_cst write */
+                       if (!act->is_seqcst() || act == last_seq_cst) {
+                               DEBUG("Adding action to may_read_from:\n");
+                               if (DBG_ENABLED()) {
+                                       act->print();
+                                       curr->print();
+                               }
+                               curr->get_node()->add_read_from(act);

                        }
                        }

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

 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {
 
                        /* Include at most one act per-thread that "happens before" curr */
                        if (act->happens_before(curr)) {