[litmus] Permit initializing shared-memory locations with labels

herd · Mar 19, 2024 · aa6fff8 · aa6fff8
1 parent 2f2663d
commit aa6fff8
Show file tree

Hide file tree

Showing 2 changed files with 46 additions and 16 deletions.
diff --git a/litmus/skel.ml b/litmus/skel.ml
@@ -369,9 +369,11 @@ module Make
                vs in
            sprintf "{%s}" (String.concat "" pps)
         | Symbolic _|Tag _|PteVal _|Frozen _|ConcreteRecord _ -> assert false
-        | Label _ ->
-            Warn.user_error
-              "Labels cannot be used as initial values of memory locations"
+        | Label (p,lab) ->
+          if do_self then
+            sprintf "_a->P%d_%s[_i]" p lab
+          else
+            sprintf "_a->P%d_%s" p lab
         | Instruction i -> A.GetInstr.instr_name i
 
 (* Dump left & right values when context is available *)
@@ -767,6 +769,7 @@ module Make
             | Indirect,_,_->
                 O.fi "%s%s *%s;" pp_t indirect_star s)
           test.T.globals ;
+        (* TODO *)
         begin match memory with
         | Direct -> []
         | Indirect ->
@@ -1546,10 +1549,16 @@ module Make
               O.fi "_sz = _a->%s * size_of_test * sizeof(ins_t);"
                 (fmt_code_size n) ;
               O.fi "_a->code%i = mmap_exec(_sz);" n)
-            test.T.code
+            test.T.code;
+            Label.Full.Set.iter
+            (fun (p,lab) ->
+              let lblname = sprintf "P%d_%s" p lab in
+              O.fi "_a->%s = malloc_check(size_of_test*sizeof(*(_a->%s)));" lblname lblname;
+            )
+            CfgLoc.label_init;
         end else begin
           UD.initialise_labels "_a" CfgLoc.label_init
-        end ;
+        end;
         O.o "}" ;
         O.o "" ;
 
@@ -1648,6 +1657,14 @@ module Make
         | Direct -> ()
         end ;
         loop_test_prelude indent "_a->_p->" ;
+        if do_self then begin
+          List.iteri
+            (fun n _ ->
+              O.fii "ins_t *_dst%i = &_a->code%i[_i*_a->code%i_sz], *_src%i=(ins_t *)code%i;" n n n n n ;
+              O.fii "for (int _k = _a->code%i_sz-1 ; _k >= 0 ; _k--) _dst%i[_k] = _src%i[_k];" n n n)
+            test.T.code
+        end ;
+        UD.reinitialise_labels "_a" "_i" CfgLoc.label_init;
         List.iter
           (fun (a,t) ->
             let v = A.find_in_state (A.location_of_addr a) test.T.init in
@@ -1708,13 +1725,6 @@ module Make
             O.oii "_a->barrier[_i] = 0;"
         | Pthread|NoBarrier|User2|TimeBase -> ()
         end ;
-        if do_self then begin
-          List.iteri
-            (fun n _ ->
-              O.fii "ins_t *_dst%i = &_a->code%i[_i*_a->code%i_sz], *_src%i=(ins_t *)code%i;" n n n n n ;
-              O.fii "for (int _k = _a->code%i_sz-1 ; _k >= 0 ; _k--) _dst%i[_k] = _src%i[_k];" n n n)
-            test.T.code
-        end ;
         O.oi "}" ;
         if Cfg.cautious then O.oi "mcautious();" ;
         begin match barrier with
@@ -2423,9 +2433,8 @@ module Make
             O.fi "size_t code%i_sz,%s;" n (OutUtils.fmt_prelude n) ;
             O.fi "ins_t *code%i;" n
           done
-        end else begin
-            UD.define_label_fields CfgLoc.label_init
         end;
+        UD.define_label_fields CfgLoc.label_init;
         O.o "} ctx_t;" ;
         O.o "" ;
         if do_staticalloc then begin

diff --git a/litmus/skelUtil.ml b/litmus/skelUtil.ml
@@ -213,6 +213,11 @@ module Make
            first argument is a pointer to struct *)
         val initialise_labels : string -> Label.Full.Set.t -> unit
 
+        (* Dump reinitialisation code of label constants,
+           first argument is a pointer to struct,
+           second argument is index identifying the code copy *)
+        val reinitialise_labels : string -> string -> Label.Full.Set.t -> unit
+
         (* Dump definition of label offsets, _i.e_ offset from code start *)
         val define_label_offsets : T.t -> Label.Full.Set.t -> unit
 
@@ -655,9 +660,12 @@ end
           if not (Label.Full.Set.is_empty lbls) then begin
             let pp =
               Label.Full.Set.pp_str ","
-                (fun (p,lbl) -> "*" ^ OutUtils.fmt_lbl_var p lbl)
+                (fun (p,lbl) ->
+                  let pointer_type =
+                    if (Cfg.variant Variant_litmus.Self) then "**" else "*" in
+                  pointer_type ^ OutUtils.fmt_lbl_var p lbl)
                 lbls in
-            O.fi "ins_t %s;"pp
+            O.fi "ins_t %s;" pp
           end
 
         let check_ascall () =
@@ -687,6 +695,19 @@ end
             label_init ;
           ()
 
+          let reinitialise_labels ptr idx label_init =
+            let open OutUtils in
+            Label.Full.Set.iter
+              (fun (p,lbl) ->
+                O.fi
+                  "%s->%s[%s] = _dst%i+%s->%s+%s;" ptr
+                  (fmt_lbl_var p lbl) idx
+                  p
+                  ptr (fmt_prelude p)
+                  (fmt_lbl_offset p lbl))
+              label_init ;
+            ()
+
 (* Output offset of labels *)
         let define_label_offsets test lbls =
           if not (Label.Full.Set.is_empty lbls) then begin