Refine AArch64 BBM modelling and add regression coverage

Makefile

@@ -283,6 +283,19 @@ cata-test:: test.herd.cata.aarch64-ETS3
 cata-test:: test.herd.cata.bpf
 cata-test:: test.herd.cata.x86_64
 
+test.herd.cata-ext.%:
+	@ echo
+	$(HERD_REGRESSION_TEST) \
+		-j $(J) \
+		$(NOHASH) \
+		-herd-path $(HERD) \
+		-libdir-path ./herd/libdir \
+		-litmus-dir  catalogue/$*/tests \
+		$(REGRESSION_TEST_MODE)
+	@ echo "herd7 catalogue $* instructions tests: OK"
+
+cata-test-all:: test.herd.cata-ext.aarch64-BBM
+
 test.herd-mixed.cata.%:
 	@ echo
 	$(HERD_CATALOGUE_REGRESSION_TEST) \

catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus

@@ -0,0 +1,12 @@
+AArch64 CoRW2+PteOA
+Variant=vmsa
+{
+  [PTE(x)]=(oa:PA(x));
+  0:X1=x;
+  1:X4=(oa:PA(y)); 1:X5=PTE(x);
+}
+ P0          | P1          ;
+ LDR W0,[X1] | STR X4,[X5] ;
+ MOV W2,#1   |             ;
+ STR W2,[X1] |             ;
+exists(0:X0=1)

catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected

@@ -0,0 +1,11 @@
+Test CoRW2+PteOA Allowed
+States 1
+0:X0=0;
+No
+Witnesses
+Positive: 0 Negative: 2
+Flag Warning-BBM-expected
+Condition exists (0:X0=1)
+Observation CoRW2+PteOA Never 0 2
+Hash=9de3aed52a968ab42947a7ce50719893
+

catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus

@@ -0,0 +1,12 @@
+AArch64 CoWR+PteOA
+Variant=vmsa
+{
+  [PTE(x)]=(oa:PA(x));
+  0:X1=x;
+  1:X4=(oa:PA(y)); 1:X5=PTE(x);
+}
+ P0          | P1          ;
+ MOV W0,#1   | STR X4,[X5] ;
+ STR W0,[X1] |             ;
+ LDR W2,[X1] |             ;
+exists(0:X2=0)

catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected

@@ -0,0 +1,12 @@
+Test CoWR+PteOA Allowed
+States 2
+0:X2=0;
+0:X2=1;
+Ok
+Witnesses
+Positive: 1 Negative: 2
+Flag Warning-BBM-expected
+Condition exists (0:X2=0)
+Observation CoWR+PteOA Sometimes 1 2
+Hash=07e4543b71a8507c54a06609bbe02023
+

catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus

@@ -0,0 +1,17 @@
+AArch64 MP+dsb.ishs-[isb]+posptev0pteoa
+Variant=vmsa
+{
+ [y]=1;
+ [PTE(x)]=(oa:PA(x));
+ 0:X1=x; 1:X1=x;
+ 1:X4=(valid:0); 1:X5=PTE(x);
+ 1:X6=(oa:PA(y));
+}
+ P0           | P1             ;
+ L1:          | STR X4,[X5]    ;
+  LDR W0,[X1] | STR X6,[X5]    ;
+  DSB ISH     |                ;
+  ISB         |                ;
+ L2:          |                ;
+  LDR W2,[X1] |                ;
+exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x)))

catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected

@@ -0,0 +1,15 @@
+Test MP+dsb.ishs-[isb]+posptev0pteoa Allowed
+States 5
+0:X0=0; 0:X2=0;  ~Fault(P0:L2,x);
+0:X0=0; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation);
+0:X0=0; 0:X2=1;  ~Fault(P0:L2,x);
+0:X0=1; 0:X2=0;  ~Fault(P0:L2,x);
+0:X0=1; 0:X2=1;  ~Fault(P0:L2,x);
+Ok
+Witnesses
+Positive: 1 Negative: 5
+Flag Warning-BBM-expected
+Condition exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x)))
+Observation MP+dsb.ishs-[isb]+posptev0pteoa Sometimes 1 5
+Hash=b59acf4b892251b7a42f01048c3b71de
+

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus

