Skip to content

Commit

Permalink
I annotation on reads and reject Plain eating I
Browse files Browse the repository at this point in the history
This commit changes the function of the I annotation to work on Reads
instead of Writes.
This commit also stops Plain annotations from eating Instr annotation,
to allow the user to specify relaxations where reads/writes cannot
become Instr
  • Loading branch information
hugookeeffe committed Oct 18, 2024
1 parent bddda2c commit 870fc1f
Show file tree
Hide file tree
Showing 6 changed files with 45 additions and 40 deletions.
9 changes: 7 additions & 2 deletions gen/AArch64Arch_gen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,8 @@ let applies_atom (a,_) d = match a,d with
| Rel _,W
| Pte (Read|ReadAcq|ReadAcqPc),R
| Pte (Set _|SetRel _),W
| (Plain _|Atomic _|Tag|CapaTag|CapaSeal|Neon _|Pair _|Instr),(R|W)
| Instr, R
| (Plain _|Atomic _|Tag|CapaTag|CapaSeal|Neon _|Pair _),(R|W)
-> true
| _ -> false

Expand Down Expand Up @@ -383,7 +384,11 @@ let is_ifetch a = match a with
let r = f (Acq o) r in
let r = f (AcqPc o) r in
let r = f (Rel o) r in
let r = f Instr r in
let r =
if do_self then
let r = f Instr r in
r
else r in
r

let fold_acc mixed f r =
Expand Down
13 changes: 8 additions & 5 deletions gen/AArch64Compile_gen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1729,15 +1729,18 @@ module Make(Cfg:Config) : XXXCompile_gen.S =
| None,_ -> Warn.fatal "AArchCompile.emit_access"
| Some d,Code lab ->
begin match d,e.C.atom with
| R,None ->
| R,Some (Instr, None) ->
let r,init,cs,st = LDR.emit_fetch st p init lab in
Some r,init,cs,st
| W,(None | Some (Instr, None)) ->
let init,cs,st = STR.emit_store_nop st p init lab in
None,init,cs,st
| R, Some (Instr, None) ->
(* 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
Some r,init,cs,st
| W, Some(Instr, None) *)
| W, None ->
let init,cs,st = STR.emit_store_nop st p init lab in
None,init,cs,st
| _,_ -> Warn.fatal "Not Yet (%s,%s)!!!"
(pp_dir d) (C.debug_evt e)
end
Expand Down
38 changes: 21 additions & 17 deletions gen/cycle.ml
Original file line number Diff line number Diff line change
Expand Up @@ -574,6 +574,8 @@ let patch_edges n =
exception FailMerge

let merge2 a1 a2 = match a1,a2 with
| (None,Some a)
| (Some a,None) when E.is_ifetch (Some a) -> raise FailMerge
| (None,a)|(a,None) -> a
| Some a1,Some a2 ->
match E.merge_atoms a1 a2 with
Expand Down Expand Up @@ -709,25 +711,25 @@ let remove_store n0 =
(* Set locations of events *)
(***************************)

let is_read_same_nonfetch m =
let is_read_same_fetch m =
let check n = (n != m && (loc_compare n.evt.loc m.evt.loc) = 0 && n.evt.dir = Some R &&
not (E.is_ifetch n.edge.E.a1)) in
(E.is_ifetch n.edge.E.a1)) in
try ignore (find_node_prev (fun n -> check n) m); true
with Not_found -> false

