model: bugfix - mo_may_allow was too restrictive
authorBrian Norris <banorris@uci.edu>
Thu, 13 Dec 2012 08:13:08 +0000 (00:13 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 13 Dec 2012 08:29:44 +0000 (00:29 -0800)
commit517125229f0d6faec89c3937753ed97d686ef696
tree66f6d225c4c743d30de24c76d9a64264b604bd1f
parent5e4e1eebcf9a6248ba9227d7f486ad1fe2a2d3d1
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