From 517125229f0d6faec89c3937753ed97d686ef696 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 13 Dec 2012 00:13:08 -0800 Subject: [PATCH] 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. --- model.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 21cfb2d..0bd8fd3 100644 --- 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)) -- 2.34.1