annoying bug... Optimization was originally intended for the following insight:
authorBrian Demsky <bdemsky@uci.edu>
Sat, 3 Nov 2012 22:24:54 +0000 (15:24 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Sat, 3 Nov 2012 22:24:54 +0000 (15:24 -0700)
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

index 1e730d7..da982d0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1388,7 +1388,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 {
        std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
        unsigned int i;
 {
        std::vector<action_list_t> *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;
        /* 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;
                                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();
                        }
                }
                                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;
        }
                if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
                        return false;
        }
-
        return true;
 }
 
        return true;
 }