[herd] No fault on crossing memtag granularity

[murzinv]

Consider litmus test

AArch64 T
{
int x[8]={1,2,3,4,5,6,7,8};

0:X0=x:green; 0:X1=x:red;
}
P0                               ;
STG X1,[X0,#1]                   ; (* set tag :red for x[4:7] *)
DMB SY                           ;
MOV W2,#9                        ;
MOV W3,#9                        ;
STP W2,W3,[X0,#12]               ; (* write to x[3:4] with tag :green *)

(* We expect tag fault due to access to x[4] *)
exists x={1,2,3,9,9,6,7,8} /\ ~fault(P0,x)

Note, that STG here relies on fix #812
Output of herd7 suggests that test is allowed

$ herd7 -variant memtag,sync T
Test T Allowed
States 1
x={1,2,3,9,9,6,7,8};  ~Fault(P0,x);
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (x={1,2,3,9,9,6,7,8} /\ not (fault(P0,x)))
Observation T Always 1 0
Time T 0.02
Hash=df433a02055836977667c54e7708421d

[maranget]

Well, as apparent from diagram, the tag is checked once only...
T.pdf