From c2d7fa973e562c194eb732d8dc58ab7659b7a2ee Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Sat, 3 Nov 2012 15:24:54 -0700 Subject: [PATCH] annoying bug... Optimization was originally intended for the following insight: if you have a unresolved read and a write w that is mod ordered after whatever that read sees, then any writes that are mo past w should not send their future values back to the unresolved read. So we begin by looking for operations that happen after the unresolved read and if they are a write we have our w, and if they are a read then its reads_from is our w. The case I missed was we don't want to consider the write that the read we want to send the value to is currently reading... It won't cause a mo problem because it will be gone if we send a future value back to that read. --- model.cc | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 1e730d7..da982d0 100644 --- a/model.cc +++ b/model.cc @@ -1388,7 +1388,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re { std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); unsigned int i; - /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { const ModelAction *write_after_read = NULL; @@ -1403,7 +1402,7 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re break; else if (act->is_write()) write_after_read = act; - else if (act->is_read()&&act->get_reads_from()!=NULL) { + else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) { write_after_read = act->get_reads_from(); } } @@ -1411,7 +1410,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer)) return false; } - return true; } -- 2.34.1