[AArch64,herd7] Failed CAS may overwrite memory

Includes review suggestions from: Hadrien Renaud <[email protected]>

herd/AArch64Sem.ml

@@ -911,20 +911,31 @@ module Make
                        fun _ -> set a_pte pte_v ii)
                  >>== fun () -> M.unitT (pte_v,ipte))
                no in
+            let add_setbits_db ipte m =
+              add_setbits
+                (m_op Op.Or (is_zero ipte.af_v) (is_zero ipte.db_v))
+                "af:0 || db:0"
+                set_afdb m in
+            let add_setbits_af ipte m =
+              add_setbits (is_zero ipte.af_v) "af:0" set_af m in
             let setbits =
               match dir with
               | Dir.W ->
                  if hd && updatedb then
-                   add_setbits
-                     (m_op Op.Or (is_zero ipte.af_v) (is_zero ipte.db_v))
-                     "af:0 || db:0"
-                     set_afdb m
+                   add_setbits_db ipte m
                  else if ha then
-                   add_setbits (is_zero ipte.af_v) "af:0" set_af m
+                   add_setbits_af ipte m
                  else m
               | Dir.R ->
-                  if ha then
-                   add_setbits (is_zero ipte.af_v) "af:0" set_af m
+                  if hd && updatedb then
+                    (* The case of a failed CAS with no write, but with a db update *)
+                    M.altT (
+                      add_setbits_db ipte m
+                    )( (* no need to check ha, because hd implies ha *)
+                      add_setbits_af ipte m
+                    )
+                  else if ha then
+                    add_setbits_af ipte m
                  else m in
             setbits in
           mok m a in
@@ -1462,7 +1473,7 @@ module Make
 
       let do_ldr rA sz an mop ma ii =
 (* Generic load *)
