model: bugfix - mo_may_allow was too restrictive

This bugfix has the same rationale as with the following commit:

commit c2d7fa973e562c194eb732d8dc58ab7659b7a2ee

We do not want the potential reader to disqualify itself from reading a
future value; previously, this was fixed only for reads (not RMW's). But
we can experience the same problem with RMW's, which are both read and
write.

So, instead of using 'act != reader' as a special case for the is_read()
case, just use it as a breaking condition in addition to

   !(reader --hb-> act)

This is really intended anyway, since our happens-before is reflexive,
whereas it is irreflexive in the specification.

diff --git a/model.cc b/model.cc
index 21cfb2d541603071afd71a432455abe1b9fad3ec..0bd8fd3e604528f164846a4bd051815eff9ae3fe 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1803,13 +1803,13 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
-                       if (!reader->happens_before(act))
+                       /* Don't disallow due to act == reader */
+                       if (!reader->happens_before(act) || reader == act)
                                break;
                        else if (act->is_write())
                                write_after_read = act;
-                       else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
+                       else if (act->is_read() && act->get_reads_from() != NULL)
                                write_after_read = act->get_reads_from();
-                       }
                }
 
                if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))