[herd] Add tests

Author: maranget

herd/tests/instructions/AArch64.kvm/A031.litmus.expected

@@ -5,9 +5,9 @@ States 3
 1:X5=2; [PTE(z)]=(oa:PA(x));
 Ok
 Witnesses
-Positive: 14 Negative: 0
+Positive: 10 Negative: 0
 Flag requires-BBM
 Condition ~exists ([PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2)
-Observation A031 Never 0 14
+Observation A031 Never 0 10
 Hash=b49f887241d4043b0d917f97925e00ab
 

herd/tests/instructions/AArch64.kvm/A032.litmus

@@ -0,0 +1,14 @@
+AArch64 A032
+Variant=vmsa
+TTHM=HA
+(* Allowed, by two spurious HW updates *)
+{
+int x=1;
+int y=2;
+[PTE(x)]=(oa:PA(x),af:0);
+0:X0=PTE(x); 0:X1=(oa:PA(y),af:0);
+}
+  P0         ;
+ LDR X3,[X0] ;
+ STR X1,[X0] ;
+exists 0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y))

herd/tests/instructions/AArch64.kvm/A032.litmus.expected

@@ -0,0 +1,13 @@
+Test A032 Allowed
+States 4
+0:X3=(oa:PA(x), af:0); [PTE(x)]=(oa:PA(y), af:0);
+0:X3=(oa:PA(x), af:0); [PTE(x)]=(oa:PA(y));
+0:X3=(oa:PA(x)); [PTE(x)]=(oa:PA(y), af:0);
+0:X3=(oa:PA(x)); [PTE(x)]=(oa:PA(y));
+Ok
+Witnesses
+Positive: 2 Negative: 6
+Condition exists (0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y)))
+Observation A032 Sometimes 2 6
+Hash=4d4ebbbbd741d64b8bb4bcece91ef26d
+

herd/tests/instructions/AArch64.kvm/A033.litmus

@@ -0,0 +1,14 @@
+AArch64 A033
+Variant=vmsa
+TTHM=HA
+(* Only 4 exections, tests the "write_loaded" optimisation in herd/mem.ml *)
+{
+  [x]=1;
+  [PTE(x)]=(oa:PA(x),af:0);
+  0:X4=(oa:PA(x),af:0); 0:X5=PTE(x);
+  0:X6=(oa:PA(y));
+}
+ P0              ;
+ CAS X4,X6,[X5]  ;
+locations [PTE(x)]
+exists [PTE(x)]=(oa:PA(x));

herd/tests/instructions/AArch64.kvm/A033.litmus.expected

@@ -0,0 +1,11 @@
+Test A033 Allowed
+States 2
+[PTE(x)]=(oa:PA(x));
+[PTE(x)]=(oa:PA(y));
+Ok
+Witnesses
+Positive: 2 Negative: 2
+Condition exists ([PTE(x)]=(oa:PA(x)))
+Observation A033 Sometimes 2 2
+Hash=3ed88fecb82a1a11276fc0a9dff5afa6
+

herd/tests/instructions/AArch64.kvm/A034.litmus

@@ -0,0 +1,22 @@
+AArch64 A034
+Variant=vmsa
+TTHM=HA
+(*
+ * Test enhanced bounds on spurious HW updates,
+ * Should terminate in decent time.
+ *)
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X1=x; 1:X1=x;
+  1:X4=(oa:PA(x),af: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         ;
+               | CAS X4,X6,[X5]  ;
+exists (0:X0=2 /\ 0:X2=1)

herd/tests/instructions/AArch64.kvm/A034.litmus.expected

@@ -0,0 +1,12 @@
+Test A034 Allowed
+States 3
+0:X0=1; 0:X2=1;
+0:X0=1; 0:X2=2;
+0:X0=2; 0:X2=2;
+No
+Witnesses
+Positive: 0 Negative: 70
+Condition exists (0:X0=2 /\ 0:X2=1)
+Observation A034 Never 0 70
+Hash=0a5d5dfceba07390c6252921dbe58a4f
+

herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg

@@ -17,3 +17,5 @@ nonames A006,F006,F007
 nonames A024,A025
 # Too long to run (copied to the catalogue)
 nonames A031
+# Too long to run
+nonames A034