-        lift_memop rA Dir.R true memtag
+        lift_memop rA Dir.R false memtag
           (fun ac ma _mv -> (* value fake here *)
             let open Precision in
             let memtag_sync =
@@ -1959,29 +1970,60 @@ module Make
         let an = rmw_to_read rmw in
         let read_rs = read_reg_data sz rs ii
         and write_rs v = write_reg_sz sz rs v ii in
-        lift_memop rn Dir.W true memtag
+        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
+        let mop_fail_no_wb ac ma _ =
+          (* CAS fails, there is no Explicit Write Effect *)
+          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
+        in
+        let mop_fail_with_wb ac ma _ =
+          (* CAS fails, there is an Explicit Write Effect writing back *)
+          (* the value that is already in memory                       *)
+          let read_mem a =
+            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
+                                      read_mem write_mem branch M.neqT
+        in
+        let mop_success ac ma mv =
+          (* CAS succeeds, there is an Explicit Write Effect *)
            (* mv is read new value from reg, not important
               as this code is not executed in morello mode *)
-          (fun ac ma mv ->
-             let noret = match rs with | AArch64.ZR -> true | _ -> false in
-             let is_phy = 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
-             M.altT
-              (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 ma read_rs write_rs read_mem branch M.neqT)
-              (let read_rt = mv
-               and read_mem a =
-                 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 ma read_rs read_rt write_rs
-                 read_mem write_mem branch M.eqT))
-          (to_perms "rw" sz) (read_reg_ord rn ii) (read_reg_data sz rt ii)
-        an ii
+          let read_rt = mv
+          and read_mem a =
+            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
+                                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
+        )( (* 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
+          )(
+            (* 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
+          )
+        )
 
       let casp sz rmw rs1 rs2 rt1 rt2 rn ii =
         let an = rmw_to_read rmw in

herd/eventsMonad.ml

@@ -611,6 +611,40 @@ Monad type:
           acts_rn (eiid,Evt.empty) in
       eiid,(acts, None)
 
+    let do_aarch64_cas_no_with_writeback
+        (is_physical:bool)
+        (read_rn:'loc t) (read_rs:'v t)
+        (write_rs:'v-> unit t)
+        (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t)
+        (branch: 'loc -> unit t)
+        (rne: 'v -> 'v -> unit t)
+        eiid =
+      let eiid,read_rn = read_rn eiid in
+      let eiid,read_rs = read_rs eiid in
+      let cv,cl_cv,es_rs = Evt.as_singleton_nospecul read_rs in
+      let acts_rn,spec = read_rn in
+      assert (Misc.is_none spec) ;
+      let eiid,acts =
+        Evt.fold
+          (fun (a,cl_a,es_rn) (eiid,acts) ->
+            let eiid,read_mem = read_mem a eiid in
+            let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem in
+            let eiid,write_mem = write_mem a ov eiid in
+            let (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in
+            let eiid,write_rs = write_rs ov eiid in
+            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
+            let eiid,branch = branch a eiid in
+            let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
+            let eiid,nem = rne ov cv eiid in
+            let (),cl_ne,eseq =  Evt.as_singleton_nospecul nem in
+            assert (E.is_empty_event_structure eseq) ;
+            let es =
+              E.aarch64_cas_ok is_physical `DataFromRx es_rn es_rs E.empty_event_structure es_wrs es_rm es_wm es_br in
+            let cls = cl_a@cl_cv@cl_rm@cl_wm@cl_wrs@cl_br@cl_ne  in
+            eiid,Evt.add ((),cls,es) acts)
+          acts_rn (eiid,Evt.empty) in
+      eiid,(acts, None)
+
 (* AArch64 successful cas *)
     let do_aarch64_cas_ok
         (is_physical:bool) (prov_data: [`DataFromRRs | `DataFromRx])
@@ -711,6 +745,12 @@ Monad type:
       in
       altT (do_ true) (do_ false)
 
+    let aarch64_cas_no_with_writeback (is_physical: bool) (read_rn: 'loc t)
+        (read_rs: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t)
+        (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (rne: 'v -> 'v -> unit t) =
+      do_aarch64_cas_no_with_writeback is_physical read_rn read_rs
+          write_rs read_mem write_mem branch rne
+
     (* RISCV store conditional may always succeed? *)
     let riscv_store_conditional = aarch64_or_riscv_store_conditional false
 

herd/monad.mli

@@ -211,6 +211,13 @@ module type S =
            ('loc -> unit t) ->
             ('v -> 'v -> unit t) -> unit t
 
+    val aarch64_cas_no_with_writeback :
+          bool -> (* physical access *)
+            'loc t -> 'v t ->
+              ('v -> unit t) -> ('loc -> 'v t) -> ('loc -> 'v -> unit t) ->
+              ('loc -> unit t) ->
+                ('v -> 'v -> unit t) -> unit t
+
     val aarch64_cas_ok :
       bool -> (* physical access *)
         'loc t -> 'v t -> 'v t ->

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syh2h0+amo.casa.w0w0-pow0w0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X3=0x1010000; [y]=0x2020202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020202 /\ 1:X1=0x101 /\ 1:X3=0x0)
-Observation MP+dmb.syh2h0+amo.casa.w0w0-pow0w0 Never 0 6
+Observation MP+dmb.syh2h0+amo.casa.w0w0-pow0w0 Never 0 8
 Hash=de0b51dd0baeae300ccb7bb64c89c67f
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syh2h2+amo.casa.w0w0-pow0w0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X2=0x1010000; 1:X4=0x1010000; [y]=0x2020202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020202 /\ 1:X2=0x1010000 /\ 1:X4=0x0)
-Observation MP+dmb.syh2h2+amo.casa.w0w0-pow0w0 Never 0 6
+Observation MP+dmb.syh2h2+amo.casa.w0w0-pow0w0 Never 0 8
 Hash=ccd1563306b43f28d7565b33bc2812c4
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syh2w0+amo.casa.h0h0-poh0w0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X3=0x1010000; [y]=0x1010202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x1010202 /\ 1:X1=0x101 /\ 1:X3=0x0)
-Observation MP+dmb.syh2w0+amo.casa.h0h0-poh0w0 Never 0 6
+Observation MP+dmb.syh2w0+amo.casa.h0h0-poh0w0 Never 0 8
 Hash=91643c1d02ebd53a9c3fb07ad22b176e
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syh2w0+amo.casa.h2h2-poh2w0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X4=0x1010000; [y]=0x2020101;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020101 /\ 1:X1=0x101 /\ 1:X4=0x0)
-Observation MP+dmb.syh2w0+amo.casa.h2h2-poh2w0 Never 0 6
+Observation MP+dmb.syh2w0+amo.casa.h2h2-poh2w0 Never 0 8
 Hash=a505ef52a19e87a874d77d613b2644a1
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syw0h0+amo.casa.w0w0-pow0h0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X3=0x101; [y]=0x2020202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020202 /\ 1:X1=0x101 /\ 1:X3=0x0)
-Observation MP+dmb.syw0h0+amo.casa.w0w0-pow0h0 Never 0 6
+Observation MP+dmb.syw0h0+amo.casa.w0w0-pow0h0 Never 0 8
 Hash=012860ecc04db3a0c0cca4401aa0a718
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syw0h2+amo.casa.w0w0-pow0h0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X2=0x1010000; 1:X4=0x101; [y]=0x2020202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020202 /\ 1:X2=0x1010000 /\ 1:X4=0x0)
-Observation MP+dmb.syw0h2+amo.casa.w0w0-pow0h0 Never 0 6
+Observation MP+dmb.syw0h2+amo.casa.w0w0-pow0h0 Never 0 8
 Hash=ce2a7c8ea6503ba5f9bc7011832e680e
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syw0w0+amo.casa.h0h0-poh0h0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X3=0x101; [y]=0x1010202;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x1010202 /\ 1:X1=0x101 /\ 1:X3=0x0)
-Observation MP+dmb.syw0w0+amo.casa.h0h0-poh0h0 Never 0 6
+Observation MP+dmb.syw0w0+amo.casa.h0h0-poh0h0 Never 0 8
 Hash=9f7ea35957b7fcaa3c120cad7b8ed304
 

herd/tests/diycross/AArch64.mixed.strict/MP+dmb.syw0w0+amo.casa.h2h2-poh2h0.litmus.expected

@@ -5,8 +5,8 @@ States 3
 1:X1=0x101; 1:X4=0x101; [y]=0x2020101;
 No
 Witnesses
-Positive: 0 Negative: 6
+Positive: 0 Negative: 8
 Condition exists ([y]=0x2020101 /\ 1:X1=0x101 /\ 1:X4=0x0)
-Observation MP+dmb.syw0w0+amo.casa.h2h2-poh2h0 Never 0 6
+Observation MP+dmb.syw0w0+amo.casa.h2h2-poh2h0 Never 0 8
 Hash=27e2a650c1b171931160eba3ded2ec7c
 

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

@@ -0,0 +1,10 @@
+AArch64 A019
+TTHM=P0:HD
+Variant=vmsa
+{
+ 0:X1=x; 0:X2=7; 0:X0=42;
+ TTD(x)=(oa:PA(x),db:0,dbm:1);
+}
+P0             ;
+CAS W0,W2,[X1] ;
+exists TTD(x)=(oa:PA(x),db:0,dbm:1)

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

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

herd/tests/instructions/AArch64.mixed/M008.litmus.expected

@@ -6,8 +6,8 @@ States 4
 1:X1=0x101; [x]=0x2; [y]=0x202;
 Ok
 Witnesses
-Positive: 2 Negative: 6
+Positive: 2 Negative: 8
 Condition exists ([x]=0x2 /\ [y]=0x202 /\ 1:X1=0x101)
-Observation M008 Sometimes 2 6
+Observation M008 Sometimes 2 8
 Hash=dce7776cf1382a6e5b1afce5eab68a83
 

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

@@ -3,8 +3,8 @@ States 1
 0:X3=0; 1:X3=0; [x]=0; [y]=2;
 Ok
 Witnesses
-Positive: 4 Negative: 0
+Positive: 6 Negative: 0
 Condition forall ([x]=0 /\ [y]=2)
-Observation L007 Always 4 0
+Observation L007 Always 6 0
 Hash=dcd669f7a9ed4f2e408f12673d09b57f