[herd] Global count of necessary spurious updates

When TTHM=HA or TTHM=HD are active, HW update of the AF flag
is performed. This include the so-called "spurious" updates
that are performed independently of test code.

For efficiency reason we limit the number of such spurious
updates to what is necessary. We do so by a global
scan of the execution candidates  counting the
writes that may unset the AF flag in the final
set of effects. Notice that we also consider the
initial writes in this scan.

We perform one optimisation: by exception, when a
write effect value is the same as the value
read by the same instruction from the same location,
there is no need to add a supplementary spurious update
as the (potential) update associated to the write that
stored the value has already been counted and is sufficient.

Author: maranget

herd/AArch64ASLSem.ml

@@ -87,6 +87,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
 
   module Mixed (SZ : ByteSize.S) : sig
     val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+    val can_unset_af_loc : event -> V.v option
     val spurious_setaf : V.v -> unit M.t
   end = struct
     module AArch64Mixed = AArch64S.Mixed (SZ)
@@ -1392,36 +1393,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
 
       let tr_cnstrnts cs = List.fold_left tr_cnstrnt [] cs
 
-
-      let dirty =
-        match TopConf.dirty with
-        | None -> DirtyBit.soft
-        | Some d -> d
-
-      let check_spurious ii =
-        (*
-         * Explicit loads or stores yield a potential spurious update of
-         * the AF flag. When the hardware feature is active, of course.
-         *)
-        if dirty.DirtyBit.ha ii.A.proc then
-          let dir_ok =
-            let open Dir in
-            if TopConf.C.variant Variant.PhantomOnLoad then
-              (function R -> true | W -> false)
-            else
-              (function W -> true | R -> false) in
-          fun act ->
-            match act with
-            | Act.Access
-                (dir,A.Location_global loc,_,_,
-                 AArch64Explicit.Exp,_,Access.(PHY_PTE|PTE DISide.Data))
-              when dir_ok dir
-              ->
-                Some loc
-            | _ -> None
-        else  fun _ -> None
-
-      let event_to_monad ii check_spurious is_bcc get_port event =
+      let event_to_monad ii is_bcc get_port event =
         let { ASLE.action; ASLE.iiid; _ } = event in
         let () =
           if _dbg then
@@ -1446,8 +1418,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
               |> M.as_port (get_port event)
               |> M.force_once
             in
-            let check_af = check_spurious action' in
-            Some (event, (check_af,m))
+            Some (event,m)
 
       let rel_to_monad event_to_monad_map comb rel =
         let one_pair (e1, e2) =
@@ -1497,17 +1468,10 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           fun e -> ASLE.EventSet.mem e bcc in
         let () = if _dbg then Printf.eprintf "\t- events: " in
         let event_list = List.of_seq events in
-        let check_spurious = check_spurious ii in
-        let spurious_locs,event_to_monad_map =
+        let event_to_monad_map =
           let seq =
-            Seq.filter_map (event_to_monad ii check_spurious is_bcc get_port) events in
-          let locs =
-            Seq.filter_map (fun (_,(loc,_))  -> loc) seq
-            |> List.of_seq
-          and map =
-            Seq.map (fun (e,(_,m)) -> (e,m)) seq
-            |> EMap.of_seq in
-          locs,map
+            Seq.filter_map (event_to_monad ii is_bcc get_port) events in
+          EMap.of_seq seq
         in
         let events_m =
           let folder _e1 m1 acc = m1 ||| acc in
@@ -1604,18 +1568,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           M.restrict (tr_cnstrnts cs)
         in
         let () = if _dbg then Printf.eprintf "\n" in
-        let m_spurious =
-          (*
-           * At most one spurious setaf operation per relevant location
-           * is probably sufficient. Anyway, it is unlikely that a given
-           * value appears more than once in the spurious_locs list.
-           *)
-          List.fold_left
-            (fun m loc ->
-               M.altT (AArch64Mixed.spurious_setaf loc) (M.unitT ()) ||| m)
-            (M.unitT ()) @@ List.sort_uniq A.V.compare spurious_locs in
         let* () =
