diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml
index 5edc612d0c..e36244be4a 100644
--- a/herd/AArch64Sem.ml
+++ b/herd/AArch64Sem.ml
@@ -916,7 +916,17 @@ module Make
                    add_setbits (is_zero ipte.af_v) "af:0" set_af m
                  else m
               | Dir.R ->
-                  if ha then
+                  if hd && updatedb then begin
+                    (* The case of a failed CAS with no write, but with a db update *)
+                    M.altT (
+                      add_setbits
+                        (m_op Op.Or (is_zero ipte.af_v) (is_zero ipte.db_v))
+                        "af:0 || db:0"
+                        set_afdb m
+                    )(if ha then
+                        add_setbits (is_zero ipte.af_v) "af:0" set_af m
+                      else m)
+                  end else if ha then
                    add_setbits (is_zero ipte.af_v) "af:0" set_af m
                  else m in
             setbits in
@@ -1455,7 +1465,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 =
@@ -1952,29 +1962,63 @@ 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 mop_fail_no_wb ac ma _ =
+          (* CAS fails, there is no Explicit Write Effect *)
+          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
+          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
+        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 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
+          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 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 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
+          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
+        in
+        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
+            (fun ac ma mv -> M.altT (mop_success ac ma mv) (mop_fail_with_wb ac ma mv))
+           (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            *)
+          (* Whether there is an update to the dirty bit of the TTD is *)
+          (*                                   IMPLEMENTATION SPECIFIC *)
+          (* The combination of Dir.R and true arguments 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
diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml
index 0919867b60..ae60ef0ddc 100644
--- a/herd/eventsMonad.ml
+++ b/herd/eventsMonad.ml
@@ -605,6 +605,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])
@@ -705,6 +739,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
 
diff --git a/herd/monad.mli b/herd/monad.mli
index 614ef15e7d..8d3461f9be 100644
--- a/herd/monad.mli
+++ b/herd/monad.mli
@@ -191,6 +191,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 ->
diff --git a/herd/tests/instructions/AArch64.kvm/A019.litmus b/herd/tests/instructions/AArch64.kvm/A019.litmus
new file mode 100644
index 0000000000..13eb96e493
--- /dev/null
+++ b/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)
diff --git a/herd/tests/instructions/AArch64.kvm/A019.litmus.expected b/herd/tests/instructions/AArch64.kvm/A019.litmus.expected
new file mode 100644
index 0000000000..11b9637c34
--- /dev/null
+++ b/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
+
diff --git a/herd/tests/instructions/AArch64.mixed/M008.litmus.expected b/herd/tests/instructions/AArch64.mixed/M008.litmus.expected
index f4061bba4f..62a410a734 100644
--- a/herd/tests/instructions/AArch64.mixed/M008.litmus.expected
+++ b/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
 
diff --git a/herd/tests/instructions/AArch64/L007.litmus.expected b/herd/tests/instructions/AArch64/L007.litmus.expected
index 26d174e6b2..4fb7cfbd86 100644
--- a/herd/tests/instructions/AArch64/L007.litmus.expected
+++ b/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