[AArch64,herd7] Failed CASP may overwrite memory

herd/AArch64Sem.ml

@@ -1971,7 +1971,6 @@ module Make
         let read_rs = read_reg_data sz rs ii
         and write_rs v = write_reg_sz sz rs v ii in
         let noret = match rs with | AArch64.ZR -> true | _ -> false in
-        let is_phy ac = Access.is_physical ac in
         let branch a =
           let cond = Printf.sprintf "[%s]==%d:%s" (V.pp_v a) ii.A.proc (A.pp_reg rs) in
             commit_pred_txt (Some cond) ii in
@@ -1980,7 +1979,7 @@ module Make
           let read_mem a =
             if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii
             else do_read_mem_ret sz an aexp ac a ii in
-          M.aarch64_cas_no (is_phy ac) ma read_rs write_rs read_mem branch M.neqT
+          M.aarch64_cas_no (Access.is_physical ac) ma read_rs write_rs read_mem branch M.neqT
         in
         let mop_fail_with_wb ac ma _ =
           (* CAS fails, there is an Explicit Write Effect writing back *)
@@ -1989,7 +1988,7 @@ module Make
             if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii
             else rmw_amo_read sz rmw ac a ii
           and write_mem a v = rmw_amo_write sz rmw ac a v ii in
-          M.aarch64_cas_no_with_writeback (is_phy ac) ma read_rs write_rs
+          M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs write_rs
                                       read_mem write_mem branch M.neqT
         in
         let mop_success ac ma mv =
@@ -2001,27 +2000,28 @@ module Make
             if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii
             else rmw_amo_read sz rmw ac a ii
           and write_mem a v = rmw_amo_write sz rmw ac a v ii in
