Memory-tagging support in herd and diy

This patch introduces support for the Memory Tagging
Extension (MTE). More precisely, loads and stores can
now be checked against a "tag" and fault if their tag
does not match. The extension also adds the LDG and STG
instructions which handle tags directly.

Co-autored-by: Luc Maranget <luc.maranget@inria.fr>
Signed-off-by: Jade Alglave <jade.alglave@arm.com>
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>

gen/AArch64Arch_gen.ml

@@ -50,7 +50,7 @@ module Mixed =
 (* AArch64 has more atoms that others *)
 let bellatom = false
 type atom_rw =  PP | PL | AP | AL
-type atom_acc = Plain | Acq | AcqPc | Rel | Atomic of atom_rw
+type atom_acc = Plain | Acq | AcqPc | Rel | Atomic of atom_rw | Tag
 type atom = atom_acc * MachMixed.t option
 
 let default_atom = Atomic PP,None
@@ -59,7 +59,7 @@ let applies_atom (a,_) d = match a,d with
 | Acq,R
 | AcqPc,R
 | Rel,W
-| (Plain|Atomic _),(R|W)
+| (Plain|Atomic _|Tag),(R|W)
   -> true
 | _ -> false
 
@@ -79,6 +79,7 @@ let applies_atom (a,_) d = match a,d with
      | Acq -> "A"
      | AcqPc -> "Q"
      | Plain -> "P"
+     | Tag -> "T"
 
    let pp_atom (a,m) = match a with
    | Plain ->
@@ -104,7 +105,7 @@ let applies_atom (a,_) d = match a,d with
    let fold_atom_rw f r = f PP (f PL (f AP (f AL r)))
 
    let fold_acc f r =
-     f Acq (f AcqPc (f Rel (fold_atom_rw (fun rw -> f (Atomic rw)) r)))
+     f Tag (f Acq (f AcqPc (f Rel (fold_atom_rw (fun rw -> f (Atomic rw)) r))))
 
    let fold_non_mixed f r = fold_acc (fun acc r -> f (acc,None) r) r
 
@@ -118,7 +119,7 @@ let applies_atom (a,_) d = match a,d with
 
    let worth_final (a,_) = match a with
      | Atomic _ -> true
-     | Acq|AcqPc|Rel|Plain -> false
+     | Acq|AcqPc|Rel|Plain|Tag -> false
 
 
    let varatom_dir _d f r = f None r
@@ -145,13 +146,14 @@ let applies_atom (a,_) d = match a,d with
        end)
 
 let overwrite_value v ao w = match ao with
-  | None| Some ((Atomic _|Acq|AcqPc|Rel|Plain),None) -> w (* total overwrite *)
-  | Some ((Atomic _|Acq|AcqPc|Rel|Plain),Some (sz,o)) ->
-      ValsMixed.overwrite_value v sz o w
+| None| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),None)
+  -> w (* total overwrite *)
+| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),Some (sz,o)) ->
+    ValsMixed.overwrite_value v sz o w
 
  let extract_value v ao = match ao with
-  | None| Some ((Atomic _|Acq|AcqPc|Rel|Plain),None) -> v
-  | Some ((Atomic _|Acq|AcqPc|Rel|Plain),Some (sz,o)) ->
+  | None| Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),None) -> v
+  | Some ((Atomic _|Acq|AcqPc|Rel|Plain|Tag),Some (sz,o)) ->
       ValsMixed.extract_value v sz o
 
 (* End of atoms *)

gen/AArch64Compile_gen.ml

@@ -111,12 +111,14 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Quad -> I_LDR (V64,r1,r2,K o)
 
     let ldr r1 r2 = I_LDR (vloc,r1,r2,K 0)
+    let ldg r1 r2 = I_LDG (r1,r2,K 0)
     let ldar r1 r2 = I_LDAR (vloc,AA,r1,r2)
     let ldapr r1 r2 = I_LDAR (vloc,AQ,r1,r2)
     let ldxr r1 r2 = I_LDAR (vloc,XX,r1,r2)
     let ldaxr r1 r2 = I_LDAR (vloc,AX,r1,r2)
     let sxtw r1 r2 = I_SXTW (r1,r2)
     let ldr_idx r1 r2 idx = I_LDR (vloc,r1,r2,RV (vloc,idx))
+    let ldg_idx r1 r2 idx = I_LDG (r1,r2,RV (vloc,idx))
 
     let ldr_mixed_idx v r1 r2 idx sz  =
       let open MachSize in
