Merge pull request herd#1175 from relokin/cas-fix

[herd] Consolidate alternative executions of a failed CAS

Author: relokin

herd/AArch64Sem.ml

@@ -1989,7 +1989,9 @@ module Make
           let read_mem a =
             if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii
             else do_read_mem_ret sz an aexp ac a ii in
-          M.aarch64_cas_no (Access.is_physical ac) ma read_rs write_rs read_mem branch M.neqT
+          let noact _ _ = M.mk_singleton_es Act.NoAction ii in
+          M.aarch64_cas_no (Access.is_physical ac) ma read_rs write_rs read_mem
+            noact branch M.neqT
         in
         let mop_fail_with_wb ac ma _ =
           (* CAS fails, there is an Explicit Write Effect writing back *)
@@ -1998,8 +2000,8 @@ module Make
             if noret then do_read_mem_ret sz Annot.NoRet aexp ac a ii
             else rmw_amo_read sz rmw ac a ii
           and write_mem a v = rmw_amo_write sz rmw ac a v ii in
-          M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs write_rs
-                                      read_mem write_mem branch M.neqT
+          M.aarch64_cas_no (Access.is_physical ac) ma read_rs write_rs
+            read_mem write_mem branch M.neqT
         in
         let mop_success ac ma mv =
           (* CAS succeeds, there is an Explicit Write Effect *)
@@ -2058,22 +2060,23 @@ module Make
           (* CASP fails, there are no Explicit Write Effects *)
           let read_mem a = do_read_mem_ret sz an aexp ac a ii
                 >>| (add_size a sz
-                >>= fun a -> do_read_mem_ret sz an aexp ac a ii) in
+                     >>= fun a -> do_read_mem_ret sz an aexp ac a ii) in
+          let noact _ _ = M.mk_singleton_es Act.NoAction ii in
           M.aarch64_cas_no (Access.is_physical ac) ma read_rs
-              write_rs read_mem branch neqp
+              write_rs read_mem noact branch neqp
         in
         let mop_fail_with_wb ac ma _ =
           (* CASP fails, there are Explicit Write Effects writing back *)
           (* the value that is already in memory                       *)
-          let read_mem a = do_read_mem_ret sz an aexp ac a ii
+          let read_mem a = rmw_amo_read sz rmw ac a ii
                 >>| (add_size a sz
-                >>= fun a -> do_read_mem_ret sz an aexp ac a ii)
+                >>= fun a -> rmw_amo_read sz rmw ac a ii)
           and write_mem a (v1,v2) =
               rmw_amo_write sz rmw ac a v1 ii
               >>| (add_size a sz >>= fun a2 ->
                   rmw_amo_write sz rmw ac a2 v2 ii)
               >>= fun _ -> M.unitT () in
-          M.aarch64_cas_no_with_writeback (Access.is_physical ac) ma read_rs
+          M.aarch64_cas_no (Access.is_physical ac) ma read_rs
               write_rs read_mem write_mem branch neqp
         in
         let mop_success ac ma _ =

herd/ASLAction.ml

@@ -265,6 +265,10 @@ module Make (C: Config) (A : S) = struct
     | Branching _ -> true
     | Access _|Barrier _|CutOff _|NoAction -> false
 
+  let is_no_action = function
+    | NoAction -> true
+    | _ -> false
+
   (* Unrolling control *)
   let cutoff msg = CutOff msg
   let is_cutoff = function

herd/BellAction.ml

@@ -200,6 +200,8 @@ end = struct
 
   let is_commit = is_bcc
 
+  let is_no_action _ = false
+
 (* Unroll control *)
   let cutoff msg = CutOff msg
   let is_cutoff = function

herd/CAction.ml

@@ -262,6 +262,8 @@ end = struct
   let is_pred ?cond:_ _ = false
   let is_commit _ = false
 
+  let is_no_action _ = false
+
 (* Unrolling control *)
   let cutoff msg = CutOff msg
   let is_cutoff = function

herd/JavaAction.ml

@@ -200,6 +200,8 @@ end = struct
   let is_pred ?cond:_ _ = false
   let is_commit _ = false
 
+  let is_no_action _ = false
+
   include Explicit.NoAction
 
   let annot_in_list _ _ = false

herd/action.mli

@@ -97,6 +97,8 @@ module type S = sig
   val is_pred : ?cond:string option -> action -> bool
   val is_commit : action -> bool
 
+  val is_no_action : action -> bool
+
 (* Unrolling control *)
   val cutoff : string -> action
   val is_cutoff : action -> bool

herd/event.ml

@@ -468,14 +468,9 @@ val same_instance : event -> event -> bool
           event_structure ->  event_structure ->  event_structure ->
             event_structure
 