-          m_spurious ||| events_m ||| iico_data ||| iico_ctrl
+          events_m ||| iico_data ||| iico_ctrl
           ||| iico_order ||| constraints ||| M.restrict eqs_test
         in
         M.addT (A.next_po_index ii.A.program_order_index) (return branch)
@@ -1777,6 +1731,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           AArch64Mixed.build_semantics test ii
       | _ -> asl_build_semantics test ii
 
+    let can_unset_af_loc e = AArch64Mixed.can_unset_af_loc e
     let spurious_setaf v = AArch64Mixed.spurious_setaf v
   end
 end

herd/AArch64Sem.ml

@@ -105,6 +105,7 @@ module Make
     (* Semantics proper *)
     module Mixed(SZ:ByteSize.S) : sig
       val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+      val can_unset_af_loc : event -> V.v option
       val spurious_setaf : V.v -> unit M.t
     end = struct
 
@@ -1120,14 +1121,15 @@ module Make
               check_cond cond)
           end in
         if pte2 then  mvirt
-        else
-          M.op1 Op.IsVirtual a_virt >>= fun cond ->
-          M.choiceT cond mvirt
+        else begin
+          let mdirect =
             (* Non-virtual accesses are disallowed from EL0.
                For instance, user code cannot access the page table. *)
-            (if is_el0 then mk_pte_fault a_virt ma dir an ii domain
-             else mdirect)
-
+            if is_el0 then mk_pte_fault a_virt ma dir an ii domain
+            else mdirect in
+          M.op1 Op.IsVirtual a_virt >>= fun cond ->
+          M.choiceT cond mvirt mdirect
+        end
 (* Read memory, return value read *)
       let do_read_mem_ret sz an anexp ac a ii =
         let m a =
@@ -1444,25 +1446,22 @@ module Make
 
 (* KVM mode *)
 
-      let some_ha = dirty.DirtyBit.some_ha || dirty.DirtyBit.some_hd
+      let can_be_pt v =
+        match V.as_constant v with
+        | None -> true
+        | Some c -> Constant.is_pt c
 
-      let fire_spurious_af dir a m domain =
-        if
-          some_ha &&
-            (let v = C.variant Variant.PhantomOnLoad in
-             match dir with Dir.W -> not v | Dir.R -> v)
-        then
-          (m >>|
-             M.altT (test_and_set_af_succeeds a E.IdSpurious domain) (M.unitT ())) >>=
-            fun (r,_) -> M.unitT r
-        else m
+      let can_af0 v =
+        (match V.as_constant v with
+        | Some (Constant.PteVal p) ->
+           p.AArch64PteVal.valid <> 0 &&  p.AArch64PteVal.af = 0
+        | _ -> true)
 
-      let lift_kvm dir updatedb mop ma an ii mphy branch domain =
+      let lift_kvm _tag dir updatedb mop ma an ii mphy branch domain =
         let mfault ma a ft = emit_fault a ma dir an ft None ii in
         let maccess a ma =
           check_ptw ii.AArch64.proc dir updatedb false a ma an ii
-            ((let m = mop (Access.PTE domain) ma in
-              fire_spurious_af dir a m domain) |> branch)
+            (mop (Access.PTE domain) ma |> branch)
             mphy
             mfault
             domain in
@@ -1515,8 +1514,7 @@ module Make
           (* tag checks only apply to data *)
           let domain = DISide.Data in
           let mdirect =
-            let m = mop (Access.PTE domain) ma in
-            fire_spurious_af dir a m domain >>= M.ignore >>= B.next1T in
+            mop (Access.PTE domain) ma >>= M.ignore >>= B.next1T in
           check_ptw ii.AArch64.proc Dir.R false true a ma an ii
             mdirect
             cond_check_tag
