Generating ARMv8 exclusives and acquire/release instructions using offset register about memalloy HOT 2 CLOSED

Interesting to note that address-dependencies into store-releases are redundant because one or the other can be removed from the point-of-view of minimality.

from memalloy.

Here's a simple test case. Put the following into execution_hints/excl.als:

pred excl[X:Exec] {
  some disj e0,e1,e2 : E {
    X.sb = ^((e0 -> e1)+(e1 -> e2))
    X.sthd = sq[e0+e1+e2]
    X.ad = (e0 -> e1) + (e0 -> e2)
    X.atom = (e1 -> e2)
  }
}

and then try:

./comparator -arch ARM8 -satisfies models/aarch64.cat -hint execution_hints/excl.als -events 3

from memalloy.