-  val aarch64_cas_no :
-    bool -> (* Physical memory access *)
-    bool -> (* Add an iico_ctrl between the Branch and the Register Write *)
-    event_structure -> event_structure -> event_structure ->
-    event_structure -> event_structure -> event_structure
-
-  val aarch64_cas_ok :
-    bool (* Physical memory access *) -> [`DataFromRRs | `DataFromRx] ->
+  val aarch64_cas :
+    bool (* Physical memory access *) ->
+    [< `DataFromRRs | `DataFromRx | `No] ->
     event_structure -> event_structure -> event_structure ->
     event_structure ->  event_structure ->  event_structure ->
     event_structure -> event_structure
@@ -2327,79 +2322,8 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
           resa.aligned @ data.aligned @ addr.aligned
           @ wres.aligned @ wresult.aligned @ wmem.aligned ;}
 
-(* AArch64 CAS, failure *)
-    let aarch64_cas_no is_phy add_ctrl rn rs wrs rm br =
-      let input_wrs = minimals wrs
-      and input_rm = minimals rm
-      and input_br = minimals br in
-      { procs = [] ;
-        events =
-        EventSet.union5
-          rn.events rs.events wrs.events rm.events br.events;
-        speculated =
-        if do_deps then
-          EventSet.union5
-            rn.speculated rs.speculated wrs.speculated rm.speculated br.speculated
-        else rn.speculated;
-        po = po_union5 rn rs wrs rm br;
-        partial_po = partial_po_union5 rn rs wrs rm br;
-        intra_causality_data =
-        EventRel.union
-          (EventRel.union5
-             rn.intra_causality_data
-             rs.intra_causality_data
-             wrs.intra_causality_data
-             rm.intra_causality_data
-             br.intra_causality_data)
-          (EventRel.union4
-             (EventRel.cartesian (get_output rn) input_rm) (* D1 *)
-             (EventRel.cartesian (get_output rm) input_wrs)    (* Df1 *)
-             (EventRel.cartesian (get_output rm) input_br)
-             (EventRel.cartesian (get_output rs) input_br)
-          );
-        intra_causality_control =
-          (if is_branching && is_phy then
-             EventRel.union
-               (EventRel.cartesian (get_ctrl_output_commits rn) input_rm)
-           else Misc.identity)
-          ((if add_ctrl then
-             EventRel.union
-               (EventRel.cartesian (get_output br) input_wrs)
-            else Misc.identity)
-          (EventRel.union5
-             rn.intra_causality_control rs.intra_causality_control
-             wrs.intra_causality_control rm.intra_causality_control
-             br.intra_causality_control)) ;
-        intra_causality_order =
-          EventRel.union5
-            rn.intra_causality_order rs.intra_causality_order
-            wrs.intra_causality_order rm.intra_causality_order
-            br.intra_causality_order;
-        control =
-        EventRel.union5 rn.control rs.control rm.control wrs.control br.control;
-        data_ports =
-        EventSet.union5
-          rn.data_ports rs.data_ports
-          wrs.data_ports rm.data_ports br.data_ports;
-        success_ports =
-        EventSet.union5
-          rn.success_ports rs.success_ports
-          wrs.success_ports rm.success_ports br.success_ports;
-        sca =
-        EventSetSet.union5
-          rn.sca rs.sca wrs.sca rm.sca br.sca;
-        mem_accesses =
-        EventSet.union5
-          rn.mem_accesses rs.mem_accesses
-          wrs.mem_accesses rm.mem_accesses br.mem_accesses;
-        input=None; data_input=None;
-        output = Some (maximals wrs);
-        ctrl_output = None ;
-        aligned = rn.aligned @ rs.aligned @ wrs.aligned @ rm.aligned @ br.aligned;
-      }
-
-(* AArch64 CAS, success *)
-    let aarch64_cas_ok is_phy prov_data rn rs rt wrs rm wm br =
+(* AArch64 CAS *)
+    let aarch64_cas is_phy mode rn rs rt wrs rm wm br =
       let input_wrs = minimals wrs
       and input_rm = minimals rm
       and input_wm = minimals wm
@@ -2428,18 +2352,34 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
                 rm.intra_causality_data;
                 br.intra_causality_data;
                 wm.intra_causality_data])
-          (let output_rn = get_output rn
-           and output_prov_data = match prov_data with
-             | `DataFromRRs -> get_output rs
-             | `DataFromRx -> get_output rm
-           in
-           EventRel.unions
-             [(EventRel.cartesian output_rn input_rm);          (* D1 *)
-              (EventRel.cartesian output_rn input_wm);          (* Ds2 *)
-              (EventRel.cartesian (get_output rt) input_wm);    (* Ds3 *)
-              (EventRel.cartesian output_prov_data input_wrs);
+          (let output_rn = get_output rn in
+           (* Data for the Register Write Effect of Ws *)
+           let wrs_data =  match mode with
+             | `DataFromRRs ->
+               [EventRel.cartesian (get_output rs) input_wrs; ]
+             | `DataFromRx | `No ->
+               [EventRel.cartesian (get_output rm) input_wrs; ] in
+           (* Address for the Write Memory Effect *)
+           let wm_addr = [EventRel.cartesian output_rn input_wm; ]
+           (* Data for the Write Memory Effect *)
+           and wm_data = match mode with
+             | `DataFromRRs | `DataFromRx ->
+               [EventRel.cartesian (get_output rt) input_wm; ]
+             | `No ->
+               [EventRel.cartesian (get_output rm) input_wm; ] in
+           (* Handle the case where wm is NoAction *)
+           let wm_rels = match EventSet.elements wm.events with
+             | [evt] when Act.is_no_action evt.action ->
+               []
+             | evts when List.for_all is_mem_store evts  ->
+               wm_data @ wm_addr
+             | _ -> assert false in
+           let rels =
+             wrs_data @ wm_rels @
+             [(EventRel.cartesian output_rn input_rm);
               (EventRel.cartesian (get_output rs) input_br);
-              (EventRel.cartesian (get_output rm) input_br);]
+              (EventRel.cartesian (get_output rm) input_br);] in
+           EventRel.unions rels
           );
         intra_causality_control =
         EventRel.union
@@ -2457,9 +2397,10 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
                 EventRel.cartesian (get_ctrl_output_commits rn)
                   (EventSet.union input_rm input_wm)
               else EventRel.empty)
-             (match prov_data with
+             (match mode with
               | `DataFromRRs -> EventRel.cartesian output_br input_wrs
-              | `DataFromRx -> EventRel.empty)
+              | `DataFromRx
+              | `No -> EventRel.empty)
              (EventRel.cartesian output_br input_wm)   (* Cs1 *)
              (EventRel.cartesian output_br input_wm)); (* Cs2 *)
         intra_causality_order =

herd/eventsMonad.ml

@@ -577,75 +577,6 @@ Monad type:
           read_addr (eiid,Evt.empty) in
       eiid,(acts,None)
 
-(* AArch64 failed cas *)
-    let do_aarch64_cas_no
-        (is_physical:bool)
-        (add_ctrl:bool)
-        (read_rn:'loc t) (read_rs:'v t)
-        (write_rs:'v-> unit t)
-        (read_mem: 'loc -> 'v t)
-        (branch: 'loc -> unit t)
-        (rne: 'v -> 'v -> unit t)
-        eiid =
-      let eiid,read_rn = read_rn eiid in
-      let eiid,read_rs = read_rs eiid in
-      let cv,cl_cv,es_rs = Evt.as_singleton_nospecul read_rs in
-      let acts_rn,spec = read_rn in
-      assert (Misc.is_none spec) ;
-      let eiid,acts =
-        Evt.fold
-          (fun  (a,cl_a,es_rn) (eiid,acts) ->
-            let eiid,read_mem = read_mem a eiid in
-            let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem in
-            let eiid,write_rs = write_rs ov eiid in
-            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
-            let eiid,branch = branch a eiid in
-            let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
-            let eiid,nem = rne ov cv eiid in
-            let (),cl_ne,eseq =  Evt.as_singleton_nospecul nem in
-            assert (E.is_empty_event_structure eseq) ;
-            let es =
-              E.aarch64_cas_no is_physical add_ctrl es_rn es_rs es_wrs es_rm es_br in
-            let cls = cl_a@cl_cv@cl_rm@cl_wrs@cl_ne@cl_br  in
-            eiid,Evt.add ((),cls,es) acts)
-          acts_rn (eiid,Evt.empty) in
-      eiid,(acts, None)
-
-(* AArch64 failed cas that writes into memory nevertheless *)
-    let do_aarch64_cas_no_with_writeback
-        (is_physical:bool)
-        (read_rn:'loc t) (read_rs:'v t)
-        (write_rs:'v-> unit t)
-        (read_mem: 'loc -> 'v t) (write_mem: 'loc -> 'v -> unit t)
-        (branch: 'loc -> unit t)
-        (rne: 'v -> 'v -> unit t)
-        eiid =
-      let eiid,read_rn = read_rn eiid in
-      let eiid,read_rs = read_rs eiid in
-      let cv,cl_cv,es_rs = Evt.as_singleton_nospecul read_rs in
-      let acts_rn,spec = read_rn in
-      assert (Misc.is_none spec) ;
-      let eiid,acts =
-        Evt.fold
-          (fun (a,cl_a,es_rn) (eiid,acts) ->
-            let eiid,read_mem = read_mem a eiid in
-            let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem in
-            let eiid,write_mem = write_mem a ov eiid in
-            let (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in
-            let eiid,write_rs = write_rs ov eiid in
-            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
-            let eiid,branch = branch a eiid in
-            let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
-            let eiid,nem = rne ov cv eiid in
-            let (),cl_ne,eseq =  Evt.as_singleton_nospecul nem in
-            assert (E.is_empty_event_structure eseq) ;
-            let es =
-              E.aarch64_cas_ok is_physical `DataFromRx es_rn es_rs E.empty_event_structure es_wrs es_rm es_wm es_br in
-            let cls = cl_a@cl_cv@cl_rm@cl_wm@cl_wrs@cl_br@cl_ne  in
-            eiid,Evt.add ((),cls,es) acts)
-          acts_rn (eiid,Evt.empty) in
-      eiid,(acts, None)
-
 (* AArch64 successful cas *)
     let do_aarch64_cas_ok
         (is_physical:bool) (prov_data: [`DataFromRRs | `DataFromRx])
