[AARCH-24571,herd] Fixes in aarch64.cat relating to FEAT_HAFDBS

This change implements AARCH-24571 as published in the Arm
Architecture Reference Manual for A-profile architecture: Known issues
in Issue L.b.

With FEAT_HAFDBS, in the case where one PE, P0, is configured with
hardware updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), but
another PE, P1, using the same translation tables is configured with
hardware updates of Dirty state disabled ((TCR_ELx.{HA, HD}={x, 0}),
the following scenario can occur:

* P1 has a copy of a writable-clean translation table entry cached in
  a TLB.
* P0 performs a hardware update of Dirty state for that translation
  table entry.
* A store is attempted on P1, and this hits the writable-clean
  translation table entry cached in the TLB.

The architecture permits the store on P1 to generate a Permission
fault, because P1 has hardware updates of Dirty state disabled.
However, the formal memory model did not permit this outcome. The
changes below relax the memory model to permit this outcome, and
therefore match the rules described in section D8.5.2.1 "Hardware
management of the dirty state".

As a result the following test is architecturally forbidden:

AArch64 S.HU+dsb.sy+dsb.sy-isb
Variant=vmsa
TTHM=P0:HD
{
 [TTD(x)]=(oa:PA(x), dbm:1, db:0);
 0:X1=x; 0:X3=y;
 1:X1=x; 1:X3=y;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W2,[X3] ;
 STR W0,[X1] | DSB SY      ;
 DSB SY      | ISB         ;
 MOV W2,#1   | MOV W0,#2   ;
 STR W2,[X3] | STR W0,[X1] ;
exists (1:X2=1 /\ fault(P1,x))

In addition, in the case where a PE is configured with hardware
updates of Dirty state enabled (TCR_ELx.{HA, HD}={1, 1}), the
architecture forbids the hardware update of Dirty state on the PE
until the associated store is known to be non-speculative and,
therefore, ahead of the address translation or the tag check of an
instruction earlier in program order. However, the formal memory
model allowed such an outcome to be observed. The changes below
strengthen the memory model to forbid this outcome, and therefore
match the rules described in section D8.5.2.1 "Hardware management of
the dirty state".

As a result, the following test is architecturally forbidden:

AArch64 S.HU+dmb.st+po-ttd
TTHM=P1:HD
Variant=vmsa,fatal
{
 [TTD(x)]=(oa:PA(x), dbm:1, db:0);
 [TTD(y)]=(oa:PA(y), valid:0);
 pteval_t 0:X6=(oa:PA(y), valid:1); 0:X7=TTD(y);
 pteval_t 0:X8=(oa:PA(x), dbm:1, db:0); 0:X9=TTD(x);
 1:X1=x; 1:X3=y;
}
 P0          | P1               ;
 STR X8,[X9] | L0: LDR WZR,[X3] ;
 DMB ST      | MOV W0,#1        ;
 STR X6,[X7] | L1: STR W0,[X1]  ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))

and the following test is architecturally forbidden:

AArch64 S.HU+dmb.st+po-tag
TTHM=P1:HD
Variant=vmsa,fatal,mte,sync
{
 [TTD(x)]=(oa:PA(x), dbm:1, db:0);
 [TTD(y)]=(oa:PA(y), TaggedNormal);
 0:X6=y:red; 0:X7=y:green;
 pteval_t 0:X8=(oa:PA(x), dbm:1, db:0);
 0:X9=TTD(x);
 1:X1=x; 1:X3=y:red;
}
 P0          | P1               ;
 STR X8,[X9] | L0: LDR WZR,[X3] ;
 DMB ST      | MOV W0,#1        ;
 STG X6,[X7] | L1: STR WZR,[X1] ;
exists (not (fault(P1:L0)) /\ [TTD(x)]=(oa:PA(x), dbm:1, db:0))

Signed-off-by: Nikos Nikoleris <nikos.nikoleris@arm.com>

Author: artkhyzha

catalogue/aarch64-VMSA/tests/VMSA-kinds.txt

@@ -621,7 +621,7 @@ D15347-2+2WExpNExp+DMBST+DSB-ISB               Allowed
 Artem2+TLBIx-HDy+dsb.ish                       Forbidden
 2+2WNExpExp+NExpNExp+SHOW                      Forbidden
 F2.mod-with-type+BBM-DSB-ISB                   Forbidden
