Track register in Litmus CAS

src/litmus.ml

@@ -63,7 +63,7 @@ type instruction =
   | LoadLink of Register.t * MyLocation.t expr * Value.t * Value.t expr
   | Store of MyLocation.t expr * Value.t expr
   | StoreCnd of MyLocation.t expr * Value.t expr
-  | Cas of MyLocation.t expr * Value.t * Value.t expr
+  | Cas of Register.t option * MyLocation.t expr * Value.t * Value.t expr
   | Fence
 
 (** Simple pretty-printing of attributes (for debugging) *)
@@ -90,10 +90,18 @@ let pp_instr oc = function
      fprintf oc "sc(%a,%a%a)"
 	     (pp_expr MyLocation.pp) le (pp_expr Value.pp) ve
              pp_attrs attrs
-  | Cas (le,v,ve), attrs ->
-     fprintf oc "cas(%a,%a,%a%a)"
+  | Cas (None,le,v,ve), attrs ->
+     fprintf oc "cas(?,%a,%a,%a%a)"
              (pp_expr MyLocation.pp) le Value.pp v (pp_expr Value.pp) ve
              pp_attrs attrs
+  | Cas (Some r,le,v,ve), attrs ->
+     fprintf oc "cas(%a,%a,%a,%a%a)"
+             Register.pp r
+             (pp_expr MyLocation.pp) le
+             Value.pp v
+             (pp_expr Value.pp) ve
+             pp_attrs attrs
+
   | Fence, attrs ->
      fprintf oc "fence(%a)"
 	     (MyList.pp_gen "" (fun oc -> fprintf oc ",%s")) attrs

src/litmus_C.ml

@@ -146,9 +146,9 @@ let pp_instr dialect oc = function
         a separate StoreCnd instruction.  (We still print _something_,
         to avoid throwing off the indentation. *)
      fprintf oc "// elided store-conditional instruction"
-  | Litmus.Cas (obj,exp,des), attrs ->
+  | Litmus.Cas (r,obj,exp,des), attrs ->
      let mo = get_mo attrs in
-     pp_cas dialect oc mo obj None exp des
+     pp_cas dialect oc mo obj r exp des
 
   | Litmus.Fence, attrs ->
      let mo = get_mo attrs in
@@ -194,7 +194,7 @@ let partition_locs_in_instr s (a_locs, b_locs) = function
   | Litmus.LoadLink (_,le,_,_), attrs
   | Litmus.Store (le,_), attrs
   | Litmus.StoreCnd (le,_), attrs
-  | Litmus.Cas (le,_,_), attrs ->
+  | Litmus.Cas (_,le,_,_), attrs ->
      let l = Litmus.expr_base_of le in
      begin match List.mem s attrs with
      | true ->
@@ -221,13 +221,14 @@ let partition_locs s lt =
     CAS without a destination register.  (If one exists, we need to
     create a temporary variable to store it.) *)
 let rec contains_regless_cas = function
-  | Litmus.Basic (Litmus.Cas (_, _, _), _) -> true
+  | Litmus.Basic (Litmus.Cas (None, _, _, _), _) -> true
   | Litmus.Basic _ -> false
   | Litmus.If (_,_,cs) -> List.exists contains_regless_cas cs
 
 let rec extract_regs regs = function
   | Litmus.Basic (Litmus.Load (r,_), _)
-    | Litmus.Basic (Litmus.LoadLink (r,_,_,_), _) -> MySet.union [r] regs
+    | Litmus.Basic (Litmus.LoadLink (r,_,_,_), _)
+    | Litmus.Basic (Litmus.Cas (Some r,_,_,_), _) -> MySet.union [r] regs
   | Litmus.Basic _ -> regs
   | Litmus.If (r,_,cs) -> MySet.union [r] (List.fold_left extract_regs regs cs)
 

src/litmus_OpenCL.ml

@@ -103,10 +103,10 @@ let pp_instr pp_loc oc = function
         to avoid throwing off the indentation. *)
      fprintf oc "// elided store-conditional instruction"
 
-  | Litmus.Cas (obj,exp,des), attrs ->
+  | Litmus.Cas (r,obj,exp,des), attrs ->
      let mo = Litmus_C.get_mo attrs in
      let ms = get_ms attrs in
-     pp_cas pp_loc oc mo ms obj None exp des
+     pp_cas pp_loc oc mo ms obj r exp des
 
   | Litmus.Fence, attrs ->
      let mo = Litmus_C.get_mo attrs in
@@ -140,7 +140,7 @@ let partition_locs_in_instr s (a_locs, na_locs) = function
   | Litmus.LoadLink (_,le,_,_), attrs
   | Litmus.Store (le,_), attrs
   | Litmus.StoreCnd (le,_), attrs
-  | Litmus.Cas (le,_,_), attrs ->
+  | Litmus.Cas (_,le,_,_), attrs ->
      let l = Litmus.expr_base_of le in
      begin match List.mem s attrs with
      | true ->

src/mk_litmus.ml

@@ -57,7 +57,10 @@ let mk_instr x maps reg_map e =
        let rval = List.assoc e maps.Exec.rval_map in
        let wval = List.assoc e maps.Exec.wval_map in
        let wval_expr = Litmus.mk_expr wval d_regs in
-       Litmus.Cas (loc_expr, rval, wval_expr)
+       (* Some CAS events spill their expected value into a register,
+          but this isn't guaranteed. *)
+       let reg = List.assoc_opt e reg_map in
+       Litmus.Cas (reg, loc_expr, rval, wval_expr)
     | true, false, false ->
        let reg = reg_of e in
        let loc = List.assoc e maps.Exec.loc_map in