model: fixup "initialized" check in build_reads_from_past()

Some... (TODO: finish message here)

diff --git a/model.cc b/model.cc
index 4cfc0efddd0a491911404454347c0d136960aad5..81679e87ae56f5c3cad43abc525e6365546f54ed 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -370,6 +370,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 
        /* 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;
 
        for (i = 0; i < thrd_lists->size(); i++) {
                action_list_t *list = &(*thrd_lists)[i];
@@ -389,6 +393,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        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 */
@@ -399,6 +408,9 @@ 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");