[herd7,aarch64] A failed CAS may write back

[artkhyzha]

The objective of this PR is to amend the instruction semantics for CAS in case when its comparison fails. Broadly speaking, whenever a CAS fails its comparison, it is now allowed to read the original value in memory and then write the same value back. This has consequences: an Explicit Write Effect may be created, a Hardware Update might be created, (with FEAT_MTE_STOREONLY not supported by herd7 presently) a TagCheck may be created.

The following kinds of executions are expected of a failed CAS:

• CAS generates an Explicit Write Effect of a value that is already in memory and, if -variant vmsa is enabled, that leads to generating a Hardware Update to the dirty bit.
• CAS does not generate an Explicit Write Effect and, if -variant vmsa is enabled, a candidate execution with a Hardware Update to the dirty bit is generated.
• CAS does not generate an Explicit Write Effect and, if -variant vmsa is enabled, a candidate execution without a Hardware Update to the dirty bit is generated.

Note that the aforementioned three executions are archetypes: other "alternatives" affect the overall number of executions. Thus, for instance, the test ./herd/tests/instructions/AArch64.kvm/A019.litmus has 5 rather than 3 executions.

[HadrienRenaud]

Hi @artkhyzha

Thanks a lot for this, sorry a comment escaped my pending review on Friday ...

I have mainly stylistic comments, feel free not to follow them.

[artkhyzha]

Thank you very much, @HadrienRenaud, the stylistic comments are much appreciated. I found them all helpful to apply.

[artkhyzha]

@jalglave, this PR seems to be in a decent shape, so I am hoping to check with you how to best go about it.

It essentially implements the outcomes of the investigation for the failed CAS: the user-level semantics, the db-bit semantics. One more outcome of that investigation was similar changes to behaviour for Tag Checks when FEAT_MTE_STORE_ONLY is implemented (essentially, to turn off tag checks for loads, with corner cases for CAS). This feature is not yet supported by herd7, so this PR has not attempted to change the semantics of CAS.

Overall, a few questions. Do we want more reviews before merging? Do we want to put FEAT_MTE_STORE_ONLY on the todo list? Is it alright to keep this feature of MTE out of scope of this PR? All feedback is very welcome!

[murzinv]

Overall, a few questions. Do we want more reviews before merging? Do we want to put FEAT_MTE_STORE_ONLY on the todo list? Is it alright to keep this feature of MTE out of scope of this PR? All feedback is very welcome!

Actually I was waiting for this PR merged to restart my work on FEAT_MTE_STORE_ONLY. If it helps, I can rebase my work on top of this PR asap and report back...

[artkhyzha]

Ah, super to hear that's something you are working on, @murzinv. Rebasing on top of this would be great, but also if you think another strategy could be more helpful, don't hesitate to let me know.

[artkhyzha]

As this seems reasonably mature, I'll be aiming to merge this by the end of the day. @HadrienRenaud, @jalglave, @murzinv -- if any reason not to merge this comes up, please let me know.

[murzinv]

Ah, super to hear that's something you are working on, @murzinv. Rebasing on top of this would be great, but also if you think another strategy could be more helpful, don't hesitate to let me know.

@artkhyzha here is change for FEAT_MTE_STOREONLY . Feel free to cherry-pick in your series or I can make separate PR

[murzinv]

As this seems reasonably mature, I'll be aiming to merge this by the end of the day. @HadrienRenaud, @jalglave, @murzinv -- if any reason not to merge this comes up, please let me know.

@artkhyzha should we do anything for CASP?

[artkhyzha]

Excellent point about CASP, @murzinv! This should have been within the scope, and its support should look similar. I'll update the PR.

[artkhyzha]

I've pushed an update for CASP essentially copying the solution for CAS.

Perhaps, overly pedantically, but reading CASP description I am not sure CASP behaves exactly like CAS (i.e., has two options for present/absent Explicit Effect rather than, say, four). Hence, I'd like to hold off merging this for a little bit.

[artkhyzha]

Apologies, a follow-up to this fell between the cracks. I had concerns that perhaps there are more sophisticated single-copy atomicity rules. However, having double checked the letter of the Arm ARM and confirmed the reading of it with architects, I believe CASP is intended to always be single-copy-atomic to its full size, for both the read effect and the write effect (if the write effect does actually occur) -- or is subject to an alignment fault. To the best of my understanding, the current status of this PR treats CASP fairly.