From 564d990b2b4557bd5b5a9fa562bb2fff85c12078 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 12 Jul 2012 18:58:18 -0700 Subject: [PATCH] model: fixup "initialized" check in build_reads_from_past() Some... (TODO: finish message here) --- model.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/model.cc b/model.cc index 4cfc0efd..81679e87 100644 --- 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"); -- 2.34.1