the initialized logic appears to be wrong... release/acquire pairs only

establish synchronization if the load reads the release store...  just because
all possible reads would synchronize doesn't mean that load can't fail to see them all...

diff --git a/model.cc b/model.cc
index 614b1a78559779dcdd1ba1ec382557fdb68e43aa..0bd9b61b410f7c57f2991f9446cb74847448a55e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -365,15 +365,16 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        ModelAction *last_seq_cst = NULL;
 
 
        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;

-       /* Would each action synchronize if we read from it? */
-       bool all_synch = true;
-       /* Is the may_read_from set empty? (tracked locally) */
-       bool empty = true;
+
+       if (curr->is_seqcst()) {
+               last_seq_cst = get_last_seq_cst(curr->get_location());
+               /* We have to at least see the last sequentially consistent write,
+                        so we are initialized. */
+               if (last_seq_cst != NULL)
+                       initialized = true;
+       }

 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {


@@ -395,11 +396,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        curr->print();
                                }
                                curr->get_node()->add_read_from(act);
                                        curr->print();
                                }
                                curr->get_node()->add_read_from(act);

-                               empty = false;
-
-                               if (!(act->is_release() && curr->is_acquire())
-                                               && !act->same_thread(curr))
-                                       all_synch = false;

                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */


@@ -410,14 +406,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                }
        }
 
                }
        }
 

-       if (!empty && all_synch)
-               initialized = true;
-

        if (!initialized) {
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");
        }
        if (!initialized) {
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");
        }

-
+       

        if (DBG_ENABLED() || !initialized) {
                printf("Reached read action:\n");
                curr->print();
        if (DBG_ENABLED() || !initialized) {
                printf("Reached read action:\n");
                curr->print();


@@ -425,7 +418,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }

-
+       

        ASSERT(initialized);
 }
 
        ASSERT(initialized);
 }