let check_fetch n0 =
let rec do_rec m =
(* ensure Instr read is followed or preceded by plain read to same location*)
begin match m.evt.loc, m.evt.dir with
| Code.Code _, Some R when not (E.is_ifetch m.edge.E.a1) ->
if is_read_same_nonfetch m then begin
| Code.Code _, Some R when (E.is_ifetch m.edge.E.a1) ->
if is_read_same_fetch m then begin
Warn.user_error "Multiple ifetch reads to same code location [%s]" (str_node m)
end;
| Code.Code _, Some R when E.is_ifetch m.edge.E.a1 ->
if not (is_read_same_nonfetch m) then begin
| Code.Code _, Some R when not (E.is_ifetch m.edge.E.a1) ->
if not (is_read_same_fetch m) then begin
Warn.user_error "Reading from label that doesn't exist [%s]" (str_node m)
end;
| Code.Code _, Some W when not (E.is_ifetch m.edge.E.a1) ->
| Code.Code _, Some W when (E.is_ifetch m.edge.E.a1) ->
Warn.user_error "Writing non-instruction value to code location: [%s]" (str_node m)
| _ -> ();
end;
Expand All @@ -743,10 +745,12 @@ let set_diff_loc st n0 =
end
else
let n1 = try
(* check if new location needs to be ifetch *)
find_node
(fun n -> (if not (same_loc n.prev.edge) then raise Not_found); E.is_ifetch n.edge.E.a1 ) m.next
with Not_found -> m in
with Not_found -> try
find_node_prev
(fun n -> (if not (same_loc n.edge) then raise Not_found); E.is_ifetch n.edge.E.a2 ) m.prev
with Not_found -> m in
next_loc n1.edge st in
m.evt <- { m.evt with loc=loc ; bank=E.atom_to_bank m.evt.atom; } ;
(* eprintf "LOC SET: %a [p=%a]\n%!" debug_node m debug_node p; *)
Expand Down Expand Up @@ -853,7 +857,8 @@ let set_same_loc st n0 =
| Data _ ->
let bank = n.evt.bank in
begin match bank with
| Ord | Instr ->
| Instr -> Warn.fatal "instruction annotation to data bank not possible?"
| Ord ->
let st = set_write_val_ord st n in
do_set_write_val next_x_ok st pte_val ns
| Pair ->
Expand Down Expand Up @@ -909,7 +914,8 @@ let set_same_loc st n0 =
| Code _ ->
let bank = n.evt.bank in
begin match bank with
| Instr ->
| Instr -> Warn.fatal "not letting instr write happen"
| Ord ->
let st = CoSt.next_co st bank in
let v = CoSt.get_co st bank in
n.evt <- { n.evt with ins = v;} ;
Expand Down Expand Up @@ -1018,7 +1024,7 @@ let do_set_read_v =
begin match n.evt.dir with
| Some R ->
begin match bank with
| Ord ->
| Ord | Instr->
set_read_v n cell
| Pair ->
set_read_pair_v n cell
Expand All @@ -1030,18 +1036,16 @@ let do_set_read_v =
n.evt <- { n.evt with v = CoSt.get_co st bank; }
| Pte ->
n.evt <- { n.evt with pte = pte_cell; }
| Instr ->
n.evt <- { n.evt with ins = CoSt.get_co st bank; }
end ;
do_rec st cell pte_cell ns
| Some W ->
let st =
match bank with
| Tag|CapaTag|CapaSeal ->
CoSt.set_co st bank n.evt.v
|Instr -> CoSt.set_co st bank n.evt.ins
| Pte|Ord|Pair|VecReg _ ->
st in
| Pte|Ord|Pair|VecReg _| Instr ->
if Code.is_data n.evt.loc then st
else CoSt.set_co st bank n.evt.ins in
do_rec st
(match bank with
| Ord|Pair|VecReg _ ->
Expand Down
14 changes: 8 additions & 6 deletions gen/edge.ml
Original file line number Diff line number Diff line change
Expand Up @@ -649,10 +649,10 @@ let fold_tedges f r =
if do_self && F.instr_atom != None then
iter_ie
(fun ie ->
add_lxm (sprintf "Iff%s" (pp_ie ie)) { a1=F.instr_atom; a2=None; edge=(Rf ie); } ;
add_lxm (sprintf "Irf%s" (pp_ie ie)) { a1=F.instr_atom; a2=None; edge=(Rf ie); } ;
add_lxm (sprintf "Fif%s" (pp_ie ie)) { a1=None; a2=F.instr_atom; edge=(Fr ie); } ;
add_lxm (sprintf "Ifr%s" (pp_ie ie)) { a1=None; a2=F.instr_atom; edge=(Fr ie); }) ;
add_lxm (sprintf "Iff%s" (pp_ie ie)) { a1=None; a2=F.instr_atom; edge=(Rf ie); } ;
add_lxm (sprintf "Irf%s" (pp_ie ie)) { a1=None; a2=F.instr_atom; edge=(Rf ie); } ;
add_lxm (sprintf "Fif%s" (pp_ie ie)) { a1=F.instr_atom; a2=None; edge=(Fr ie); } ;
add_lxm (sprintf "Ifr%s" (pp_ie ie)) { a1=F.instr_atom; a2=None; edge=(Fr ie); });
()


Expand Down Expand Up @@ -737,8 +737,8 @@ let fold_tedges f r =
| _ -> false

let is_fetch e = match e.edge with
| Rf _ -> is_ifetch e.a1
| Fr _ -> is_ifetch e.a2
| Rf _ -> is_ifetch e.a2
| Fr _ -> is_ifetch e.a1
| _ -> is_ifetch e.a1 || ( loc_sd e = Same && is_ifetch e.a2)

let compat_atoms a1 a2 = match F.merge_atoms a1 a2 with
Expand Down Expand Up @@ -883,6 +883,8 @@ let fold_tedges f r =
let r =
match a1,a2 with
| None,None -> e1,e2
| None,Some a
| Some a,None when F.is_ifetch (Some a)-> e1, e2
| None,Some _ -> set_a2 e1 a2,e2
| Some _,None -> e1, set_a1 e2 a1
| Some a1,Some a2 ->
Expand Down
4 changes: 1 addition & 3 deletions gen/final.ml
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,7 @@ module Make : functor (O:Config) -> functor (C:ArchRun.S) ->
| Code.CapaSeal
| Code.Ord
| Code.Pair
| Code.Instr
->
Some (I evt.C.C.v)
| Code.VecReg _->
Expand All @@ -186,9 +187,6 @@ module Make : functor (O:Config) -> functor (C:ArchRun.S) ->
Some (S (Code.add_tag (Code.as_data evt.C.C.loc) evt.C.C.v))
| Code.Pte ->
Some (P evt.C.C.pte)
| Code.Instr ->
let s = C.A.pp_i evt.C.C.ins in
Some (S s)
end
| Some Code.W ->
assert (evt.C.C.bank = Code.Ord || evt.C.C.bank = Code.CapaSeal) ;
Expand Down
7 changes: 0 additions & 7 deletions gen/top_gen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -257,16 +257,9 @@ let get_fence n =
begin match o with
| None -> finals (* Code write *)
| Some r -> (* fetch! *)
match n.C.prev.C.edge.E.edge, n.C.edge.E.edge with
| E.Rf _, _ when E.is_ifetch n.C.prev.C.edge.E.a2 ->
F.add_final (A.get_friends st) p o n finals
| _, E.Po _ | _, E.Fr _ when E.is_ifetch n.C.edge.E.a1 ->
F.add_final (A.get_friends st) p o n finals
| _, _-> begin
let m,fenv = finals in
m,F.add_final_v p r (IntSet.singleton (U.fetch_val n))
fenv
end
end),
st
end
Expand Down

0 comments on commit 870fc1f

Please sign in to comment.