Skip to content

Commit 83bb909

Browse files
relokinrelokin
authored
Merge pull request herd#1227 from relokin/aarch64-tests
Add tests to the aarch64 catalogue for existing relations of the memory model.
2 parents 12ee5b7 + 3fc8fe1 commit 83bb909

8 files changed

Lines changed: 82 additions & 0 deletions

‎catalogue/aarch64/shelf.py‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,4 +88,9 @@
8888
# "tests/R+CAS-rfi-ctrl+DMBST.litmus",
8989
# "tests/SB+CAS-rfi-addr+DMBSY.litmus",
9090
# "tests/SB+SWP-rfi-addr+DMBSY.litmus",
91+
"tests/MP+rel+addr-po-loc-addr.litmus",
92+
"tests/MP+rel+addr-lrs-acq.litmus",
93+
"tests/MP+rel+data-lrs-acq.litmus",
94+
"tests/MP+rel+ctrl-lrs-acq.litmus",
95+
"tests/MP+rel+rmw-lrs-acq.litmus",
9196
]

‎catalogue/aarch64/tests/@all‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,3 +50,8 @@ MP+rel+swp-acq.litmus
5050
# SB+dmb.sy+rel-acqpc.litmus
5151
# MP+rel+acqpc.litmus
5252
# MP+rel+swp-acqpc.litmus
53+
MP+rel+addr-po-loc-addr.litmus
54+
MP+rel+addr-lrs-acq.litmus
55+
MP+rel+data-lrs-acq.litmus
56+
MP+rel+ctrl-lrs-acq.litmus
57+
MP+rel+rmw-lrs-acq.litmus

‎catalogue/aarch64/tests/MP+rel+addr-lrs-acq.litmus‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
AArch64 MP+rel+addr-lrs-acq
2+
{
3+
0:X1=x; 0:X3=y;
4+
1:X1=x; 1:X3=y; 1:X5=z;
5+
}
6+
P0 | P1 ;
7+
MOV W0,#1 | LDR W2,[X3] ;
8+
STR W0,[X1] | EOR W4,W2,W2 ;
9+
MOV W2,#1 | MOV W6,#1 ;
10+
STLR W2,[X3] | STR W6,[X5,W4,SXTW] ;
11+
| LDAR W7,[X5] ;
12+
| EOR W8,W7,W7 ;
13+
| LDR W0,[X1] ;
14+
exists (1:X2=1 /\ 1:X0=0)

‎catalogue/aarch64/tests/MP+rel+addr-po-loc-addr.litmus‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
AArch64 MP+rel+addr-po-loc-addr
2+
{
3+
0:X1=x; 0:X3=y;
4+
1:X1=x; 1:X3=y; 1:X5=z;
5+
}
6+
P0 | P1 ;
7+
MOV W0,#1 | LDR W2,[X3] ;
8+
STR W0,[X1] | EOR W4,W2,W2 ;
9+
MOV W2,#1 | LDR W6,[X5,W4,SXTW] ;
10+
STLR W2,[X3] | LDR W7,[X5] ;
11+
| EOR W8,W7,W7 ;
12+
| LDR W0,[X1,W8,SXTW] ;
13+
exists (1:X2=1 /\ 1:X0=0)

‎catalogue/aarch64/tests/MP+rel+ctrl-lrs-acq.litmus‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
AArch64 MP+rel+ctrl-lrs-acq
2+
{
3+
0:X1=x; 0:X3=y;
4+
1:X1=x; 1:X3=y; 1:X5=z;
5+
}
6+
P0 | P1 ;
7+
MOV W0,#1 | LDR W2,[X3] ;
8+
STR W0,[X1] | CMP W2,#1 ;
9+
MOV W2,#1 | B.EQ L0 ;
10+
STLR W2,[X3] |L0: ;
11+
| MOV W6,#1 ;
12+
| STR W6,[X5] ;
13+
| LDAR W7,[X5] ;
14+
| LDR W0,[X1] ;
15+
exists (1:X2=1 /\ 1:X0=0)

‎catalogue/aarch64/tests/MP+rel+data-lrs-acq.litmus‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
AArch64 MP+rel+data-lrs-acq
2+
{
3+
0:X1=x; 0:X3=y;
4+
1:X1=x; 1:X3=y; 1:X5=z;
5+
}
6+
P0 | P1 ;
7+
MOV W0,#1 | LDR W2,[X3] ;
8+
STR W0,[X1] | EOR W4,W2,W2 ;
9+
MOV W2,#1 | ADD W6,W4,#1 ;
10+
STLR W2,[X3] | STR W6,[X5] ;
11+
| LDAR W7,[X5] ;
12+
| LDR W0,[X1] ;
13+
exists (1:X2=1 /\ 1:X0=0)

‎catalogue/aarch64/tests/MP+rel+rmw-lrs-acq.litmus‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
AArch64 MP+rel+rmw-lrs-acq
2+
{
3+
0:X1=x; 0:X3=y;
4+
1:X1=x; 1:X3=y;
5+
}
6+
P0 | P1 ;
7+
MOV W0,#1 | MOV W6,#2 ;
8+
STR W0,[X1] | SWP W6,W2,[X3] ;
9+
MOV W2,#1 | LDAR W7,[X3] ;
10+
STLR W2,[X3] | EOR W8,W7,W7 ;
11+
| LDR W0,[X1] ;
12+
exists (1:X2=1 /\ 1:X0=0)

‎catalogue/aarch64/tests/kinds.txt‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,3 +62,8 @@ MP+rel+acq Forbidden
6262
MP+rel+acqpc Forbidden
6363
MP+rel+swp-acq Forbidden
6464
MP+rel+swp-acqpc Forbidden
65+
MP+rel+addr-po-loc-addr Allowed
66+
MP+rel+addr-lrs-acq Forbidden
67+
MP+rel+data-lrs-acq Forbidden
68+
MP+rel+ctrl-lrs-acq Allowed
69+
MP+rel+rmw-lrs-acq Forbidden

0 commit comments

Comments
 (0)