@@ -677,7 +608,7 @@ Monad type:
             let (),cl_eq,eseq =  Evt.as_singleton_nospecul eqm in
             assert (E.is_empty_event_structure eseq) ;
             let es =
-              E.aarch64_cas_ok is_physical prov_data es_rn es_rs es_rt es_wrs es_rm es_wm es_br in
+              E.aarch64_cas is_physical prov_data es_rn es_rs es_rt es_wrs es_rm es_wm es_br in
             let cls = cl_a@cl_cv@cl_nv@cl_rm@cl_wm@cl_wrs@cl_br@cl_eq  in
             eiid,Evt.add ((),cls,es) acts)
           acts_rn (eiid,Evt.empty) in
@@ -737,20 +668,35 @@ Monad type:
       in
       altT (do_ `DataFromRRs) (do_ `DataFromRx)
 
-    let aarch64_cas_no (is_physical:bool) (read_rn:'loc t) (read_rs:'v t)
-        (write_rs:'v-> unit t) (read_mem: 'loc -> 'v t) (branch: 'loc -> unit t)
-        (rne: 'v -> 'v -> unit t) =
-      let do_ add_ctrl =
-        do_aarch64_cas_no is_physical add_ctrl read_rn read_rs write_rs
-          read_mem branch rne
-      in
-      altT (do_ true) (do_ false)
-
-    let aarch64_cas_no_with_writeback (is_physical: bool) (read_rn: 'loc t)
+    let aarch64_cas_no (is_physical: bool) (read_rn: 'loc t)
         (read_rs: 'v t) (write_rs: 'v -> unit t) (read_mem: 'loc -> 'v t)
-        (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (rne: 'v -> 'v -> unit t) =
-      do_aarch64_cas_no_with_writeback is_physical read_rn read_rs
-          write_rs read_mem write_mem branch rne
+        (write_mem: 'loc -> 'v -> unit t) (branch: 'loc -> unit t) (rne: 'v -> 'v -> unit t)
+        eiid =
+      let eiid,read_rn = read_rn eiid in
+      let eiid,read_rs = read_rs eiid in
+      let cv,cl_cv,es_rs = Evt.as_singleton_nospecul read_rs in
+      let acts_rn,spec = read_rn in
+      assert (Misc.is_none spec) ;
+      let eiid,acts =
+        Evt.fold
+          (fun (a,cl_a,es_rn) (eiid,acts) ->
+            let eiid,read_mem = read_mem a eiid in
+            let ov,cl_rm,es_rm = Evt.as_singleton_nospecul read_mem in
+            let eiid,write_mem = write_mem a ov eiid in
+            let (),cl_wm,es_wm= Evt.as_singleton_nospecul write_mem in
+            let eiid,write_rs = write_rs ov eiid in
+            let (),cl_wrs,es_wrs = Evt.as_singleton_nospecul write_rs in
+            let eiid,branch = branch a eiid in
+            let (),cl_br,es_br =  Evt.as_singleton_nospecul branch in
+            let eiid,nem = rne ov cv eiid in
+            let (),cl_ne,eseq =  Evt.as_singleton_nospecul nem in
+            assert (E.is_empty_event_structure eseq) ;
+            let es =
+              E.aarch64_cas is_physical `No es_rn es_rs E.empty_event_structure es_wrs es_rm es_wm es_br in
+            let cls = cl_a@cl_cv@cl_rm@cl_wm@cl_wrs@cl_br@cl_ne  in
+            eiid,Evt.add ((),cls,es) acts)
+          acts_rn (eiid,Evt.empty) in
+      eiid,(acts, None)
 
     (* RISCV store conditional may always succeed? *)
     let riscv_store_conditional = aarch64_or_riscv_store_conditional false