@@ -135,8 +137,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Quad -> I_STR (V64,r1,r2,K o)
 
     let str r1 r2 = I_STR (vloc,r1,r2,K 0)
+    let stg r1 r2 = I_STG (r1,r2,K 0)
     let stlr r1 r2 = I_STLR (vloc,r1,r2)
     let str_idx r1 r2 idx = I_STR (vloc,r1,r2,RV (vloc,idx))
+    let stg_idx r1 r2 idx = I_STG (r1,r2,RV (vloc,idx))
     let stxr r1 r2 r3 = I_STXR (vloc,YY,r1,r2,r3)
     let stlxr r1 r2 r3 = I_STXR (vloc,LY,r1,r2,r3)
 
@@ -298,8 +302,6 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
             [] in
           rA,init,cs,st
 
-
-
         let emit_load_not_zero st p init x =
           let rA,st = next_reg st in
           let rB,init,st = U.next_init st p init x in
@@ -364,6 +366,14 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
           let load_idx st rA rB idx = [ldr_idx rA rB idx],st
         end)
 
+    module LDG =
+      LOAD
+        (struct
+          let load = wrap_st ldg
+          let load_idx st rA rB idx = [ldg_idx rA rB idx],st
+        end)
+
+
 (* For export *)
     let emit_load_one = LDR.emit_load_one
     let emit_load = LDR.emit_load
@@ -442,6 +452,13 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
           let store_idx st rA rB idx = [str_idx rA rB idx],st
         end)
 
+    module STG =
+      STORE
+        (struct
+          let store = wrap_st stg
+          let store_idx st rA rB idx = [stg_idx rA rB idx],st
+        end)
+
     module STLR =
       STORE
         (struct
@@ -451,8 +468,6 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
             ins@[stlr rA r],st
         end)
 
-
-
 (***************************)
 (* Atomic loads and stores *)
 (***************************)
@@ -731,6 +746,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | R,Some (Plain,Some (sz,o)) ->
             let r,init,cs,st = emit_load_mixed sz o st p init loc in
             Some r,init,cs,st
+        | R,Some (Tag,Some (sz,o)) ->
+            let r,init,cs,st = LDG.emit_load st p init loc  in
+            Some r,init,cs,st
         | W,None ->
             let init,cs,st = STR.emit_store st p init loc e.v in
             None,init,cs,st
@@ -762,7 +780,11 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
                 end) in
             let init,cs,st = S.emit_store st p init loc e.v in
             None,init,cs,st
+        | W,Some (Tag,Some (sz,o)) ->
+            let init,cs,st = STG.emit_store st p init loc e.v in
+            None,init,cs,st
         | _,Some (Plain,None) -> assert false
+        | _,Some (Tag,None) -> assert false
         | J,_ -> emit_joker st init
         end
 
@@ -947,6 +969,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
           | R,Some (Atomic rw,Some (sz,o)) ->
               let r,init,cs,st = emit_lda_mixed_idx sz o rw st p init loc r2 in
               Some r,init, Instruction c::cs,st
+          | R,Some (Tag,(Some (sz,o))) ->
+              let r,init,cs,st = LDG.emit_load_idx st p init loc r2 in
+              Some r,init, Instruction c::cs,st
           | W,None ->
               let init,cs,st = STR.emit_store_idx st p init loc r2 e.v in
               None,init,Instruction c::cs,st
@@ -1005,8 +1030,12 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
               let rA,init,cs_mov,st = U.emit_mov_sz sz st p init e.v in
               let init,cs,st = S.emit_store_idx_reg st p init loc r2 rA in
               None,init,Instruction c::cs_mov@cs,st
+          | W,Some (Tag, Some (sz,o)) ->
+              let init,cs,st = STG.emit_store_idx st p init loc r2 e.v in
+              None,init,Instruction c::cs,st
           | J,_ -> emit_joker st init
           | _,Some (Plain,None) -> assert false
+          | _,Some (Tag,None) -> assert false
           end
       | _,Code _ -> Warn.fatal "No dependency to code location"
 
@@ -1086,7 +1115,11 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
                   end) in
               let init,cs,st = S.emit_store_reg st p init loc r2 in
               None,init,cs2@cs,st
+          | Some (Tag, Some (sz,o)) ->
+              let init,cs,st = STG.emit_store_reg st p init loc r2 in
+              None,init,cs2@cs,st
           | Some (Plain,None) -> assert false
+          | Some (Tag,None) -> assert false
           end
       | Some J,_ -> emit_joker st init
       | _,Code _ -> Warn.fatal "Not Yet (%s,dep_data)" (C.debug_evt e)

