From 387839acf602ffd6e0b94188e107e1695b0e9056 Mon Sep 17 00:00:00 2001 From: Vladimir Murzin Date: Fri, 11 Oct 2024 13:42:05 +0100 Subject: [PATCH] [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 --- herd-www/jerd.ml | 1 + herd/AArch64Sem.ml | 37 ++++++++++++------- herd/herd.ml | 1 + herd/mem.ml | 1 + herd/opts.ml | 1 + herd/opts.mli | 1 + herd/parseTest.ml | 2 + .../tests/instructions/AArch64.MTE/S00.litmus | 13 +++++++ .../AArch64.MTE/S00.litmus.expected | 10 +++++ .../tests/instructions/AArch64.MTE/S01.litmus | 9 +++++ .../AArch64.MTE/S01.litmus.expected | 11 ++++++ herd/variant.ml | 7 ++++ herd/variant.mli | 2 + lib/parseTag.ml | 5 ++- lib/parseTag.mli | 2 + lib/testVariant.ml | 3 ++ lib/testVariant.mli | 2 + litmus/top_litmus.ml | 1 + litmus/variant_litmus.ml | 1 + litmus/variant_litmus.mli | 1 + 20 files changed, 97 insertions(+), 14 deletions(-) create mode 100644 herd/tests/instructions/AArch64.MTE/S00.litmus create mode 100644 herd/tests/instructions/AArch64.MTE/S00.litmus.expected create mode 100644 herd/tests/instructions/AArch64.MTE/S01.litmus create mode 100644 herd/tests/instructions/AArch64.MTE/S01.litmus.expected diff --git a/herd-www/jerd.ml b/herd-www/jerd.ml index 01b00fc2c..d1b9032f2 100644 --- a/herd-www/jerd.ml +++ b/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 diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index dadea717a..b17e8aa41 100644 --- a/herd/AArch64Sem.ml +++ b/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,7 +615,7 @@ 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 @@ -623,7 +623,16 @@ module Make 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) diff --git a/herd/herd.ml b/herd/herd.ml index 148c69f3d..988b7c068 100644 --- a/herd/herd.ml +++ b/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 diff --git a/herd/mem.ml b/herd/mem.ml index d7f06ff41..9f289653a 100644 --- a/herd/mem.ml +++ b/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 diff --git a/herd/opts.ml b/herd/opts.ml index 4e4996107..d46efbd04 100644 --- a/herd/opts.ml +++ b/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 diff --git a/herd/opts.mli b/herd/opts.mli index 0d0493504..825415850 100644 --- a/herd/opts.mli +++ b/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 diff --git a/herd/parseTest.ml b/herd/parseTest.ml index 030b63985..1f0983854 100644 --- a/herd/parseTest.ml +++ b/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 diff --git a/herd/tests/instructions/AArch64.MTE/S00.litmus b/herd/tests/instructions/AArch64.MTE/S00.litmus new file mode 100644 index 000000000..fb3f24ff1 --- /dev/null +++ b/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) diff --git a/herd/tests/instructions/AArch64.MTE/S00.litmus.expected b/herd/tests/instructions/AArch64.MTE/S00.litmus.expected new file mode 100644 index 000000000..3fe5b125d --- /dev/null +++ b/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 + diff --git a/herd/tests/instructions/AArch64.MTE/S01.litmus b/herd/tests/instructions/AArch64.MTE/S01.litmus new file mode 100644 index 000000000..acbfddf69 --- /dev/null +++ b/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) diff --git a/herd/tests/instructions/AArch64.MTE/S01.litmus.expected b/herd/tests/instructions/AArch64.MTE/S01.litmus.expected new file mode 100644 index 000000000..7844cbfd6 --- /dev/null +++ b/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 + diff --git a/herd/variant.ml b/herd/variant.ml index 61d5bd092..3b5f700a1 100644 --- a/herd/variant.ml +++ b/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 diff --git a/herd/variant.mli b/herd/variant.mli index 1bef459e0..630dfbc12 100644 --- a/herd/variant.mli +++ b/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 diff --git a/lib/parseTag.ml b/lib/parseTag.ml index 970af14cf..aa34bfe96 100644 --- a/lib/parseTag.ml +++ b/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 diff --git a/lib/parseTag.mli b/lib/parseTag.mli index 337de8ddf..f4fc45362 100644 --- a/lib/parseTag.mli +++ b/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 diff --git a/lib/testVariant.ml b/lib/testVariant.ml index 2bf0cb097..122629792 100644 --- a/lib/testVariant.ml +++ b/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 diff --git a/lib/testVariant.mli b/lib/testVariant.mli index 34e50bed6..b3ca9fd81 100644 --- a/lib/testVariant.mli +++ b/lib/testVariant.mli @@ -22,6 +22,7 @@ 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 @@ -29,6 +30,7 @@ module Make : functor 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 diff --git a/litmus/top_litmus.ml b/litmus/top_litmus.ml index 75833cc23..22d3e451f 100644 --- a/litmus/top_litmus.ml +++ b/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 diff --git a/litmus/variant_litmus.ml b/litmus/variant_litmus.ml index 45802c893..bdac738bd 100644 --- a/litmus/variant_litmus.ml +++ b/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 diff --git a/litmus/variant_litmus.mli b/litmus/variant_litmus.mli index a87648d27..cc0eaa369 100644 --- a/litmus/variant_litmus.mli +++ b/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