[catalogue,aarch64] Four forbidden tests with acq/acqpc

herd · Feb 7, 2025 · 3b760e7 · 3b760e7
1 parent e660aa7
commit 3b760e7
Show file tree

Hide file tree

Showing 6 changed files with 66 additions and 0 deletions.
diff --git a/catalogue/aarch64/tests/@all b/catalogue/aarch64/tests/@all
@@ -45,3 +45,7 @@ SB+SWP-rfi-addr+DMBSY.litmus
 STABLE.litmus
 SB+dmb.sy+rel-acq.litmus
 SB+dmb.sy+rel-acqpc.litmus
+MP+rel+acq.litmus
+MP+rel+acqpc.litmus
+MP+rel+swp-acq.litmus
+MP+rel+swp-acqpc.litmus
diff --git a/catalogue/aarch64/tests/MP+rel+acq.litmus b/catalogue/aarch64/tests/MP+rel+acq.litmus
@@ -0,0 +1,14 @@
+AArch64 MP+rel+acq
+Hash=495a52a1116ac63cc33ec0326b58baf2
+
+{
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1           ;
+ MOV W0,#1    | LDAR W2,[X3] ;
+ STR W0,[X1]  | LDR W0,[X1]  ;
+ MOV W2,#1    |              ;
+ STLR W2,[X3] |              ;
+
+exists (1:X2=1 /\ 1:X0=0)
diff --git a/catalogue/aarch64/tests/MP+rel+acqpc.litmus b/catalogue/aarch64/tests/MP+rel+acqpc.litmus
@@ -0,0 +1,14 @@
+AArch64 MP+rel+acqpc
+Hash=d6d86cf550511c467b404723f249e4b5
+
+{
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1            ;
+ MOV W0,#1    | LDAPR W2,[X3] ;
+ STR W0,[X1]  | LDR W0,[X1]   ;
+ MOV W2,#1    |               ;
+ STLR W2,[X3] |               ;
+
+exists (1:X2=1 /\ 1:X0=0)
diff --git a/catalogue/aarch64/tests/MP+rel+swp-acq.litmus b/catalogue/aarch64/tests/MP+rel+swp-acq.litmus
@@ -0,0 +1,15 @@
+AArch64 MP+rel+swp-acq
+Hash=888df33148f87689cd7e94563e4ac353
+
+{
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W4,#2      ;
+ STR W0,[X1]  | SWP W4,W2,[X3] ;
+ MOV W2,#1    | LDAR W6,[X3]   ;
+ STLR W2,[X3] | LDR W0,[X1]    ;
+
+locations [1:X6;]
+exists (1:X2=1 /\ 1:X0=0)
diff --git a/catalogue/aarch64/tests/MP+rel+swp-acqpc.litmus b/catalogue/aarch64/tests/MP+rel+swp-acqpc.litmus
@@ -0,0 +1,15 @@
+AArch64 MP+rel+swp-acqpc
+Hash=488776eb14009dc2c498c181e1ff7d3a
+
+{
+ 0:X1=x; 0:X3=y;
+ 1:X1=x; 1:X3=y;
+}
+ P0           | P1             ;
+ MOV W0,#1    | MOV W4,#2      ;
+ STR W0,[X1]  | SWP W4,W2,[X3] ;
+ MOV W2,#1    | LDAPR W6,[X3]  ;
+ STLR W2,[X3] | LDR W0,[X1]    ;
+
+locations [1:X6;]
+exists (1:X2=1 /\ 1:X0=0)
diff --git a/catalogue/aarch64/tests/kinds.txt b/catalogue/aarch64/tests/kinds.txt
@@ -58,3 +58,7 @@ CoWW           Forbidden
 LB+SWP-RsRt-addr+rel Allowed
 SB+dmb.sy+rel-acq               Forbidden
 SB+dmb.sy+rel-acqpc             Allowed
+MP+rel+acq                      Forbidden
+MP+rel+acqpc                    Forbidden
+MP+rel+swp-acq                  Forbidden
+MP+rel+swp-acqpc                Forbidden