@@ -0,0 +1,20 @@
+AArch64 MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld
+Variant=vmsa
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X1=(valid:0); 0:X0=PTE(x);
+  0:X5=(oa:PA(y),valid:1);
+  0:X3=z; 0:X4=x;
+  1:X3=z; 1:X4=x;
+}
+ P0              | P1          ;
+ STR X1,[X0]     | LDR W2,[X3] ;
+ DSB ISH         | DMB LD      ;
+ LSR X9,X4,#12   | LDR W5,[X4] ;
+ TLBI VAAE1IS,X9 |             ;
+ DSB ISH         |             ;
+ STR X5,[X0]     |             ;
+ MOV W2,#1       |             ;
+ STLR W2,[X3]    |             ;
+exists (1:X2=1 /\ 1:X5=1)

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected

@@ -0,0 +1,14 @@
+Test MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld Allowed
+States 5
+1:X2=0; 1:X5=0;
+1:X2=0; 1:X5=1;
+1:X2=0; 1:X5=2;
+1:X2=1; 1:X5=0;
+1:X2=1; 1:X5=2;
+No
+Witnesses
+Positive: 0 Negative: 6
+Condition exists (1:X2=1 /\ 1:X5=1)
+Observation MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld Never 0 6
+Hash=7d38f0901d8d6b17719acf4e80afbd92
+

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus

@@ -0,0 +1,18 @@
+AArch64 MP+tlbi-sync.ishpteoadb0p+dmb.ld
+Variant=vmsa
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x),db:0);
+  0:X1=(oa:PA(y),db:0); 0:X0=PTE(x);
+  0:X3=z; 0:X4=x;
+  1:X3=z; 1:X4=x;
+}
+ P0              | P1          ;
+ STR X1,[X0]     | LDR W2,[X3] ;
+ DSB ISH         | DMB LD      ;
+ LSR X9,X4,#12   | LDR W5,[X4] ;
+ TLBI VAAE1IS,X9 |             ;
+ DSB ISH         |             ;
+ MOV W2,#1       |             ;
+ STR W2,[X3]     |             ;
+exists (1:X2=1 /\ 1:X5=1)

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected

@@ -0,0 +1,12 @@
+Test MP+tlbi-sync.ishpteoadb0p+dmb.ld Allowed
+States 3
+1:X2=0; 1:X5=1;
+1:X2=0; 1:X5=2;
+1:X2=1; 1:X5=2;
+No
+Witnesses
+Positive: 0 Negative: 4
+Condition exists (1:X2=1 /\ 1:X5=1)
+Observation MP+tlbi-sync.ishpteoadb0p+dmb.ld Never 0 4
+Hash=6f66d48a711d25dc7a97d5151c6a07d1
+

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus

@@ -0,0 +1,18 @@
+AArch64 MP+tlbi-sync.ishpteoap+dmb.ld
+Variant=vmsa
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X1=(oa:PA(y),valid:1); 0:X0=PTE(x);
+  0:X3=z; 0:X4=x;
+  1:X3=z; 1:X4=x;
+}
+ P0              | P1          ;
+ STR X1,[X0]     | LDR W2,[X3] ;
+ DSB ISH         | DMB LD      ;
+ LSR X9,X4,#12   | LDR W5,[X4] ;
+ TLBI VAAE1IS,X9 |             ;
+ DSB ISH         |             ;
+ MOV W2,#1       |             ;
+ STR W2,[X3]     |             ;
+exists (1:X2=1 /\ 1:X5=1)

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected

@@ -0,0 +1,13 @@
+Test MP+tlbi-sync.ishpteoap+dmb.ld Allowed
+States 3
+1:X2=0; 1:X5=1;
+1:X2=0; 1:X5=2;
+1:X2=1; 1:X5=2;
+No
+Witnesses
+Positive: 0 Negative: 4
+Flag Warning-BBM-expected
+Condition exists (1:X2=1 /\ 1:X5=1)
+Observation MP+tlbi-sync.ishpteoap+dmb.ld Never 0 4
+Hash=68710d542d637562dda4d817ef00baef
+

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus

@@ -0,0 +1,18 @@
+AArch64 MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos
+Variant=vmsa
+TTHM=P1:HA
+{
+ [x]=1;
+ [y]=2;
+ 0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); pteval_t 0:X2=0; 0:X3=(oa:PA(y)); 0:X4=x;
+ 1:X4=x;
+}
+ P0              | P1               ;
+ STR X1,[X0]     | L01: LDR W2,[X4] ;
+ DSB ISH         | L00: LDR W5,[X4] ;
+ LSR X5,X4,#12   |                  ;
+ TLBI VAAE1IS,X5 |                  ;
+ DSB ISH         |                  ;
+ CAS X1,X3,[X0]  |                  ;
+
+exists (1:X2=2 /\ 1:X5=1)

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected

@@ -0,0 +1,12 @@
+Test MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos Allowed
+States 3
+1:X2=1; 1:X5=1;
+1:X2=1; 1:X5=2;
+1:X2=2; 1:X5=2;
+No
+Witnesses
+Positive: 0 Negative: 70
+Condition exists (1:X2=2 /\ 1:X5=1)
+Observation MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos Never 0 70
+Hash=2d93e28584c394c2b67face920ecd28c
+

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus

@@ -0,0 +1,17 @@
+AArch64 MP+tlbi-sync.ishspteaf0pteoa.af1+pos
+Variant=vmsa
+{
+ [x]=1;
+ [y]=2;
+ 0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); 0:X2=(oa:PA(y)); 0:X3=x;
+ 1:X3=x;
+}
+ P0              | P1               ;
+ STR X1,[X0]     | L01: LDR W4,[X3] ;
+ DSB ISH         | L00: LDR W5,[X3] ;
+ LSR X4,X3,#12   |                  ;
+ TLBI VAAE1IS,X4 |                  ;
+ DSB ISH         |                  ;
+ STR X2,[X0]     |                  ;
+
+exists (1:X4=2 /\ 1:X5=1)

catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected

@@ -0,0 +1,15 @@
+Test MP+tlbi-sync.ishspteaf0pteoa.af1+pos Allowed
+States 6
+1:X4=0; 1:X5=0;
+1:X4=1; 1:X5=0;
+1:X4=1; 1:X5=1;
+1:X4=1; 1:X5=2;
+1:X4=2; 1:X5=0;
+1:X4=2; 1:X5=2;
+No
+Witnesses
+Positive: 0 Negative: 9
+Condition exists (1:X4=2 /\ 1:X5=1)
+Observation MP+tlbi-sync.ishspteaf0pteoa.af1+pos Never 0 9
+Hash=e6ef300b6f55d2300ac976c99b0e5c3e
+

catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus

@@ -0,0 +1,14 @@
+AArch64 RW+RR+rel+acq+PteOA
+Variant=vmsa
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X0=x; 1:X0=x;
+  0:X3=z; 1:X3=z;
+  2:X4=(oa:PA(y)); 2:X5=PTE(x);
+}
+ P0           | P1           | P2          ;
+ LDR W1,[X0]  | LDAR W2,[X3] | STR X4,[X5] ; 
+ MOV W2,#1    | LDR W1,[X0]  |             ;
+ STLR W2,[X3] |              |             ;
+exists(0:X1=2 /\ 1:X1=1)

catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected

@@ -0,0 +1,14 @@
+Test RW+RR+rel+acq+PteOA Allowed
+States 4
+0:X1=1; 1:X1=1;
+0:X1=1; 1:X1=2;
+0:X1=2; 1:X1=1;
+0:X1=2; 1:X1=2;
+Ok
+Witnesses
+Positive: 2 Negative: 6
+Flag Warning-BBM-expected
+Condition exists (0:X1=2 /\ 1:X1=1)
+Observation RW+RR+rel+acq+PteOA Sometimes 2 6
+Hash=2679c3daefc5c2fefdfa8b6eb6c93e54
+

catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus

@@ -0,0 +1,13 @@
+AArch64 W+WW+PteOA
+Variant=vmsa
+{
+  [PTE(x)]=(oa:PA(x));
+  0:X1=x;
+  1:X4=(oa:PA(y)); 1:X5=PTE(x);
+}
+ P0          | P1          ;
+ MOV W0,#1   | STR X4,[X5] ;
+ STR W0,[X1] |             ;
+ MOV W2,#2   |             ;
+ STR W2,[X1] |             ;
+exists([x]=0 /\ [y]=1)

catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected

@@ -0,0 +1,14 @@
+Test W+WW+PteOA Allowed
+States 4
+[x]=0; [y]=2;
+[x]=1; [y]=2;
+[x]=2; [y]=0;
+[x]=2; [y]=1;
+No
+Witnesses
+Positive: 0 Negative: 4
+Flag Warning-BBM-expected
+Condition exists ([x]=0 /\ [y]=1)
+Observation W+WW+PteOA Never 0 4
+Hash=91f83a50665f5fef5bb692282cd910f1
+

catalogue/aarch64-BBM/tests/coRR+BBM.litmus

@@ -0,0 +1,18 @@
+AArch64 coRR+BBM 
+(* coRR-pte9 *)
+Variant=vmsa
+{
+ [y]=1;
+ [PTE(x)]=(oa:PA(x));
+ 0:X1=x; 1:X1=x;
+ 1:X4=(valid:0); 1:X5=PTE(x);
+ 1:X6=(oa:PA(y));
+}
+ P0           | P1              ;
+ L1:          | STR X4,[X5]     ;
+  LDR W0,[X1] | DSB ISH         ;
+ L2:          | LSR X9,X1,#12   ;
+  LDR W2,[X1] | TLBI VAAE1IS,X9 ;
+              | DSB ISH         ;
+              | STR X6,[X5]     ;
+exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x)))

catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected

@@ -0,0 +1,14 @@
+Test coRR+BBM Allowed
+States 5
+0:X0=0; 0:X2=0;  ~Fault(P0:L2,x);
+0:X0=0; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation);
+0:X0=0; 0:X2=1;  ~Fault(P0:L2,x);
+0:X0=1; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation);
+0:X0=1; 0:X2=1;  ~Fault(P0:L2,x);
+No
+Witnesses
+Positive: 0 Negative: 9
+Condition exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x)))
+Observation coRR+BBM Never 0 9
+Hash=f6ece5ca033543aee1f3f75d5cea8844
+

catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus

@@ -0,0 +1,14 @@
+AArch64 coRR+dsb.ishs-[isb]+PteOA
+Variant=vmsa
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X0=x;
+  1:X2=(oa:PA(y)); 1:X1=PTE(x);
+}
+ P0          | P1          ;
+ LDR W1,[X0] | STR X2,[X1] ; 
+ DSB ISH     |             ;
+ ISB         |             ;
+ LDR W2,[X0] |             ;
+exists(0:X1=2 /\ 0:X2=1)

catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected

@@ -0,0 +1,14 @@
+Test coRR+dsb.ishs-[isb]+PteOA Allowed
+States 4
+0:X1=1; 0:X2=1;
+0:X1=1; 0:X2=2;
+0:X1=2; 0:X2=1;
+0:X1=2; 0:X2=2;
+Ok
+Witnesses
+Positive: 1 Negative: 3
+Flag Warning-BBM-expected
+Condition exists (0:X1=2 /\ 0:X2=1)
+Observation coRR+dsb.ishs-[isb]+PteOA Sometimes 1 3
+Hash=be7e96ca19af00f9ecaab86436e5bdd9
+