[herd, aarch64]: Introduce support for FEAT_MTE_STORE_ONLY

FEAT_MTE_STORE_ONLY introduces control if Load instructions are Tag
Unchecked. Let's add support for that feature, yet (as usual) we need
to take extra care for CAS and friends:

  RMNHCZ If FEAT_MTE_STORE_ONLY is implemented, for a Tag Checked
         Compare and swap instruction, if the compare fails, it is
         CONSTRAINED UNPREDICTABLE whether the Tag Check operation is
         performed.

Signed-off-by: Vladimir Murzin <[email protected]>

herd-www/jerd.ml

@@ -189,6 +189,7 @@ let run_herd bell cat litmus cfg =
     let variant = !variant
     let fault_handling = !Refs.fault_handling
     let mte_precision = !Refs.mte_precision
+    let mte_store_only = !Refs.mte_store_only
     let sve_vector_length = !Refs.sve_vector_length
     let sme_vector_length = !Refs.sme_vector_length
     let dumpallfaults = !dumpallfaults

herd/AArch64Sem.ml

@@ -603,7 +603,7 @@ module Make
 
      (* Tag checking, MTE *)
 
-      let delayed_check_tags a_virt a_phy ma ii m1 m2 =
+      let delayed_check_tags dir a_virt a_phy ma ii m1 m2 =
         let (+++) = M.data_input_union in
         let rtag  =
           read_tag_mem (match a_phy with None -> a_virt | Some a -> a) ii in
@@ -615,15 +615,24 @@ module Make
         let m =
           let (>>=) = match a_phy with None -> (+++) | Some _ -> (>>=) in
           m >>= fun cond -> commit +++ fun _ -> M.unitT cond in
-        M.delay_kont "check_tags" m
+        let check = M.delay_kont "check_tags" m
           (fun c m ->
             let ma = (* NB output to initial ma *)
               match a_phy with
               | None ->
                 ma >>== fun a -> m >>== fun _ -> loc_extract a
               | Some _ ->
                 M.bind_ctrldata ma (fun a -> m >>== fun _ -> M.unitT a) in
-            choice c ma)
+            choice c ma) in
+        match (dir,C.mte_store_only) with
+          | Dir.W,_
+          | Dir.R,false
+            -> check
+          | Dir.R,true
+            ->
+            (* The case of a failed CAS with no write, but with a tag chek *)
+            let ma = ma >>= fun a -> loc_extract a in
+            M.altT (check) (m1 ma)
 
       (* Tag checking Morello *)
       let do_append_commit ma txt ii =
@@ -1377,7 +1386,7 @@ module Make
             fault ma >>! B.Fault [] in
           let check_tag moa a_virt =
             let do_check_tag a_phy moa =
-              delayed_check_tags a_virt (Some a_phy) moa ii mok mno in
+              delayed_check_tags dir a_virt (Some a_phy) moa ii mok mno in
             M.delay_kont "check_tag" moa do_check_tag in
           let cond_check_tag mpte_t a_virt =
             (* Only read and check the tag if the PTE of the tag op allows it *)
@@ -1410,7 +1419,7 @@ module Make
           (fun a_virt ma  ->
              let mm = mop Access.VIR in
              let ft = Some FaultType.AArch64.TagCheck in
-             delayed_check_tags a_virt None ma ii
+             delayed_check_tags dir a_virt None ma ii
                (fun ma -> mm ma >>= M.ignore >>= B.next1T)
                (lift_fault_memtag
                   (mk_fault (Some a_virt) dir an ii ft None) mm dir ii))
@@ -1479,16 +1488,18 @@ module Make
           else if checked then
             lift_memtag_virt mop ma dir an ii
           else
+            let ma = if C.mte_store_only then ma >>= fun a -> loc_extract a else ma in
             mop Access.VIR ma >>= M.ignore >>= B.next1T
 
       let do_ldr rA sz an mop ma ii =
 (* Generic load *)