@@ -1617,7 +1615,7 @@ Arguments:
               when translating for instruction fetches.
 - domain:     Whether the translation is for data or instruction access.
 *)
-      let do_lift_memop rA (* Base address register *)
+      let do_lift_memop ?tag rA (* Base address register *)
             dir updatedb checked mop perms ma mv an ii branch domain =
         if morello then
           lift_morello mop perms ma mv dir an ii branch
@@ -1630,15 +1628,15 @@ Arguments:
                 M.op1 Op.IsVirtual a_virt >>= fun c ->
                 M.choiceT c
                   (mop Access.PHY ma)
-                  (fire_spurious_af dir a_virt (mop Access.PHY_PTE ma) domain) |> branch
+                  (mop Access.PHY_PTE ma)
+                |> branch
               else
-                mop Access.PHY ma
-                |> branch in
+                mop Access.PHY ma |> branch in
             let mphy =
               if checked then lift_memtag_phy dir mop ma an ii mphy
               else mphy
             in
-            let m = lift_kvm dir updatedb mop ma an ii mphy branch domain in
+            let m = lift_kvm tag dir updatedb mop ma an ii mphy branch domain in
             (* M.short will add an iico_data only if memtag is enabled *)
             M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m
           else if pac then
@@ -1648,10 +1646,10 @@ Arguments:
           else
             mop Access.VIR ma |> branch
 
-      let lift_memop rA (* Base address register *)
+      let lift_memop ?(tag = "") rA (* Base address register *)
             dir updatedb checked mop perms ma mv an ii =
         let domain = DISide.Data in
-        do_lift_memop rA dir updatedb checked mop perms ma mv an ii
+        do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii
           (fun a -> a >>= M.ignore >>= B.next1T) domain
 
       (* Address translation instruction *)
@@ -1679,8 +1677,7 @@ Arguments:
         let domain = DISide.Data in
         let maccess a ma =
           check_ptw ii.AArch64.proc dir false false a ma Annot.N ii
-            ((let m = mop (Access.PTE domain) ma in
-              fire_spurious_af dir a m domain) >>= M.ignore >>= B.next1T)
+            (mop (Access.PTE domain) ma >>= M.ignore >>= B.next1T)
             mphy
             mfault
             domain in
@@ -1694,7 +1691,7 @@ Arguments:
           if memtag && C.mte_store_only then
             ma >>= fun a -> loc_extract a
           else ma in
