failed store exclusives should prevent pairing of preceding load exclusives

Line 112 in 7c2a817

| step_write_failure

There is a blind spot somewhere (maybe here): if there is a load exclusive followed by a failed store exclusive, then a later (successful) store exclusive should not be allowed pair with this load exclusive.

Right.. Thanks for pointing out a nasty bug!

Probably we need to do one of the following two options:

Insert write-failure event in the graph. But it deviates from the standard presenatation, right?
Construct rmw in the execution. I think we need to go this way..

I agree, I think that's what we should do. The first option would also mismatch with herd. What Jean and I were also talking about: there is still an open detail concerning what ARM wants from 'rmw' in the case of memory accesses to different addresses. I'll write an email to Will and see if he has an opinion, but I think he's fairly busy. Maybe we should rename 'rmw' to something different and make it relate any paired load and store exclusive, and then depending on whether ARM wants 'rmw' to contain any such pairs or only same-address pairs obtain 'rmw' as a derived relation from rmw?

…

On 17/05/18 14:56, Jeehoon Kang wrote: Right.. Thanks for pointing out a nasty bug! Probably we need to do one of the following two options: * Insert write-failure event in the graph. But it deviates from the standard presenatation, right? * Construct |rmw| in the execution. I think we need to go this way.. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#5 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AGUw4mN4ko2iX-wd6Ynggoao8LT7I-oBks5tzYGFgaJpZM4UDGMd>.

Currently I'm not sure which is the best way in terms of formalization. I'll leave this issue open, and resolve it during proving the simulations.

Now the issue is resolved: rmw is constructed in the axiomatic execution, and failed store exclusives prevent paring of preceding load exclusives.

Regarding @cp526's comment, let's temporarily assume only ldrex/stlex on the same location are paired. I'm opening a new issue #8 on this, and closing this issue.