`rmw` relates load/store exclusives on different locations?

[jeehoonkang]

Currently it doesn't. But it's unclear whether the spec allows it: #5 (comment)

[jeehoonkang]

The manual says "The address used in a STREX instruction must be the same as the address in the most recently executed LDREX instruction. The result of executing a STREX instruction to a different address is unpredictable." (http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0489e/Cihbghef.html) So basically it's undefined behavior..

[cp526]

I just had some email conversation with Will Deacon about that. What they are saying is that you get something slightly less than undefined behaviour either CONSTRAINED UNPREDICTABLE, or that the value returned from the load exclusive and the value the store exclusive writes to memory become UNKNOWN. I'm not sure what we should best do with that. We could have a special operational model state for this and then allow that to match any axiomatic model execution?

…

On 27 May 2018, at 06:47, Jeehoon Kang ***@***.***> wrote: The manual says "The address used in a STREX instruction must be the same as the address in the most recently executed LDREX instruction. The result of executing a STREX instruction to a different address is unpredictable." (http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.dui0489e/Cihbghef.html) So basically it's undefined behavior.. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[jeehoonkang]

It's very unclear what CONSTRAINED UNPREDICTABLE and UNKNOWN mean.. and I don't think we have to define it precisely in this paper. Also, I think introducing special operational model state will complicate things too much.. at least in formalization.

Currently, the formalization follows what's written in the view_arm repo (https://bitbucket.org/jean_pichon/view_arm, main.pdf, notblocked). In short, the semantics unconditionally allows relating different locations as an rmw pair. It's different from what the manual says, but I think it's a reasonable choice.

[jeehoonkang]

Also, May I ask if you could add Jean, Gil, and me in the conversation with Will Deacon?

[cp526]

Sure, sorry, done that now. We had the conversation going before the issue came up in Promising.

…

On 27 May 2018, at 16:11, Jeehoon Kang ***@***.***> wrote: Also, May I ask if you could add Jean, Gil, and me in the conversation with Will Deacon? — You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[jeehoonkang]

our semantics: nondeterministically succeed or fail.

discuss the caveat in the paper. architecture allows constrainted unpredictable (?) behaviors.