-        lift_memop rA Dir.R false memtag
+        let checked = memtag && not C.mte_store_only in
+        lift_memop rA Dir.R false checked
           (fun ac ma _mv -> (* value fake here *)
             let open Precision in
             let memtag_sync =
-              memtag && (C.mte_precision = Synchronous ||
-                         C.mte_precision = Asymmetric) in
+              checked && (C.mte_precision = Synchronous ||
+                          C.mte_precision = Asymmetric) in
             if memtag_sync || Access.is_physical ac then
               M.bind_ctrldata ma (mop ac)
             else
@@ -1956,7 +1967,7 @@ module Make
         | RMW_A | RMW_AL -> A
 
       let swp sz rmw r1 r2 r3 ii =
-        lift_memop r3 Dir.W true (* swp is a write for the purpose of DB *)
+        lift_memop r3 Dir.W  true (* swp is a write for the purpose of DB *)
           memtag
           (fun ac ma mv ->
             let noret = match r2 with | AArch64.ZR -> true | _ -> false in
@@ -3162,10 +3173,10 @@ module Make
         else begin
             (* TODO: The size for DC should be a cache line *)
             let mop _ac a = dc_loc op a ii in
-            let dir = match op.AArch64Base.DC.funct with
-              | AArch64Base.DC.I -> Dir.W
-              | _ -> Dir.R in
-            lift_memop rd dir false memtag
+            let dir,checked = match op.AArch64Base.DC.funct with
+              | AArch64Base.DC.I -> Dir.W,memtag
+              | _ -> Dir.R,memtag && not C.mte_store_only in
+            lift_memop rd dir false checked
               (fun ac ma _mv -> (* value fake here *)
                 if Access.is_physical ac then
                   M.bind_ctrldata ma (mop ac)

herd/herd.ml

@@ -462,6 +462,7 @@ let () =
     let variant = !variant
     let fault_handling = !Refs.fault_handling
     let mte_precision = !Refs.mte_precision
+    let mte_store_only = !Refs.mte_store_only
     let sve_vector_length = !Refs.sve_vector_length
     let sme_vector_length = !Refs.sme_vector_length
   let byte = !byte

herd/mem.ml

@@ -35,6 +35,7 @@ module type CommonConfig = sig
   val variant : Variant.t -> bool
   val fault_handling : Fault.Handling.t
   val mte_precision : Precision.t
+  val mte_store_only : bool
 end
 
 module type Config = sig

herd/opts.ml

@@ -49,6 +49,7 @@ let variant = ref (fun _ -> false)
 module Refs = struct
   let fault_handling = ref Fault.Handling.default
   let mte_precision = ref Precision.default
+  let mte_store_only = ref false
   let sve_vector_length = ref 128
   let sme_vector_length = ref 128
 end

herd/opts.mli

@@ -46,6 +46,7 @@ val variant : (Variant.t -> bool) ref
 module Refs : sig
   val fault_handling : Fault.Handling.t ref
   val mte_precision : Precision.t ref
+  val mte_store_only : bool ref
   val sve_vector_length : int ref
   val sme_vector_length : int ref
 end

herd/parseTest.ml

@@ -44,6 +44,7 @@ module Top (TopConf:RunTest.Config) = struct
             let info = splitted.Splitter.info
             let variant = TopConf.variant
             let mte_precision = TopConf.mte_precision
+            let mte_store_only = TopConf.mte_store_only
             let fault_handling = TopConf.fault_handling
             let sve_vector_length = TopConf.sve_vector_length
             let sme_vector_length = TopConf.sme_vector_length
@@ -62,6 +63,7 @@ module Top (TopConf:RunTest.Config) = struct
         (function | None -> unroll | Some _ as o -> o)
       let fault_handling = TestConf.fault_handling
       let mte_precision = TestConf.mte_precision
+      let mte_store_only = TestConf.mte_store_only
       let sve_vector_length = TestConf.sve_vector_length
       let sme_vector_length = TestConf.sme_vector_length
       let variant = TestConf.variant

herd/tests/instructions/AArch64.MTE/S00.litmus

@@ -0,0 +1,13 @@
+AArch64 S00
+variant=memtag,sync,store-only
+{
+int x=1;
+tag(x)=:red;
+0:X0=x:green;
+}
+ P0          ;
+ L0:         ;
+ LDR W1,[X0] ;
+ L1:         ;
+ STR WZR,[X0];
+forall fault(P0:L1,x)

herd/tests/instructions/AArch64.MTE/S00.litmus.expected

@@ -0,0 +1,10 @@
+Test S00 Required
+States 1
+ Fault(P0:L1,x:green,TagCheck);
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall (fault(P0:L1,x))
+Observation S00 Always 1 0
+Hash=5229396c405f2016eb0680a632b41e0f
+

herd/tests/instructions/AArch64.MTE/S01.litmus

@@ -0,0 +1,9 @@
+AArch64 S01
+variant=memtag,sync,store-only
+{
+0:X9=x:red;
+}
+ P0             ;
+MOV W0,#1       ;
+CAS W0,WZR,[X9] ;
+exists ~fault(P0,x)

herd/tests/instructions/AArch64.MTE/S01.litmus.expected

@@ -0,0 +1,11 @@
+Test S01 Allowed
+States 2
+  ~Fault(P0,x);
+ Fault(P0,x:red,TagCheck);
+Ok
+Witnesses
+Positive: 2 Negative: 3
+Condition exists (not (fault(P0,x)))
+Observation S01 Sometimes 2 3
+Hash=1f4ab0e23e8f6210451620fc77f6e82a
+

herd/variant.ml

@@ -46,6 +46,7 @@ type t =
 (* Tags *)
   | MemTag
   | MTEPrecision of Precision.t (* MTE tag mismatch handling *)
+  | MTEStoreOnly
   | FaultHandling of Fault.Handling.t (* Fault handling *)
   | CutOff
   | Morello
@@ -143,6 +144,7 @@ let parse s = match Misc.lowercase s with
 | "lkmmv1" -> Some (LKMMVersion `lkmmv1)
 | "lkmmv2" -> Some (LKMMVersion `lkmmv2)
 | "tagmem"|"memtag"|"mte" -> Some MemTag
+| "store-only" -> Some MTEStoreOnly
 | "cutoff" -> Some CutOff
 | "morello" -> Some Morello
 | "neon" -> Some Neon
@@ -242,6 +244,7 @@ let pp = function
   | LKMMVersion `lkmmv2 -> "lkmmv2"
   | MemTag -> "memtag"
   | MTEPrecision p -> Precision.pp p
+  | MTEStoreOnly -> "store-only"
   | FaultHandling p -> Fault.Handling.pp p
   | CutOff -> "CutOff"
   | Morello -> "Morello"
@@ -318,6 +321,10 @@ let set_mte_precision r = function
   | MTEPrecision p -> r := p; true
   | _ -> false
 
+let set_mte_store_only r = function
+  | MTEStoreOnly -> r := true; true
+  | _ -> false
+
 let check_vector_length memo n =
   let () =
   if n < 128 || n > 2048 || n mod 128 <> 0 then

herd/variant.mli

@@ -44,6 +44,7 @@ type t =
   | DontCheckMixed
   | MemTag           (* Memory Tagging, synonym of MTE *)
   | MTEPrecision of Precision.t (* MTE tag mismatch handling *)
+  | MTEStoreOnly     (* Load instructions are Tag Unchecked *)
   | FaultHandling of Fault.Handling.t (* Fault handling *)
   | CutOff
   | Morello
@@ -128,6 +129,7 @@ val get_default :  Archs.t -> t -> bool
 val get_switch : Archs.t -> t -> (t -> bool) -> bool
 
 val set_mte_precision : Precision.t ref -> t -> bool
+val set_mte_store_only : bool ref -> t -> bool
 val set_fault_handling : Fault.Handling.t ref -> t -> bool
 
 val set_sve_length : int ref -> t -> t option

lib/parseTag.ml

@@ -118,6 +118,7 @@ module type SArg = sig
 
   val set_fault_handling :  Fault.Handling.t ref -> t -> bool
   val set_mte_precision : Precision.t ref -> t -> bool
+  val set_mte_store_only : bool ref -> t -> bool
   val set_sve_length : int ref -> t -> t option
   val set_sme_length : int ref -> t -> t option
   val check_tag : t -> t list
@@ -126,6 +127,7 @@ end
 module type RefsArg = sig
   val fault_handling : Fault.Handling.t ref
   val mte_precision : Precision.t ref
+  val mte_store_only : bool ref
   val sve_vector_length : int ref
   val sme_vector_length : int ref
 end
@@ -137,7 +139,8 @@ module MakeOptS =
 
     let setnow t =
       set_fault_handling Refs.fault_handling t ||
-      set_mte_precision Refs.mte_precision t
+      set_mte_precision Refs.mte_precision t ||
+      set_mte_store_only Refs.mte_store_only t
 
     let check_lengths t =
       let (>>=) o f = match o with

lib/parseTag.mli

@@ -55,6 +55,7 @@ module type SArg = sig
 
   val set_fault_handling :  Fault.Handling.t ref -> t -> bool
   val set_mte_precision : Precision.t ref -> t -> bool
+  val set_mte_store_only : bool ref -> t -> bool
   val set_sve_length : int ref -> t -> t option
   val set_sme_length : int ref -> t -> t option
   val check_tag : t -> t list
@@ -63,6 +64,7 @@ end
 module type RefsArg = sig
   val fault_handling : Fault.Handling.t ref
   val mte_precision : Precision.t ref
+  val mte_store_only : bool ref
   val sve_vector_length : int ref
   val sme_vector_length : int ref
 end

lib/testVariant.ml

@@ -23,6 +23,7 @@ module
       val info : MiscParser.info
       val variant : Opt.t -> bool
       val mte_precision : Precision.t
+      val mte_store_only : bool
       val fault_handling : Fault.Handling.t
       val sve_vector_length : int
       val sme_vector_length : int
@@ -33,6 +34,7 @@ module
       module Refs = struct
 
         let mte_precision = ref Var.mte_precision
+        let mte_store_only = ref Var.mte_store_only
         and fault_handling = ref Var.fault_handling
         and sve_vector_length = ref Var.sve_vector_length
         and sme_vector_length = ref Var.sme_vector_length
@@ -55,6 +57,7 @@ module
             with Arg.Bad msg ->  Warn.user_error "%s" msg
 
        let mte_precision = !Refs.mte_precision
+       let mte_store_only = !Refs.mte_store_only
        and fault_handling = !Refs.fault_handling
        and sve_vector_length = !Refs.sve_vector_length
        and sme_vector_length = !Refs.sme_vector_length

lib/testVariant.mli

@@ -22,13 +22,15 @@ module Make : functor
       val info : MiscParser.info
       val variant : Opt.t -> bool
       val mte_precision : Precision.t
+      val mte_store_only : bool
       val fault_handling : Fault.Handling.t
       val sve_vector_length : int
       val sme_vector_length : int
     end) ->
       sig
         type t = Var.Opt.t
         val mte_precision : Precision.t
+        val mte_store_only : bool
         val fault_handling : Fault.Handling.t
         val sve_vector_length : int
         val sme_vector_length : int

litmus/top_litmus.ml

@@ -405,6 +405,7 @@ end = struct
               let info = splitted.Splitter.info
               let variant = OT.variant
               let mte_precision = OT.mte_precision
+              let mte_store_only = false
               let fault_handling = OT.fault_handling
               let sve_vector_length = 0
               let sme_vector_length = 0

litmus/variant_litmus.ml

@@ -79,6 +79,7 @@ let set_fault_handling r = function
 | _ -> false
 
 let set_mte_precision _ _ = false
+let set_mte_store_only _ _ = false
 
 let set_sve_length _ _ = None
 let set_sme_length _ _ = None

litmus/variant_litmus.mli

@@ -33,6 +33,7 @@ val compare : t -> t -> int
 
 val set_fault_handling : Fault.Handling.t ref -> t -> bool
 val set_mte_precision : Precision.t ref -> t -> bool
+val set_mte_store_only : bool ref -> t -> bool
 
 val set_sve_length : int ref -> t -> t option
 val set_sme_length : int ref -> t -> t option