[AARCH-25772,cat] Changes to the ordering requirements of DMB LD and DSB LD#1880
[AARCH-25772,cat] Changes to the ordering requirements of DMB LD and DSB LD#1880artkhyzha wants to merge 2 commits into
Conversation
|
Fixed. A different change implemented to handle "domain". Also, the cat file is edited slightly to improve the output. |
| | (if "ETS2" || "ETS3" then [M | DC.CVAU | IC | TLBI]; po; [dsb.full]; po; [Imp & TTD & M] else 0) | ||
| | [(Exp & R) \ NoRet | Imp & Tag & R]; po; [dsb.ld]; po; [~(Imp & TTD & M | Imp & Instr & R)] | ||
| | (if "ETS2" || "ETS3" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M] else 0) | ||
| | [(Exp & R) \ NoRet | domain([Imp & Tag & R]; same-instance; [(Exp & R) \ NoRet])]; po; [dsb.ld]; po; [~(Imp & TTD & M | Imp & Instr & R)] |
There was a problem hiding this comment.
have we consider the case where E1 is generated by a LDR instruction that faults?
There was a problem hiding this comment.
Yes and no. It is quite hard to come up with a relevant test. In simple MP shapes, this Imp Tag R would be IFB-ordered-before everything that follows the exception entry in program order. This renders DMB LD irrelevant.
So in principle it is interesting to ponder whether the phrasing for the changes to DMB LD needs to be adjusted to account for the faulting case, but it could be good to invent a test for it.
There was a problem hiding this comment.
Can you please also add the catdefinitions.tex here?
I assume you didn't have to make any changes to catdefinitions.tex?
2 participants
This PR relaxes the architectural intent so that DMB LD and DSB LD provide order from Implicit Tag Memory Read Effects only if those are generated by instructions that (1) also generate Explicit Memory Read Effects, and (2) are not atomic instructions that use a zero register as their destination register.
In the case of DSB LD, implementing the relaxation to the architectural intent means correcting the ETS2 clause that previously omitted Implicit Tag Memory Reads. Hence, this specific case actually shows up as a strengthening in logs.
The following is the output of verdicts from
herd7for the tests in this PR. Some of them illustrate the changes, others illustrate corner cases that are not affected.P.S. The above table is produced via commands: