[herd] Strengthen the ordering requirements for Exp-haz-ob in aarch64.cat

Feedback from the the Linux kernel indicated that the implementation
of qspinlock would benefit from stronger ordering guarantees for
mixed-size memory accesses. This proposal is updating to the
Explicit-hazard-ordered-before rule in order to strengthen the
ordering requirements of the architecture.

As a result of this change, the following two tests become forbidden:

AArch64 CoRR+amo.swph0h0-posh0a.w0+w0
Variant=mixed
{
 uint32_t 0:X3; uint32_t 0:X2;
 0:X0=x;
 uint32_t 1:X1=0xccddeeff; 1:X0=x;
}
 P0              | P1          ;
 MOV W2,herd#42      | STR W1,[X0] ;
 SWPH W2,W1,[X0] |             ;
 LDAR W3,[X0]    |             ;
exists (0:X1=0xeeff /\ 0:X3=42)

AArch64 CoRR+rmwh0h0-posh0a.w0+w0
Variant=mixed
{
 uint32_t 0:X3; uint32_t 0:X2;
 0:X0=x;
 uint32_t 1:X1=0xccddeeff; 1:X0=x;
}
 P0               | P1          ;
 MOV W2,herd#42       | STR W1,[X0] ;
 LDXRH W1,[X0]    |             ;
 STXRH W4,W1,[X0] |             ;
 LDAR W3,[X0]     |             ;
exists (0:X1=0xeeff /\ 0:X3=42 /\ 0:X4=0)

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

Author: artkhyzha

catalogue/aarch64-mixed/shelf.py

@@ -2,13 +2,15 @@
 
 cats = [
     "cats/aarch64.cat",
-    ]
+]
 
 cfgs = [
     "cfgs/web-mixed.cfg",
 ]
 
 illustrative_tests = [
+    "tests/CoRR+amo.swph0h0-posh0a.w0+w0.litmus",
+    "tests/CoRR+rmwh0h0-posh0a.w0+w0.litmus",
     "tests/MP-Koeln.litmus",
     "tests/LB+dmb.sy+data-wsi-wsi+MIXED+H.litmus",
     "tests/MP+HAmo+BAcqAmo.litmus",

catalogue/aarch64-mixed/tests/@all

@@ -1,3 +1,5 @@
+CoRR+rmwh0h0-posh0a.w0+w0.litmus
+CoRR+amo.swph0h0-posh0a.w0+w0.litmus
 2+2W+posb0b0+posb1b1.litmus
 2+2W+posw0w0+posw4w4.litmus
 CO-MIXED-20cc+H.litmus

catalogue/aarch64-mixed/tests/CoRR+amo.swph0h0-posh0a.w0+w0.litmus

@@ -0,0 +1,14 @@
+AArch64 CoRR+amo.swph0h0-posh0a.w0+w0
+Variant=mixed
+{
+ uint32_t 0:X3; uint32_t 0:X2;
+ 0:X0=x;
+ uint32_t 1:X1=0xccddeeff; 1:X0=x;
+}
+ P0              | P1          ;
+ MOV W2,#42      | STR W1,[X0] ;
+ SWPH W2,W1,[X0] |             ;
+ LDAR W3,[X0]    |             ;
+exists (0:X1=0xeeff /\ 0:X3=42)
+
+(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *)

catalogue/aarch64-mixed/tests/CoRR+rmwh0h0-posh0a.w0+w0.litmus

@@ -0,0 +1,15 @@
+AArch64 CoRR+rmwh0h0-posh0a.w0+w0
+Variant=mixed
+{
+ uint32_t 0:X3; uint32_t 0:X2;
+ 0:X0=x;
+ uint32_t 1:X1=0xccddeeff; 1:X0=x;
+}
+ P0               | P1          ;
+ MOV W2,#42       | STR W1,[X0] ;
+ LDXRH W1,[X0]    |             ;
+ STXRH W4,W1,[X0] |             ;
+ LDAR W3,[X0]     |             ;
+exists (0:X1=0xeeff /\ 0:X3=42 /\ 0:X4=0)
+
+(* Linux's qspinlock for systems without FEAT_LSE requires that this is forbidden *)

catalogue/aarch64-mixed/tests/kinds.txt

@@ -1,3 +1,5 @@
+CoRR+amo.swph0h0-posh0a.w0+w0  Forbidden
+CoRR+rmwh0h0-posh0a.w0+w0      Forbidden
 2+2W+posb0b0+posb1b1           Allowed
 CO-MIXED-20cc+H                Forbidden
 CoRW2+posb0b0+b0               Allowed

herd/libdir/aarch64.cat

@@ -61,7 +61,7 @@ with IC-after from (all-IC-Imp_Instr_R-enums local-hw-reqs)
 
 (** Explicitly-hazard-ordered-before **)
 let Exp-haz-ob =
-  [Exp & R]; (po & same-loc); [Exp & R]; (ca & ext); [Exp & W]
+  [Exp & R]; (po & same-loc); [Exp & R]; sca-class?; [Exp & R]; (ca & ext); [Exp & W]; sca-class?; [Exp & W]
 
 (** TLBI-ordered-before **)
 

herd/libdir/catdefinitions.tex

@@ -18,7 +18,7 @@
 \newcommand{\sameloc}[2]{#1 and #2 are to the Same Location}
 \newcommand{\samelocemph}[2]{#1 and #2 are to the \emph{Same Location}}
 
-\newcommand{\sca}[2]{#1 belongs to the same single-copy-atomic class as #2}
+\newcommand{\sca}[2]{#1 belongs to the same single-copy-atomic grouping as #2}
 \newcommand{\po}[2]{#1 appears in program order before #2}
 
 \newcommand{\coemph}[2]{#1 is \emph{Coherence-write-before} #2}