-          M.aarch64_cas_ok (is_phy ac) ma read_rs read_rt write_rs
+          M.aarch64_cas_ok (Access.is_physical ac) ma read_rs read_rt write_rs
                                 read_mem write_mem branch M.eqT
         in
         M.altT (
           (* CAS succeeds and generates an Explicit Write Effect *)
           (* there must be an update to the dirty bit of the TTD *)
-          lift_memop rn Dir.W true memtag mop_success
-           (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
+          lift_memop rn Dir.W true memtag mop_success (to_perms "rw" sz)
+            (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
         )( (* CAS fails *)
           M.altT (
             (* CAS generates an Explicit Write Effect              *)
             (* there must be an update to the dirty bit of the TTD *)
-            lift_memop rn Dir.W true memtag mop_fail_with_wb
-            (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
+            lift_memop rn Dir.W true memtag mop_fail_with_wb (to_perms "rw" sz)
+              (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
           )(
             (* CAS does not generate an Explicit Write Effect          *)
             (* It is IMPLEMENTATION SPECIFIC if there is an update to  *)
             (*                                the dirty bit of the TTD *)
             (* Note: the combination of dir=Dir.R and updatedb=true    *)
             (*                    triggers an alternative in check_ptw *)
-            lift_memop rn Dir.R true memtag mop_fail_no_wb (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
+            lift_memop rn Dir.R true memtag mop_fail_no_wb (to_perms "rw" sz)
+              (read_reg_ord rn ii) (read_reg_data sz rt ii) an ii
           )
         )
 
@@ -2037,37 +2037,77 @@ module Make
           let cond = Printf.sprintf "[%s]=={%d:%s,%d:%s}" (V.pp_v a)
             ii.A.proc (A.pp_reg rs1) ii.A.proc (A.pp_reg rs1) in
           commit_pred_txt (Some cond) ii in
-        lift_memop rn Dir.W true memtag
-          (fun ac ma _ ->
-            let is_phy = Access.is_physical ac in
-             M.altT
-              (let read_mem a = do_read_mem_ret sz an aexp ac a ii
+        let neqp (v1,v2) (x1,x2) =
+            M.op Op.Eq v1 x1 >>| M.op Op.Eq v2 x2
+            >>= fun (b1,b2) -> M.op Op.And b1 b2
+            >>= M.eqT V.zero
+        and eqp (v1,v2) (x1,x2) =
+            M.eqT v1 x1 >>| M.eqT v2 x2
+            >>= fun _ -> M.unitT () in
+        let mop_fail_no_wb ac ma _ =
+          (* CASP fails, there are no Explicit Write Effects *)
+          let read_mem a = do_read_mem_ret sz an aexp ac a ii
                 >>| (add_size a sz
                 >>= fun a -> do_read_mem_ret sz an aexp ac a ii) in
-               let neqp (v1,v2) (x1,x2) =
-                 M.op Op.Eq v1 x1 >>| M.op Op.Eq v2 x2
-                 >>= fun (b1,b2) -> M.op Op.And b1 b2
-                 >>= M.eqT V.zero in
-               M.aarch64_cas_no is_phy ma read_rs write_rs read_mem branch neqp)
-              (let read_rt = read_reg_data sz rt1 ii
+          M.aarch64_cas_no (Access.is_physical ac) ma read_rs
+              write_rs read_mem branch neqp
+        in
+        let mop_fail_with_wb ac ma _ =
+          (* CASP fails, there are Explicit Write Effects writing back *)
+          (* the value that is already in memory                       *)
+          let read_mem a = do_read_mem_ret sz an aexp ac a ii
+                >>| (add_size a sz
+                >>= fun a -> do_read_mem_ret sz an aexp ac a ii)
+          and write_mem a (v1,v2) =
+              rmw_amo_write sz rmw ac a v1 ii
+              >>| (add_size a sz >>= fun a2 ->
+                  rmw_amo_write sz rmw ac a2 v2 ii)
+              >>= fun _ -> M.unitT () in
+          M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs
+              write_rs read_mem write_mem branch neqp
+        in
+        let mop_success ac ma _ =
+          (* CASP succeeds, there are Explicit Write Effects *)
+          let read_rt = read_reg_data sz rt1 ii
                 >>| read_reg_data sz rt2 ii
-               and read_mem a = rmw_amo_read sz rmw ac a ii
+          and read_mem a = rmw_amo_read sz rmw ac a ii
                 >>| (add_size a sz
                 >>= fun a -> rmw_amo_read sz rmw ac a ii)
-               and write_mem a (v1,v2) =
-                   rmw_amo_write sz rmw ac a v1 ii
-                   >>| (add_size a sz >>= fun a2 ->
-                       rmw_amo_write sz rmw ac a2 v2 ii)
-                   >>= fun _ -> M.unitT ()
-               and eqp (v1,v2) (x1,x2) =
-                 M.eqT v1 x1 >>| M.eqT v2 x2
-                 >>= fun _ -> M.unitT () in
-               M.aarch64_cas_ok is_phy ma read_rs read_rt write_rs
-                 read_mem write_mem branch eqp))
-          (to_perms "rw" sz)
-          (read_reg_ord rn ii)
-          (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii)
-        an ii
+          and write_mem a (v1,v2) =
+              rmw_amo_write sz rmw ac a v1 ii
+              >>| (add_size a sz >>= fun a2 ->
+                  rmw_amo_write sz rmw ac a2 v2 ii)
+              >>= fun _ -> M.unitT () in
+          M.aarch64_cas_ok (Access.is_physical ac) ma read_rs
+              read_rt write_rs read_mem write_mem branch eqp
+        in
+        M.altT (
+          (* CASP succeeds and generates Explicit Write Effects  *)
+          (* there must be an update to the dirty bit of the TTD *)
+          lift_memop rn Dir.W true memtag mop_success
+            (to_perms "rw" sz) (read_reg_ord rn ii)
+            (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii)
+            an ii
+        )( (* CASP fails *)
+          M.altT (
+            (* CASP generates Explicit Write Effects               *)
+            (* there must be an update to the dirty bit of the TTD *)
+            lift_memop rn Dir.W true memtag mop_fail_with_wb
+              (to_perms "rw" sz) (read_reg_ord rn ii)
+              (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii)
+              an ii
+          )(
+            (* CASP does not generate Explicit Write Effects           *)
+            (* It is IMPLEMENTATION SPECIFIC if there is an update to  *)
+            (*                                the dirty bit of the TTD *)
+            (* Note: the combination of dir=Dir.R and updatedb=true    *)
+            (*                    triggers an alternative in check_ptw *)
+            lift_memop rn Dir.R true memtag mop_fail_no_wb
+              (to_perms "rw" sz) (read_reg_ord rn ii)
+              (read_reg_data sz rt1 ii >>> fun _ -> read_reg_data sz rt2 ii)
+              an ii
+          )
+        )
 
       (* Temporary morello variation of CAS *)
       let cas_morello sz rmw rs rt rn ii =

herd/tests/instructions/AArch64/A242.litmus.expected

@@ -3,8 +3,8 @@ States 1
 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0;
 Ok
 Witnesses
-Positive: 16 Negative: 0
+Positive: 36 Negative: 0
 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2)
-Observation A242 Always 16 0
+Observation A242 Always 36 0
 Hash=a53545f0a258acc581288f0aa9b5c936
 

herd/tests/instructions/AArch64/A243.litmus.expected

@@ -3,8 +3,8 @@ States 1
 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0;
 Ok
 Witnesses
-Positive: 16 Negative: 0
+Positive: 36 Negative: 0
 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2)
-Observation A243 Always 16 0
+Observation A243 Always 36 0
 Hash=450d6bea2cb06cb6a4eec6037dcb6802
 

herd/tests/instructions/AArch64/A244.litmus.expected

@@ -3,8 +3,8 @@ States 1
 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0;
 Ok
 Witnesses
-Positive: 16 Negative: 0
+Positive: 36 Negative: 0
 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2)
-Observation A244 Always 16 0
+Observation A244 Always 36 0
 Hash=f5f65af42b0b1c4ef91a867eb4c84a3c
 

herd/tests/instructions/AArch64/A245.litmus.expected

@@ -3,8 +3,8 @@ States 1
 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0;
 Ok
 Witnesses
-Positive: 16 Negative: 0
+Positive: 36 Negative: 0
 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2)
-Observation A245 Always 16 0
+Observation A245 Always 36 0
 Hash=51b29db6588f853cf4e04fe2a1242893
 

herd/tests/instructions/AArch64/A246.litmus.expected

@@ -3,8 +3,8 @@ States 1
 a[0]=2; a[1]=2; x[0]=0; x[1]=0; y[0]=2; y[1]=2; z[0]=0; z[1]=0;
 Ok
 Witnesses
-Positive: 16 Negative: 0
+Positive: 36 Negative: 0
 Condition forall (x[0]=0 /\ x[1]=0 /\ y[0]=2 /\ y[1]=2 /\ z[0]=0 /\ z[1]=0 /\ a[0]=2 /\ a[1]=2)
-Observation A246 Always 16 0
+Observation A246 Always 36 0
 Hash=dfcdd105748ed1fb63dad2657811b691
 

herd/tests/instructions/AArch64/L056.litmus.expected

@@ -4,8 +4,8 @@ States 2
 1:X0=1; 1:X1=0; x={1,0};
 Ok
 Witnesses
-Positive: 4 Negative: 0
+Positive: 6 Negative: 0
 Condition forall (x={1,0} \/ x={1,2})
-Observation L056 Always 4 0
+Observation L056 Always 6 0
 Hash=56239ea29c96ee505c91efa59ac63a18
 

herd/tests/instructions/AArch64/L057.litmus.expected

@@ -4,8 +4,8 @@ States 2
 1:X0=0; 1:X1=1; x={0,1};
 Ok
 Witnesses
-Positive: 4 Negative: 0
+Positive: 6 Negative: 0
 Condition forall (x={0,1} \/ x={2,1})
-Observation L057 Always 4 0
+Observation L057 Always 6 0
 Hash=57ac32621316eec60874e7e2c863b043