-2+2WNExpExp+NExpNExp+DMBST+DMBST               Allowed
+2+2WNExpExp+NExpNExp+DMBST+DMBST               Forbidden
 2+2WNExpExp+NExpNExp+DMBST+DMBST+SHOW          Forbidden
 Artem2+TLBIx-TLBIy+dmb2                        Forbidden
 Artem3+UCx-TLBIy+dsb.ish-isb+dmb.ld            Forbidden

herd/libdir/aarch64.cat

@@ -108,13 +108,13 @@ let Tag-obs =
 
 (** TTD-observed-by **)
 
-(* TLBUncacheable-predecessor *)
-let TLBuncacheable-pred =
-  [range([TLBUncacheable & FAULT]; tr-ib^-1)]; (ca & ~intervening(W,ca)); [Exp & W]
+(* TLBUncacheable-coherence-after *)
+let TLBuncacheable-ca =
+  [range([TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R])]; ca; [Exp & W | HU]
 
-(* Hardware-update-predecessor *)
-let HU-pred =
-  (ca & ~intervening(W,ca)); [HU]
+(* Hardware-update-coherence-after *)
+let HU-ca =
+  [Exp & R]; ca; [HU]
 
 (* TLBI-coherence-after *)
 let TLBI-ca =
@@ -123,8 +123,8 @@ let TLBI-ca =
 (* TTD-observed-by *)
 let TTD-obs =
     [Imp & TTD]; rf | rf; [Imp & TTD]
-    | TLBuncacheable-pred
-    | HU-pred
+    | TLBuncacheable-ca
+    | HU-ca
     | [HU]; ca; [W] | [W]; ca; [HU]
     | TLBI-ca
 

herd/libdir/aarch64hwreqs.cat

@@ -97,8 +97,8 @@ let dob =
  | addr; [Exp & M]; po; [Exp & W | HU]
  | addr; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
  | data; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
- | [Imp & TTD & R]; tr-ib; [Exp & M]; po; [Exp & W]
- | [Imp & Tag & R]; tc-before; [Exp & M]; po; [Exp & W] 
+ | [Imp & TTD & R]; tr-ib; [Exp & M]; po; [Exp & W | HU]
+ | [Imp & Tag & R]; tc-before; [Exp & M]; po; [Exp & W | HU]
 
 (* Fetch-ordered-before *)
 let f-ob =

herd/libdir/catdefinitions.tex

@@ -380,18 +380,12 @@
 \newcommand{\ob}[2]{#1 is Ordered-before #2}
 \newcommand{\obemph}[2]{#1 is \emph{Ordered-before} #2}
 
-\newcommand{\TLBuncacheablepredname}{a TLBUncacheable-Write-Predecessor of}
-\newcommand{\TLBuncacheablepred}[2]{#1 is a TLBUncacheable-Write-Predecessor of #2}
-\newcommand{\TLBuncacheablepredemph}[2]{#1 is \emph{a TLBUncacheable-Write-Predecessor of} #2}
-\newcommand{\TLBuncacheablesuccname}{a TLBUncacheable-Write-Successor of}
-\newcommand{\TLBuncacheablesucc}[2]{#1 is a TLBUncacheable-Write-Successor of #2}
-\newcommand{\TLBuncacheablesuccemph}[2]{#1 is \emph{a TLBUncacheable-Write-Successor of} #2}
-\newcommand{\HUpredname}{a Hardware-Update-Predecessor of}
-\newcommand{\HUpred}[2]{#1 is a Hardware-Update-Predecessor of #2}
-\newcommand{\HUpredemph}[2]{#1 is \emph{a Hardware-Update-Predecessor of} #2}
-\newcommand{\HUsuccname}{a Hardware-Update-Successor of}
-\newcommand{\HUsucc}[2]{#1 is a Hardware-Update-Successor of #2}
-\newcommand{\HUsuccemph}[2]{#1 is \emph{a Hardware-Update-Successor of} #2}
+\newcommand{\TLBuncacheablecaname}{TLBUncacheable-coherence-before}
+\newcommand{\TLBuncacheableca}[2]{#1 is \TLBuncacheablecaname{} #2}
+\newcommand{\TLBuncacheablecaemph}[2]{#1 is \emph{\TLBuncacheablecaname{}} #2}
+\newcommand{\HUcaname}{Hardware-Update-coherence-before}
+\newcommand{\HUca}[2]{#1 is \HUcaname{} #2}
+\newcommand{\HUcaemph}[2]{#1 is \emph{\HUcaname{}} #2}
 
 %
 \newcommand{\rangelxsx}[1]{#1 is generated by a Store-Exclusive instruction as part of \lxsx}