diff --git a/Makefile b/Makefile index 0cb9096b92..5366ba9c11 100644 --- a/Makefile +++ b/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) \ diff --git a/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus new file mode 100644 index 0000000000..4442d41283 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected new file mode 100644 index 0000000000..a38d7d2d10 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus new file mode 100644 index 0000000000..28c687d1ce --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected new file mode 100644 index 0000000000..5dd9c9c771 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus new file mode 100644 index 0000000000..bafb26f76f --- /dev/null +++ b/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))) diff --git a/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected new file mode 100644 index 0000000000..638b6df112 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus new file mode 100644 index 0000000000..32d186d274 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected new file mode 100644 index 0000000000..c7e10c7fd1 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus new file mode 100644 index 0000000000..8b6ccea373 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected new file mode 100644 index 0000000000..b90c646963 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus new file mode 100644 index 0000000000..96b760a3d7 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected new file mode 100644 index 0000000000..f9d4f7caad --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus new file mode 100644 index 0000000000..c8f00110d8 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected new file mode 100644 index 0000000000..8da2206f2c --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus new file mode 100644 index 0000000000..d1acce7f11 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected new file mode 100644 index 0000000000..4190f20ca8 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus new file mode 100644 index 0000000000..02f4180681 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected new file mode 100644 index 0000000000..3a8b35f8b1 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus new file mode 100644 index 0000000000..4d03a56550 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected new file mode 100644 index 0000000000..189e8ef0f6 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/coRR+BBM.litmus b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus new file mode 100644 index 0000000000..b1ae195093 --- /dev/null +++ b/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))) diff --git a/catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected new file mode 100644 index 0000000000..ab0fa0a163 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus new file mode 100644 index 0000000000..0b21eb1fd6 --- /dev/null +++ b/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) diff --git a/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected new file mode 100644 index 0000000000..6f55907cb0 --- /dev/null +++ b/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 + diff --git a/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus new file mode 100644 index 0000000000..01a81ccbf0 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus @@ -0,0 +1,15 @@ +AArch64 coRW+Wpteoa-copy +Variant=vmsa +{ + [PTE(z)]=(oa:PA(x)); + 0:X1=z; + 1:X4=(oa:PA(y)); 1:X5=PTE(z); + 1:X7=x; + 1:X8=y; +} + P0 | P1 ; + LDR W0,[X1] | STR X4,[X5] ; + MOV W2,#1 | DSB SY ; + STR W2,[X1] | LDR W6,[X7] ; + | STR W6,[X8] ; +exists(0:X0=1) diff --git a/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected new file mode 100644 index 0000000000..10f19656af --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected @@ -0,0 +1,12 @@ +Test coRW+Wpteoa-copy Allowed +States 2 +0:X0=0; +0:X0=1; +Ok +Witnesses +Positive: 1 Negative: 10 +Flag Warning-BBM-expected +Condition exists (0:X0=1) +Observation coRW+Wpteoa-copy Sometimes 1 10 +Hash=9a8a5039bac4a5d305e3600d23eea57f + diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat index bfeb957ad6..32b1ae8747 100644 --- a/herd/libdir/aarch64.cat +++ b/herd/libdir/aarch64.cat @@ -48,9 +48,6 @@ catdep (* This option says that the cat file computes dependencies *) include "aarch64hwreqs.cat" -(*** Coherence-after ***) -let ca = fr | co - (*** TLBI-after, DC-after, IC-after ***) include "enumerations.cat" with TLBI-after from (all-TLBI-Imp_TTD_R-enums local-hw-reqs) @@ -170,8 +167,8 @@ irreflexive [Exp & Tag & W]; (po & same-loc); [Imp & Tag & R]; (ca & int) as coW empty (rmw & (fr; co)) \ (([Exp]; rmw; [Exp]) & (fri ; [Exp & W]; coi)) as atomic (*** Break Before Make ***) -let BBM = ([TTDV]; ca; [TTDINV]; co; [TTDV]) -flag ~empty (TTD-update-needsBBM & ~BBM) as requires-BBM +let BBM = [TLBCacheableTTD]; ca; [TLBUncacheableTTD]; ob; [TLBI]; ob & inv-scope; [TLBCacheableTTD] +flag ~empty (TTD-update-needsBBM \ BBM) as Warning-BBM-expected (*** Additional synchronisation requirements for CMODX ***) let CMODX-conflicts = same-loc & ( diff --git a/herd/libdir/aarch64bbm.cat b/herd/libdir/aarch64bbm.cat index 79c96e9ad3..1444ce45a4 100644 --- a/herd/libdir/aarch64bbm.cat +++ b/herd/libdir/aarch64bbm.cat @@ -46,43 +46,37 @@ *) include "aarch64memattrs.cat" -(* Can we move this to stdlib? *) -(* Coherence-after *) -let ca = fr | co - -let PTE-MT-update = +let TTD-MT-update = [Normal]; ca; [Device] | [Device]; ca; [Normal] -let PTE-SH-update = +let TTD-SH-update = [NSH]; ca; [ISH | OSH] | [ISH]; ca; [OSH | NSH] | [OSH]; ca; [NSH | ISH] -let PTE-ICH-update = +let TTD-ICH-update = [iNC]; ca; [iWT | iWB] | [iWT]; ca; [iWB | iNC] | [iWB]; ca; [iNC | iWT] -let PTE-OCH-update = +let TTD-OCH-update = [oNC]; ca; [oWT | oWB] | [oWT]; ca; [oWB | oNC] | [oWB]; ca; [oNC | oWT] -let PTE-DT-update = +let TTD-DT-update = [Device-GRE]; ca; [Device-nGRE | Device-nGnRE | Device-nGnRnE] | [Device-nGRE]; ca; [Device-GRE | Device-nGnRE | Device-nGnRnE] | [Device-nGnRE]; ca; [Device-GRE | Device-nGRE | Device-nGnRnE] | [Device-nGnRnE]; ca; [Device-GRE | Device-nGRE | Device-nGnRE] -let PTE-OA-update = ([PTE]; ca; [PTE & oa-changes(PTE, ca^-1)]) -let PTE-OA-update-writable = PTE-OA-update & - ([PTE]; ca; [PTE & at-least-one-writable(PTE, ca^-1)]) +let TTD-OA-update = oa-changes(TTD*TTD) & ca +let TTD-at-least-one-writable = at-least-one-writable(TTD*TTD) -let PTE-update-needsBBM = ([PTEV]; ca \ (ca; [PTEV]; ca); [PTEV]) & - (PTE-MT-update | PTE-SH-update | PTE-ICH-update | PTE-OCH-update | PTE-DT-update - | PTE-OA-update) +let TLBUncacheableTTD = TTDINV | TTDAF0 +let TLBCacheableTTD = TTD \ TLBUncacheableTTD -let TTDV = PTEV -let TTDINV = PTEINV -let TTD-update-needsBBM = PTE-update-needsBBM +let TTD-update-needsBBM = + [TLBCacheableTTD]; (TTD-MT-update | TTD-SH-update | TTD-ICH-update | TTD-OCH-update | TTD-DT-update + | TTD-OA-update & TTD-at-least-one-writable); [TLBCacheableTTD] diff --git a/herd/libdir/aarch64fences.cat b/herd/libdir/aarch64fences.cat index 3ef45cca5d..8296f3cde5 100644 --- a/herd/libdir/aarch64fences.cat +++ b/herd/libdir/aarch64fences.cat @@ -45,5 +45,5 @@ let dsb.full = DSB.NSH | DSB.ISH | DSB.OSH | DSB.SY let dsb.ld = DSB.NSHLD | DSB.ISHLD | DSB.OSHLD | DSB.LD flag ~empty (DSB.NSHLD | DSB.ISHLD | DSB.OSHLD) as Maintenance-scope-for-DSB-LD-is-deprecated let dsb.st = DSB.NSHST | DSB.ISHST | DSB.OSHST | DSB.ST -flag ~empty (DSB.NSHST | DSB.ISHST | DSB.OSHST) as Maintnenace-scope-for-DSB-ST-is-deprecated +flag ~empty (DSB.NSHST | DSB.ISHST | DSB.OSHST) as Maintenance-scope-for-DSB-ST-is-deprecated diff --git a/herd/libdir/aarch64memattrs.cat b/herd/libdir/aarch64memattrs.cat index 27e49fafac..1c689f1aaf 100644 --- a/herd/libdir/aarch64memattrs.cat +++ b/herd/libdir/aarch64memattrs.cat @@ -41,8 +41,6 @@ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -let TTD = PTE - (*** Device Memory ***) (* Device Memory Types *) diff --git a/herd/libdir/aarch64util.cat b/herd/libdir/aarch64util.cat index 9b8a779bdf..411ded9260 100644 --- a/herd/libdir/aarch64util.cat +++ b/herd/libdir/aarch64util.cat @@ -55,12 +55,13 @@ let ii_data = [DATA]; (iico_data|iico_ctrl)+ * -variant vmsa *) -let PTE = if "vmsa" then PTE else emptyset -let PTEV = if "vmsa" then PTEV else emptyset -let PTEINV = if "vmsa" then PTEINV else emptyset +let TTD = if "vmsa" then PTE else emptyset +let TTDV = if "vmsa" then PTEV else emptyset +let TTDINV = if "vmsa" then PTEINV else emptyset +let TTDAF0 = if "vmsa" then PTEAF0 else emptyset let inv-domain = if "vmsa" then inv-domain else 0 -let D-PTE = if "vmsa" then D-PTE else emptyset -let I-PTE = if "vmsa" && "ifetch" then PTE \ D-PTE else emptyset +let D-TTD = if "vmsa" then D-PTE else emptyset +let I-TTD = if "vmsa" && "ifetch" then PTE \ D-PTE else emptyset let AF = if "vmsa" then AF else emptyset let DB = if "vmsa" then DB else emptyset let MMU = if "vmsa" then MMU else emptyset @@ -97,7 +98,6 @@ let IC = IC.IALLUIS | IC.IALLU | IC.IVAU let Imp = NExp let SPONTANEOUS = SPURIOUS let inv-scope = inv-domain -let TTD = PTE let D-TTD = if "vmsa" then D-PTE else emptyset let I-TTD = if "vmsa" then I-PTE else emptyset let Tag = T diff --git a/herd/libdir/catdefinitions.tex b/herd/libdir/catdefinitions.tex index 61a45de749..9532e6012d 100644 --- a/herd/libdir/catdefinitions.tex +++ b/herd/libdir/catdefinitions.tex @@ -98,6 +98,21 @@ % % +\newcommand{\TTDupdateneedsBBMemph}[2]{The TTD update from #1 to #2 needs BBM} +\newcommand{\TTDupdateneedsBBM}[2]{The TTD update from #1 to #2 needs BBM} +\newcommand{\TLBCacheableTTD}[1]{The value of #1 is TLB Cacheable} +\newcommand{\TLBUncacheableTTD}[1]{The value of #1 is TLB Uncacheable} +\newcommand{\TTDV}[1]{The value of #1 is a valid TTD} +\newcommand{\TTDMTupdate}[2]{#1 and #2 specify different memory type} +\newcommand{\TTDDTupdate}[2]{#1 and #2 specify different Device memory type} +\newcommand{\TTDSHupdate}[2]{#1 and #2 specify different Shareability} +\newcommand{\TTDICHupdate}[2]{#1 and #2 specify different inner Cacheability} +\newcommand{\TTDOCHupdate}[2]{#1 and #2 specify different outer Cacheability} +\newcommand{\TTDOAupdate}[2]{#1 and #2 specify different OA} +\newcommand{\TTDatleastonewritable}[2]{Either #1 or #2 grant write permission} +\newcommand{\BBMemph}[2]{There is a \emph{Break-before-make sequence} between #1 and #2} +\newcommand{\BBM}[2]{There is a Break-before-make sequence between #1 and #2} + \newcommand{\Exp}[1]{#1 is an Explicit Effect} \newcommand{\ExpMREof}[1]{the Explicit \MRE{} of #1} \newcommand{\ImpMREof}[1]{the Implicit \MRE{} of #1} diff --git a/herd/libdir/cos.cat b/herd/libdir/cos.cat index d50481a7e9..c045bb0ab3 100644 --- a/herd/libdir/cos.cat +++ b/herd/libdir/cos.cat @@ -5,3 +5,6 @@ if "cos-opt" else include "cos-no-opt.cat" end + +(*** Coherence-after ***) +let ca = fr | co diff --git a/herd/machModelChecker.ml b/herd/machModelChecker.ml index 73a74ac4c9..df388dab8a 100644 --- a/herd/machModelChecker.ml +++ b/herd/machModelChecker.ml @@ -156,24 +156,17 @@ module Make S.A.V.Cst.PteVal.same_oa p1 p2 | _ -> false - let writable2 = - let writable ha hd e = match S.E.value_of e with + let writable2 e1 e2 = + let writable e = + let open DirtyBit in + let ha, hd = match O.dirty with + | Some d -> d.some_ha, d.some_hd + | _ -> false, false in + match S.E.value_of e with | Some (S.A.V.Val (Constant.PteVal p)) -> - S.A.V.Cst.PteVal.writable ha hd p + S.A.V.Cst.PteVal.writable ha hd p | _ -> false in - fun e1 e2 -> - let p = S.E.proc_of e1 in - match p with - | None -> - Warn.user_error - "Init or spurious write as first argument of writable2" - | Some p -> - let ha,hd = - let open DirtyBit in - match O.dirty with - | Some d -> d.ha p,d.hd p - | None -> false,false in - writable ha hd e1 || writable ha hd e2 + writable e1 || writable e2 end diff --git a/herd/tests/instructions/AArch64.kvm/A018.litmus.expected b/herd/tests/instructions/AArch64.kvm/A018.litmus.expected index 4fabaefcb2..590feb72aa 100644 --- a/herd/tests/instructions/AArch64.kvm/A018.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A018.litmus.expected @@ -4,7 +4,7 @@ States 1 Loop Ok Witnesses Positive: 1 Negative: 0 -Flag Maintnenace-scope-for-DSB-ST-is-deprecated +Flag Maintenance-scope-for-DSB-ST-is-deprecated Condition forall (0:X0=1) Observation A018 Always 1 0 Hash=218f088f0c448c84eeeb7c12fcb86c43 diff --git a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected index fef58ad5a4..9b3222b3fd 100644 --- a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected @@ -6,7 +6,7 @@ States 3 Ok Witnesses Positive: 8 Negative: 0 -Flag requires-BBM +Flag Warning-BBM-expected Condition ~exists ([PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2) Observation A031 Never 0 8 Hash=b49f887241d4043b0d917f97925e00ab diff --git a/herd/tests/instructions/AArch64.kvm/A032.litmus.expected b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected index d63c2a24e7..40ae9cf29f 100644 --- a/herd/tests/instructions/AArch64.kvm/A032.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected @@ -7,6 +7,7 @@ States 4 Ok Witnesses Positive: 1 Negative: 5 +Flag Warning-BBM-expected Condition exists (0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y))) Observation A032 Sometimes 1 5 Hash=4d4ebbbbd741d64b8bb4bcece91ef26d diff --git a/herd/tests/instructions/AArch64.kvm/A036.litmus.expected b/herd/tests/instructions/AArch64.kvm/A036.litmus.expected index fd0c770d44..a8ffc6e63a 100644 --- a/herd/tests/instructions/AArch64.kvm/A036.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A036.litmus.expected @@ -6,6 +6,7 @@ Ok Witnesses Positive: 8 Negative: 0 Flag Shareability-argument-for-DMB-is-deprecated +Flag Warning-BBM-expected Condition exists (0:X0=2 /\ 0:X1=1) Observation A036 Always 8 0 Hash=cfe50b9b0465b36af5f17bad83823a0b diff --git a/lib/interpreter.ml b/lib/interpreter.ml index 7ba97995e2..920e498330 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -916,6 +916,17 @@ module Make *) let arg_mismatch () = raise (PrimError "argument mismatch") + let filter_rel f = + function + | V.Rel r -> + V.Rel (E.EventRel.restrict_rel f r) + | V.TransRel tr -> + V.Rel + E.EventRel. + (restrict_rel f @@ transitive_closure tr) + | _ -> arg_mismatch () + + let partition arg = match arg with | Set evts -> let r = U.partition_events evts in @@ -1136,50 +1147,13 @@ module Make and different_values arg = let different_val e1 e2 = not (U.same_value e1 e2) in - match arg with - | V.Rel r -> - let r = E.EventRel.restrict_rel different_val r in - V.Rel r - | V.TransRel tr -> - let r = E.EventRel.transitive_closure tr in - let r = E.EventRel.restrict_rel different_val r in - V.Rel r - | _ -> arg_mismatch () + filter_rel different_val arg - and same_oaRel arg = - match arg with - | V.Rel r -> - V.Rel (E.EventRel.restrict_rel U.same_oa r) - | V.TransRel tr -> - V.Rel - E.EventRel. - (restrict_rel U.same_oa @@ transitive_closure tr) - | _ -> arg_mismatch () + and same_oaRel arg = filter_rel U.same_oa arg - and check_two pred arg = match arg with - | V.Tuple [V.Set ws; (V.Rel _ | V.TransRel _) as prec; ] -> - let m = - match prec with - | V.Rel m -> m - | V.TransRel m -> E.EventRel.transitive_closure m - | _ -> assert false - in - let ws = - E.EventSet.filter - (fun w -> - E.is_store w && E.is_pt w && - begin - match E.EventSet.as_singleton (E.EventRel.succs m w) with - | Some p -> pred w p - (* w does not qualify when zero of two or more prec-related events *) - | None -> false - end) - ws in - V.Set ws - | _ -> arg_mismatch () + and oa_changes arg = filter_rel (fun w p -> not (U.same_oa w p)) arg - let oa_changes = check_two (fun w p -> not (U.same_oa w p)) - and at_least_one_writable = check_two U.writable2 + and at_least_one_writable arg = filter_rel U.writable2 arg let as_transitive = function diff --git a/tools/miaou.ml b/tools/miaou.ml index 4ae9e4c821..04bf235284 100644 --- a/tools/miaou.ml +++ b/tools/miaou.ml @@ -564,7 +564,14 @@ and cons_seqs (fs:exp list) (es:exp list) = List { l with items = List.rev items; } | _ as i -> i end - | e -> + | App (_,Var (_,"domain"), rel) -> + let e3 = Next.next () in + begin match tr_rel e1 e3 rel with + | List ({ items; _ } as l) -> + List { l with items = List.rev items; } + | _ as i -> i + end + | e -> Item (fail (ASTUtils.exp2loc e) "ignoring expression") and tr_evts_not e1 e = notItem (tr_evts e1 e)