Add missing fault label in all RMW related instruction.

The LxSx has to label both the generated load and store instructions.
Also the fault check for those two instructions should be composited
disjectively.

Author: ShaleXIONG

gen/AArch64Compile_gen.ml

@@ -1723,18 +1723,30 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
 
     let get_tagged_loc e = add_tag (as_data e.C.loc) e.C.tag
 
-    let add_label_to_instructions e cs =
+    let add_label_to_last_instructions e cs =
       match e.C.check_fault with
       | Some (label_name, _) ->
-        (* Always label the last instruction,
-           which should be the actual load or store. *)
         let rec do_rec = function
           | [] -> assert false (* the `cs` should not be empty *)
           | [instr] -> [Label(label_name, instr)]
           | instr::rem -> instr::do_rec rem in
         do_rec cs
       | None -> cs
 
+    let add_label_to_first_instructions e cs =
+      match e.C.check_fault with
+      | Some (label_name, _) ->
+        (* find the first non-label instruction *)
+        let rec do_rec cs = match cs with
+          | [] -> assert false (* the `cs` should not be empty *)
+          | instr::rem -> begin match instr with
+            (* skip label or instruction that is already labelled *)
+            | Label(_) -> instr::do_rec rem
+            |_ -> Label(label_name, instr)::rem
+        end in
+        do_rec cs
+      | None -> cs
+
     let emit_access st p init e =
     (* collapse the value `v` in event `e` to integer *)
     let value = Code.value_to_int e.C.v in
@@ -1745,7 +1757,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | R,Some (Instr, None) ->
             let r,init,cs,st = LDR.emit_fetch st p init lab in
             Some r,init,cs,st
