From: Brian Norris <banorris@uci.edu>
Date: Thu, 1 Nov 2012 17:38:49 +0000 (-0700)
Subject: model: update mo_may_allow restrictions
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=d5c56ae55e7adf3e489de357ed5c80c640b67ec9;hp=d5c56ae55e7adf3e489de357ed5c80c640b67ec9

model: update mo_may_allow restrictions

For future values, we can enforce the following rule:

  If X --hb-> Y --mo-> Z, then X should not read from Z.

This a change from previous behavior, where we used 'sb' instead of
'hb'.

Tested with linuxrwlocks example:

  ./run.sh test/linuxrwlocks.o -f 4 -m 1

No difference in number of executions (feasible or infeasible); HASH
values were exactly the same.
---