-        lift_memop rA Dir.R false checked
+        lift_memop ~tag:"LD" rA Dir.R false checked
           (fun ac ma _mv -> (* value fake here *)
             let open Precision in
             let memtag_sync =
@@ -1709,7 +1706,7 @@ Arguments:
 
 (* Generic store *)
       let do_str rA mop sz an ma mv ii =
-        lift_memop rA Dir.W true memtag
+        lift_memop ~tag:"ST" rA Dir.W true memtag
           (fun ac ma mv ->
             let open Precision in
             let memtag_sync = memtag && C.mte_precision = Synchronous in
@@ -1994,12 +1991,12 @@ Arguments:
 
       let str_simple sz rs rd m_ea ii =
         do_str rd
-          (fun ac a _ ii ->
-               M.data_input_next
-                 (read_reg_data_sz sz rs ii)
-                 (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
+          (fun ac a v ii ->
+            M.data_input_next
+              (M.unitT v)
+              (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
           sz Annot.N
-          m_ea  (M.unitT V.zero) ii
+          m_ea (read_reg_data_sz sz rs ii) ii
 
       let str sz rs rd e ii =
         let open AArch64Base in
@@ -2013,14 +2010,14 @@ Arguments:
                (read_reg_addr rd ii)
                (fun a_virt ma ->
                  do_str rd
-                   (fun ac a _ ii ->
+                   (fun ac a v ii ->
                      M.add a_virt (V.intToV k) >>= fun b -> write_reg rd b ii
                      >>|
                      M.data_input_next
-                       (read_reg_data_sz sz rs ii)
+                       (M.unitT v)
                        (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
                    sz Annot.N
-                   ma (M.unitT V.zero) ii) in
+                   ma (read_reg_data_sz sz rs ii) ii) in
            if kvm then M.upOneRW (is_this_reg rd) m
            else m
         | Imm (k,PreIdx) ->
@@ -2117,9 +2114,9 @@ Arguments:
               (write_reg ResAddr V.zero ii)
               (fun v -> write_reg rr v ii)
               (mw an ac))
-              (to_perms "w" sz)
-              (read_reg_addr rd ii)
-              ms an ii
+          (to_perms "w" sz)
+          (read_reg_addr rd ii)
+          ms an ii
 
       let stxr sz t rr rs rd ii =
         do_stxr
@@ -2193,7 +2190,7 @@ Arguments:
               (* Dir.W would force check for dbm bit:                  *)
               (* - if set then either update or not db bit per R_TXGHB *)
               (* - if unset raise Permission fault                     *)
-              lift_memop rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
+              lift_memop ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
           in
           if do_wb then
             do_action true checked ma
@@ -2234,7 +2231,7 @@ Arguments:
         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) ma mv an ii
+          lift_memop ~tag:"CAS" rn Dir.W true memtag mop_success (to_perms "rw" sz) ma mv an ii
         )( (* CAS fails *)
           M.altT (
             (* CAS generates an Explicit Write Effect              *)
@@ -4881,6 +4878,19 @@ Arguments:
             else do_build_semantics test ii.A.inst ii
           end
 
+      let can_unset_af_loc e =
+        match E.access_of e with
+        | Some Access.(PTE _|PHY_PTE)
+          ->
+            begin
+              match E.location_of e,E.written_of e with
+              | Some (A.Location_global loc),Some v ->
+                  if E.is_explicit e && can_be_pt loc && can_af0 v then Some loc
+                  else None
+              | _ -> None
+            end
+        | _ -> None
+
       let spurious_setaf v =
         test_and_set_af_succeeds v E.IdSpurious DISide.Data
 

herd/ARMSem.ml

@@ -514,7 +514,7 @@ module
 
           end
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
 

herd/ASLAction.ml

@@ -112,6 +112,10 @@ module Make (C: Config) (A : S) = struct
   (**************************************)
   (* Access to sub_components of events *)
   (**************************************)
+  let access_of = function
+    | Access (_,_,_,_,(_,_,a)) -> Some a
+    | Fault _|Barrier _|Branching _|CutOff _|NoAction
+      -> None
 
   let value_of =
     function

herd/ASLSem.ml

@@ -152,6 +152,7 @@ module Make (Conf : Config) = struct
   let atomic_pair_allowed _ _ = true
   module Mixed (SZ : ByteSize.S) : sig
     val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+    val can_unset_af_loc : event -> A.V.v option
     val spurious_setaf : A.V.v -> unit M.t
   end = struct
     module Mixed = M.Mixed (SZ)
@@ -931,6 +932,7 @@ module Make (Conf : Config) = struct
       assert (V.equal i V.zero);
       M.addT !(snd ii_env) B.nextT
 
-    let spurious_setaf _ = assert false
+    include NoAF
+
   end
 end

herd/BPFSem.ml

@@ -246,6 +246,7 @@ struct
            >>= fun v -> commit ii >>= fun () -> B.bccT v lbl)
     ;;
 
-    let spurious_setaf _ = assert false
+    include NoAF
+
   end
 end

herd/BellAction.ml

@@ -81,6 +81,9 @@ end = struct
   | CutOff msg -> "CutOff:" ^ msg
 
 (* Utility functions to pick out components *)
+
+  let access_of _ = None
+
   let value_of a = match a with
   | Access (_,_ ,v,_,_,_) -> Some v
   | _ -> None