-        (* Plain read from an instruction label is currently not supported, 
+        (* Plain read from an instruction label is currently not supported,
            but will be implemented in a future patch
         | R, None ->
             let r,init,cs,st = LDR.emit_load st p init lab in
@@ -1940,7 +1952,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | W,Some (Neon _,Some _) -> assert false
         end in
         (* Add a label to instructions `cs`, when a fault check is required. *)
-        let cs = add_label_to_instructions e cs in
+        let cs = add_label_to_last_instructions e cs in
         regs,inits,cs,st
     (* END of emit_access *)
 
@@ -1960,6 +1972,15 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       check_cu (not (A64.do_cu || same_sz szr szw)) ;
       ar,aw
 
+    let add_label_to_pair er ew cs=
+      (* Add the label to the read event,
+         which should be the first non-labelled instruction *)
+      cs |> add_label_to_first_instructions er
+      (* After the first read event being labelled,
+         add the label to the write event which should now
+         be the first non-labelled instruction *)
+         |> add_label_to_first_instructions ew
+
 
     let emit_addr_simple  st p init er =
       let rA,init,st = U.next_init st p init (get_tagged_loc er) in
@@ -1971,6 +1992,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let rW,init,csi,st = U.emit_mov st p init (Code.value_to_int ew.C.v) in
       let arw = check_arw_lxsx er ew in
       let init,cs,st = XSingle.emit_pair arw p st init rR rW rA ew in
+      let cs = add_label_to_pair er ew cs in
       rR,init,csi@caddr@cs,st
 
     let emit_exch1 = do_emit_exch1 emit_addr_simple
@@ -1983,6 +2005,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let arw = check_arw_lxsx er ew in
       let init,cs,st =
         XPair.emit_pair arw p st init (rR1,rR2) (rW1,rW2) rA ew in
+      let cs = add_label_to_pair er ew cs in
       rR1,init,csi@caddr@cs,st
 
     let emit_exch22 = do_emit_exch22 emit_addr_simple
@@ -1995,6 +2018,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let module X = ExclusivePair(XLoadPair)(XStore) in
       let init,cs,st =
         X.emit_pair arw p st init (rR1,rR2) rW rA ew in
+      let cs = add_label_to_pair er ew cs in
       rR1,init,csi@caddr@cs,st
 
     let emit_exch21 = do_emit_exch21 emit_addr_simple
@@ -2008,6 +2032,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       let module X = ExclusivePair(XLoad)(XStorePair) in
       let init,cs,st =
         X.emit_pair arw p st init rR (rW1,rW2) rA ew in
+      let cs = add_label_to_pair er ew cs in
       rR,init,csi@caddr@cs,st
 
     let emit_exch12 = do_emit_exch12 emit_addr_simple
@@ -2068,8 +2093,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[ins_mixed sz a rW rR rA],st in
+      let cs = add_label_to_last_instructions er (pseudo cs) in
       let cs2 = emit_ldr_addon opt rR in
-      rR,init,csi@csi2@pseudo (cs@cs2),st
+      rR,init,(csi@csi2@cs@pseudo cs2),st
 
     let do_emit_ldop ins ins_mixed st p init er ew =
       let rA,init,st =
@@ -2094,8 +2120,9 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[cas_mixed sz a rS rT rA],st in
+      let cs = add_label_to_last_instructions er (pseudo cs) in
       let cs2 = emit_ldr_addon opt rS in
-      rS,init,csS@csS2@csT@csT2@pseudo (cs@cs2),st
+      rS,init,csS@csS2@csT@csT2@cs@pseudo cs2,st
 
     let emit_cas  st p init er ew =
       let rA,init,st =
@@ -2118,7 +2145,8 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
       | Some (sz,o) ->
           let rA,cs,st = sumi_addr st rA o in
           cs@[stop_mixed op sz a rW rA],st in
-      None,init,csi@pseudo cs,st
+      let cs = add_label_to_last_instructions er (pseudo cs) in
+      None,init,csi@cs,st
 
     let emit_stop  op st p init er ew =
       let rA,init,st =
@@ -2235,7 +2263,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
               assert (Misc.is_none m) ;
               Some (a,Some (MachSize.S128,0))
             | _ -> Some (a,m) end in
-          begin match d,atom with
+          let regs,inits,cs,st = begin match d,atom with
           | R,None ->
               let r,init,cs,st =
                 LDR.emit_load_idx_var vloc vdep st p init loc r2 in
@@ -2449,8 +2477,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
               None,init,pseudo cs0@cs,st
           | W,Some (Neon _,Some _) -> assert false
           | _,Some (Plain _,None) -> assert false
-          end
-      | _,Code _ -> Warn.fatal "No dependency to code location"
+          end in
+          (* Add a label to instructions `cs`, when a fault check is required. *)
+          regs,inits,(add_label_to_last_instructions e cs),st
+        | _,Code _ -> Warn.fatal "No dependency to code location"
       (* END of emit_access_dep_addr *)
 
     let emit_addr_dep csel vdep st p init loc rd =
@@ -2512,7 +2542,7 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
         | _ -> Some (a,m) end in
       (* collapse the value `v` in event `e` to integer *)
       let value = Code.value_to_int e.C.v in
-      match e.C.dir,e.C.loc with
+      let regs,inits,cs,st = match e.C.dir,e.C.loc with
       | None,_ -> Warn.fatal "TODO"
       | Some R,_ -> Warn.fatal "data dependency to load"
       | Some W,Data loc ->
@@ -2660,8 +2690,10 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
              None,init,cs2@cs,st
           | Some (Pair _,Some _) -> assert false
           end
-      | _,Code _ -> Warn.fatal "Not Yet (%s,dep_data)" (C.debug_evt e)
-      (* END of emit_access_dep_data *)
+      (* END of `Some W` *)
+      | _,Code _ -> Warn.fatal "Not Yet (%s,dep_data)" (C.debug_evt e) in
+    regs,inits,(add_label_to_last_instructions e cs),st
+    (* END of emit_access_dep_data *)
 
     let is_ctrlisync = function
       | D.CTRLISYNC -> true

gen/CCompile_gen.ml

@@ -826,7 +826,7 @@ module Make(O:Config) : Builder.S
                   F.run evts m
               | Cycle -> F.check f
               | Observe -> F.observe f in
-            (add_args env c,f (F.FaultSet.empty,F.FaultSet.empty)),
+            (add_args env c,f ([],[])),
             (U.compile_prefetch_ios (List.length obsc) ios,
              U.compile_coms splitted),
             env

gen/cycle.ml

@@ -493,7 +493,6 @@ let int_com e = match e.E.edge with
   | _ -> false
 
 
-
 (* Coherence definition *)
 
 module CoSt = struct
@@ -565,10 +564,34 @@ module CoSt = struct
 
   let get_check_value st = st.check_value
 
+  let _set_check_fault st = {st with check_fault = true }
+
   (* read the check_fault flag, and reset/clean it *)
   let read_and_unset_check_fault st =
     st.check_fault, {st with check_fault = false }
 
+  (* Check if `pte_val` might fault *)
+  let label_fault pte_val = Some ((Label.next_label "L"), (PteVal.can_fault pte_val))
+
+  (* Helper function returns a fresh label and a boolean for if it should fault,
+     if a fault check is need. Otherwise return `None` *)
+  let fault_update st =
+    let check_fault, st = read_and_unset_check_fault st in
+    let pte_val = get_pte_value st in
+    let fault =
+      if check_fault then
+        if do_kvm then label_fault pte_val
+        (* While `memory tag` mode, any memory tag write to a variable
+           invalidates the tag, hence leads to fault. However, due to
+           potential weak memory behaviour, the final postcondition checks
+           if memory load to the variable can still observe the default,
+           and valid memory tag. Therefore we take a short cut here by
+           always inject a negtive check once a tag to the variable changes.*)
+        else if do_memtag then begin Some ((Label.next_label "L"), false) end
+        else None
+      else None in
+    fault, st
+
   let set_tcell st e = match e.bank with
     | Tag ->
        {e with tcell=[| e.v; |];},st
@@ -596,9 +619,6 @@ let pte_val_init loc = match loc with
 | Code.Data loc when do_kvm -> PteVal.default loc
 | _ -> pte_default
 
-(* Check if `pte_val` might fault *)
-let label_fault pte_val = Some ((Label.next_label "L"), (PteVal.can_fault pte_val))
-
 (****************************)
 (* Add events in edge cycle *)
 (****************************)
@@ -914,20 +934,19 @@ let set_same_loc st n0 =
       | Some W ->
           begin
           let check_value = Some (CoSt.get_check_value st) in
+          (* No need to add fault check in read modify write
+             situation, as the label will be assigned in read *)
+          let fault_update_without_rmw st =
+            if n.evt.rmw && E.is_one_rmw_instruction n.edge
+            then None,st else CoSt.fault_update st in
           match n.evt.loc with
           | Data _ ->
-            (* Helper function returns a fresh label and a boolean for if it should fault,
-               if a fault check is need. Otherwise return `None` *)
-            let fault_update st =
-              let check_fault, st = CoSt.read_and_unset_check_fault st in
-              let pte_val = CoSt.get_pte_value st in
-              (if do_kvm && check_fault then label_fault pte_val else None), st in
             let bank = n.evt.bank in
             begin match bank with
             | Instr -> Warn.fatal "instruction annotation to data bank not possible?"
             | Ord ->
               let st = set_write_val_ord st n in
-              let check_fault, st = fault_update st in
+              let check_fault, st = fault_update_without_rmw st in
               n.evt <- { n.evt with check_fault; check_value; };
               (next_x_ok, st)
             | Pair ->
@@ -938,7 +957,7 @@ let set_same_loc st n0 =
               assert (Array.length cell>=2) ;
               let st = CoSt.next_co st Ord in (* Pre-increment *)
               let st = set_write_val_ord st n in
-              let check_fault, st = fault_update st in
+              let check_fault, st = fault_update_without_rmw st in
               n.evt <- { n.evt with check_fault; check_value; };
               (next_x_ok, st)
             | Tag|CapaTag|CapaSeal ->
@@ -1118,28 +1137,30 @@ let do_set_read_v init =
         let check_value = Some (CoSt.get_check_value st) in
         begin match bank with
         | Ord | Instr->
-          set_read_individual_v n cell check_value
+          set_read_individual_v n cell check_value;
+          let check_fault, st = CoSt.fault_update st in
+          n.evt <- { n.evt with check_fault };
+          st
         | Pair ->
-          set_read_pair_v n cell check_value
+          set_read_pair_v n cell check_value;
+          let check_fault, st = CoSt.fault_update st in
+          n.evt <- { n.evt with check_fault };
+          st
         | VecReg a ->
           let cell = Array.map Code.value_to_int cell in
           let v = E.SIMD.read a cell
                    |> E.SIMD.reduce
                    |> Code.value_of_int in
-          n.evt <- { n.evt with v=v ; vecreg=[]; bank=Ord; check_value; }
+          let check_fault, st = CoSt.fault_update st in
+          n.evt <- { n.evt with v=v ; vecreg=[]; bank=Ord; check_value; check_fault ; };
+          st
         | Tag|CapaTag|CapaSeal ->
-          n.evt <- { n.evt with v = CoSt.get_co st bank; check_value; }
+          n.evt <- { n.evt with v = CoSt.get_co st bank; check_value; };
+          st
         | Pte ->
-          n.evt <- { n.evt with pte = CoSt.get_pte_value st; }
-        end ;
-        (* Update if this memory load might fault *)
-        let fault_update st =
-          let check_fault, st = CoSt.read_and_unset_check_fault st in
-          let pte_val = CoSt.get_pte_value st in
-            (if do_kvm && check_fault then label_fault pte_val else None), st in
-        let fault, st = fault_update st in
-        n.evt <- { n.evt with check_fault = fault };
-        st
+          n.evt <- { n.evt with pte = CoSt.get_pte_value st; };
+          st
+        end
       (* Update `st`, `cell` and `pte_cell` for future read events *)
       | Some W ->
         let st =

gen/edge.ml

@@ -72,6 +72,8 @@ module type S = sig
 
   type edge = { edge: tedge;  a1:atom option; a2: atom option; }
 
+  val is_one_rmw_instruction : edge -> bool
+
   val plain_edge : tedge -> edge
 
   val fold_atomo : (atom option -> 'a -> 'a) -> 'a -> 'a
@@ -458,6 +460,10 @@ let fold_tedges f r =
   let ok_rmw rmw a1 a2 =
     not (F.is_one_instruction rmw) || same_access_atoms a1 a2
 
+  let is_one_rmw_instruction e = match e.edge with
+    | Rmw rmw -> F.is_one_instruction rmw
+    | _ -> false
+
   let ok_non_rmw e a1 a2 =
     do_is_diff e || do_disjoint ||
     (overlap_atoms a1 a2 &&