gen/config.ml

@@ -48,6 +48,7 @@ let optcoherence = ref false
 let bell = ref None
 let scope = ref Scope.No
 let variant = ref (fun (_:Variant_gen.t) -> false)
+let mtags = ref false
 
 type do_observers =
   | Avoid   (* was false *)
@@ -165,7 +166,9 @@ let common_specs =
    ("-hexa", Arg.Unit (fun () -> hexa := true),"hexadecimal output")::
    ("-o", Arg.String (fun s -> tarfile := Some s),
     "<name.tar> output litmus tests in archive <name.tar> (default, output in curent directory)")::
-  ("-c", Arg.Bool (fun b ->  canonical_only := b),
+  ("-mtags", Arg.Bool (fun b ->  mtags := b),
+   sprintf "<bool> initialise tags (default %b)" !mtags)::
+   ("-c", Arg.Bool (fun b ->  canonical_only := b),
    sprintf "<b> avoid equivalent cycles (default %b)" !canonical_only)::
   ("-list",
    Arg.Unit (fun () -> show := Some ShowGen.Edges),

gen/diy.ml

@@ -241,6 +241,7 @@ let () =
     let docheck = !Config.docheck
     let typ = !Config.typ
     let hexa = !Config.hexa
+    let mtags = !Config.mtags
  end in
   let module C = struct
     let verbose = !Config.verbose

gen/diycross.ml

@@ -216,6 +216,7 @@ let () =
       let cpp = match !Config.arch with `CPP -> true | _ -> false
       let scope = !Config.scope
       let variant = !Config.variant
+      let mtags = !Config.mtags
     end in
     let module T = Top_gen.Make(C) in
     begin match !Config.arch with

gen/diyone.ml

@@ -215,6 +215,7 @@ let () =
     let neg = !Config.neg
     let typ = !Config.typ
     let hexa = !Config.hexa
+    let mtags = !Config.mtags
 (* Specific *)
     let norm = !norm
     let cpp = cpp

gen/top_gen.ml

@@ -37,6 +37,7 @@ module type Config = sig
   val typ : TypBase.t
   val hexa : bool
   val variant : Variant_gen.t -> bool
+  val mtags : bool
 end
 
 module Make (O:Config) (Comp:XXXCompile_gen.S) : Builder.S
@@ -526,7 +527,7 @@ let min_max xs =
                    in do_rec oks k'
     in do_rec oks []
 
-  let compile_cycle ok n =
+ let compile_cycle ok n =
     let open Config in
     Label.reset () ;
     let splitted =  C.split_procs n in
@@ -651,6 +652,9 @@ let dump_init chan inits env =
         let p = get_proc left in
         if p <> q then fprintf chan "\n" else fprintf chan " " ;
         fprintf chan "%s=%s;" (A.pp_location left) loc ;
+        if !Config.mtags then
+          if not(List.exists (fun (a,b) -> b=loc) rem)
+          then fprintf chan " %s.atag;" loc ;
         p_rec p rem in
   p_rec (-1) inits
 

herd/AArch64Arch_herd.ml

@@ -21,7 +21,7 @@ module Make (C:sig include Arch_herd.Config val moreedges : bool end) (V:Value.S
     let pp_barrier_short = pp_barrier
     let reject_mixed = true
 
-    type annot = A | XA | L | XL | X | N | Q | NoRet
+    type annot = A | XA | L | XL | X | N | Q | NoRet | T
     type lannot = annot
 
     let empty_annot = N
@@ -52,6 +52,10 @@ module Make (C:sig include Arch_herd.Config val moreedges : bool end) (V:Value.S
       | L | XL -> true
       | _ -> false
 
+    let is_tag = function
+      | T -> true
+      | _ -> false
+
     let barrier_sets =
       do_fold_dmb_dsb C.moreedges
         (fun b k ->
@@ -65,6 +69,7 @@ module Make (C:sig include Arch_herd.Config val moreedges : bool end) (V:Value.S
       "Q",  wrap_is is_acquire_pc;
       "L",  wrap_is is_release;
       "NoRet", wrap_is is_noreturn;
+      "T", wrap_is is_tag
     ]
 
     let is_isync = is_barrier ISB
@@ -79,6 +84,7 @@ module Make (C:sig include Arch_herd.Config val moreedges : bool end) (V:Value.S
       | X -> "*"
       | N -> ""
       | NoRet -> "NoRet"
+      | T -> "Tag"
 
     module V = V