[herd] Fix UDF CMODX type and introduce relaxation for non-modifying writes

[diaolo01]

In chapter B2.2.5 Concurrent modification and execution of instructions (CMODX) UDF is defined as an instruction for which the behaviour is more restricted.

Concurrent modification and execution of instructions can lead to the resulting instruction behaving like any possible sequence of instructions executable at the same Exception level. However, the behavior is more restricted if both the instruction before and the instruction after modification are one of B, B.cond, BL, BRK, CB, CBB, CBH, CBNZ, CBZ, HVC, ISB, NOP, SMC, SVC, TBNZ, TBZ, TRCIT, or UDF.

Therefore, UDF has been placed to have the appropriate behaviour and the comment associated with this paragraph has been updated.

Furthermore, this PR implements the relaxation such that for CMODX purposes, a write E2 is not considered to modify instruction location L when it writes the same value as the latest write E1 to L in coherence order.

[diaolo01]

@relokin While I was reviewing another PR I noticed a discrepancy between the Arm ARM and herd on the requirements for UDF. Given the comment in herd which I updated as part of this PR, is it safe to assume that this was a recent change in the Arm ARM? Does it match your expectation for the behaviour for UDF?

[relokin]

@artkhyzha can you please have a look at this?

[artkhyzha]

Yes, the CMODX rules were updated for the issue M.a (P.S. correction: it was M.b). The list of instructions with restricted behaviour got extended with UDF. This patch seems to implement that.

Additionally, the update added a note:

For the purposes of CMODX behavior, it is not considered a modification of an instruction at a Location L if a Memory Write Effect E2 writes the same value to L that was written by the latest Memory Write Effect E1 earlier in the coherence order for L than E2.

This note is not being implemented as a part of this PR, as far as I can see.

[diaolo01]

Thanks @artkhyzha.

I have added the test associated with the relaxation of the CMODX behaviour on the two writes. The result is that what used to return

Test A018 Required
States 1
1:X0=42;
Ok
Witnesses
Positive: 2 Negative: 0
Flag violates-CMODX-requirements
Condition forall (1:X0=42)
Observation A018 Always 2 0
Time A018 0.01

Now returns:

Test A018 Required
States 1
1:X0=42;
Ok
Witnesses
Positive: 2 Negative: 0
Condition forall (1:X0=42)
Observation A018 Always 2 0
Time A018 0.01

[artkhyzha]

Thank you, @diaolo01 -- LGTM.

Sharing two comments, but I think those are more like discussion points.

[artkhyzha]

Not important at the current stage (and I don't think this is a mandatory change for this PR), but "different-values" being a function may cause challenges for miaou7. I wonder if it needs to be a function? A bit surprised it's not a relation.

P.S. Not very important, because we are not currently transliterating these requirements with miaou7.

[artkhyzha]

Again, not sure this is an issue with the PR, just to raise awareness. I suppose "kinds" do not capture presence or absence of hints in the output, so this verdict is not sensitive to changes to cat.