Skip to content

GitLab

Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit ac7b7bd5 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work

parents dff562c4 a05f9278
Hide whitespace changes
Inline Side-by-side
Showing with 370 additions and 566 deletions
Makefile
View file @ ac7b7bd5
......@@ -297,6 +297,7 @@ compcert.ini: Makefile.config
echo "linker_options=$(CLINKER_OPTIONS)";\
echo "arch=$(ARCH)"; \
echo "model=$(MODEL)"; \
echo "os=$(OS)"; \
echo "abi=$(ABI)"; \
echo "endianness=$(ENDIANNESS)"; \
echo "system=$(SYSTEM)"; \
......
aarch64/Machregs.v
View file @ ac7b7bd5
......@@ -158,7 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
match ef with
| EF_memcpy sz al => R15 :: R17 :: R29 :: nil
| EF_inline_asm txt sg clob => destroyed_by_clobber clob
| EF_profiling _ _ => R15 :: R17 :: nil
| EF_profiling _ _ => R15 :: R17 :: R29 :: nil
| _ => nil
end.
......
aarch64/TargetPrinter.ml
View file @ ac7b7bd5
......@@ -231,8 +231,8 @@ module Target (*: TARGET*) =
fprintf oc "%s:\n" lbl;
fprintf oc " ldaxr x17, [x15]\n";
fprintf oc " add x17, x17, 1\n";
fprintf oc " stlxr w17, x17, [x15]\n";
fprintf oc " cbnz w17, %s\n" lbl;
fprintf oc " stlxr w29, x17, [x15]\n";
fprintf oc " cbnz w29, %s\n" lbl;
fprintf oc "%s end profiling %a %d\n" comment
Profilingaux.pp_id id kind;;
......
backend/Duplicateaux.ml
View file @ ac7b7bd5
......@@ -24,6 +24,76 @@ open Maps
open Camlcoq
open DebugPrint
let stats_oc = ref None
let set_stats_oc () =
try
let name = Sys.getenv "COMPCERT_PREDICT_STATS" in
let oc = open_out_gen [Open_append; Open_creat; Open_text] 0o666 name in
stats_oc := Some oc
with Not_found -> ()
(* number of total CBs *)
let stats_nb_total = ref 0
(* we predicted the same thing as the profiling *)
let stats_nb_correct_predicts = ref 0
(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false) *)
let stats_nb_mispredicts = ref 0
(* we did not predict anything (None) even though the profiling did predict something *)
let stats_nb_missed_opportunities = ref 0
(* we predicted something (say Some true) but the profiling preferred not to predict anything (None) *)
let stats_nb_overpredict = ref 0
(* heuristic specific counters *)
let wrong_opcode = ref 0
let wrong_return = ref 0
let wrong_loop2 = ref 0
let wrong_loop = ref 0
let wrong_call = ref 0
let right_opcode = ref 0
let right_return = ref 0
let right_loop2 = ref 0
let right_loop = ref 0
let right_call = ref 0
let reset_stats () = begin
stats_nb_total := 0;
stats_nb_correct_predicts := 0;
stats_nb_mispredicts := 0;
stats_nb_missed_opportunities := 0;
stats_nb_overpredict := 0;
wrong_opcode := 0;
wrong_return := 0;
wrong_loop2 := 0;
wrong_loop := 0;
wrong_call := 0;
right_opcode := 0;
right_return := 0;
right_loop2 := 0;
right_loop := 0;
right_call := 0;
end
let incr theref = theref := !theref + 1
let has_some o = match o with Some _ -> true | None -> false
let stats_oc_recording () = has_some !stats_oc
let write_stats_oc () =
match !stats_oc with
| None -> ()
| Some oc -> begin
Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total
!stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities
!stats_nb_overpredict
!wrong_opcode !wrong_return !wrong_loop2 !wrong_loop !wrong_call
!right_opcode !right_return !right_loop2 !right_loop !right_call
;
close_out oc
end
let get_loop_headers = LICMaux.get_loop_headers
let get_some = LICMaux.get_some
let rtl_successors = LICMaux.rtl_successors
......@@ -270,120 +340,66 @@ let get_inner_loops f code is_loop_header =
) (PTree.elements loopmap)
end
let get_loop_bodies code entrypoint =
let predecessors = get_predecessors_rtl code in
(* Algorithm from Muchnik, Compiler Design & Implementation, Figure 7.21 page 192 *)
let natural_loop n m =
debug "Natural Loop from %d to %d\n" (P.to_int n) (P.to_int m);
let in_body = ref (PTree.map (fun n b -> false) code) in
let body = ref [] in
let add_to_body n = begin
in_body := PTree.set n true !in_body;
body := n :: !body
end
in let rec process_node p =
debug " Processing node %d\n" (P.to_int p);
List.iter (fun pred ->
debug " Looking at predecessor of %d: %d\n" (P.to_int p) (P.to_int pred);
let is_in_body = get_some @@ PTree.get pred !in_body in
if (not @@ is_in_body) then begin
debug " --> adding to body\n";
add_to_body pred;
process_node pred
end
) (get_some @@ PTree.get p predecessors)
in begin
add_to_body m;
add_to_body n;
(if (m != n) then process_node m);
!body
end
in let option_natural_loop n = function
| None -> None
| Some m -> Some (natural_loop n m)
in PTree.map option_natural_loop (LICMaux.get_loop_backedges code entrypoint)
(* Returns a PTree of either None or Some b where b determines the node following the loop, for a cb instruction *)
(* It uses the fact that loops in CompCert are done by a branch (backedge) instruction followed by a cb *)
(* Returns a PTree of either None or Some b where b determines the node in the loop body, for a cb instruction *)
let get_loop_info f is_loop_header bfs_order code =
debug "GET LOOP INFO\n";
debug "==================================\n";
let loop_info = ref (PTree.map (fun n i -> None) code) in
let mark_path n lbody =
let cb_info = ref PTree.empty in
let visited = ref (PTree.map (fun n i -> false) code) in
(* Returns true if there is a path from src to dest (not involving jumptables) *)
(* Mark nodes as visited along the way *)
let explore src dest =
debug "Trying to dive a path from %d to %d\n" (P.to_int src) (P.to_int dest);
(* Memoizing the results to avoid exponential blow-up *)
let memory = ref PTree.empty in
let rec explore_rec src =
debug "explore_rec %d vs %d... " (P.to_int src) (P.to_int dest);
if (P.to_int src) == (P.to_int dest) then (debug "FOUND\n"; true)
else if (get_some @@ PTree.get src !visited) then (debug "VISITED... :( \n"; false)
(* if we went out of the innermost loop *)
else if (not @@ List.mem src lbody) then (debug "Out of innermost...\n"; false)
else begin
let inst = get_some @@ PTree.get src code in
visited := PTree.set src true !visited;
match rtl_successors inst with
| [] -> false
| [s] -> explore_wrap s
| [s1; s2] -> let snapshot_visited = ref !visited in begin
debug "\t\tSplit at %d: either %d or %d\n" (P.to_int src) (P.to_int s1) (P.to_int s2);
(* Remembering that we tried the ifso node *)
cb_info := PTree.set src true !cb_info;
match explore_wrap s1 with
| true -> (
visited := !snapshot_visited;
match explore_wrap s2 with
| true -> begin
(* Both paths lead to a loop: we cannot predict the CB
* (but the explore still succeeds) *)
cb_info := PTree.remove src !cb_info;
true
end
| false -> true (* nothing to do, the explore succeeded *)
)
| false -> begin
cb_info := PTree.set src false !cb_info;
match explore_wrap s2 with
| true -> true
| false -> (cb_info := PTree.remove src !cb_info; false)
end
end
| _ -> false
let mark_body body =
List.iter (fun n ->
match get_some @@ PTree.get n code with
| Icond (_, _, ifso, ifnot, _) -> begin
match PTree.get n !loop_info with
| None -> ()
| Some _ ->
let b1 = List.mem ifso body in
let b2 = List.mem ifnot body in
if (b1 && b2) then ()
else if (b1 || b2) then begin
if b1 then loop_info := PTree.set n (Some true) !loop_info
else if b2 then loop_info := PTree.set n (Some false) !loop_info
end
end
and explore_wrap src = begin
match PTree.get src !memory with
| Some b -> b
| None ->
let result = explore_rec src in
(memory := PTree.set src result !memory; result)
end in explore_wrap src
(* Goes forward until a CB is encountered
* Returns None if no CB was found, or Some the_cb_node
* Marks nodes as visited along the way *)
in let rec advance_to_cb src =
if (get_some @@ PTree.get src !visited) then None
else begin
visited := PTree.set src true !visited;
match get_some @@ PTree.get src code with
| Inop s | Iop (_, _, _, s) | Iload (_,_,_,_,_,s) | Istore (_,_,_,_,s) | Icall (_,_,_,_,s)
| Ibuiltin (_,_,_,s) -> advance_to_cb s
| Icond _ -> Some src
| Ijumptable _ | Itailcall _ | Ireturn _ -> None
end
in begin
debug "Attempting to find natural loop from HEAD %d..\n" (P.to_int n);
match advance_to_cb n with
| None -> (debug "\tNo CB found\n")
| Some s -> ( debug "\tFound a CB! %d\n" (P.to_int s);
match get_some @@ PTree.get s !loop_info with
| None | Some _ -> begin
match get_some @@ PTree.get s code with
| Icond (_, _, n1, n2, _) -> (
let b1 = explore n1 n in
let b2 = explore n2 n in
if (b1 && b2) then
debug "\tBoth paths lead back to the head: NONE\n"
else if (b1 || b2) then begin
if b1 then begin
debug "\tTrue path leads to the head: TRUE\n";
loop_info := PTree.set s (Some true) !loop_info;
end else if b2 then begin
debug "\tFalse path leads to the head: FALSE\n";
loop_info := PTree.set s (Some false) !loop_info
end;
debug "\tSetting other CBs encountered..\n";
List.iter (fun (cb, dir) ->
debug "\t\t%d is %B\n" (P.to_int cb) dir;
loop_info := PTree.set cb (Some dir) !loop_info
) (PTree.elements !cb_info)
end else
debug "\tNo path leads back to the head: NONE\n"
)
| _ -> failwith "\tNot an Icond\n"
end
(* | Some _ -> ( debug "already loop info there\n" ) FIXME - we don't know yet whether a branch to a loop head is a backedge or not *)
)
end
in let iloops = get_inner_loops f code is_loop_header in
begin
List.iter (fun il -> mark_path il.head il.body) iloops;
(* List.iter mark_path @@ List.filter (fun n -> get_some @@ PTree.get n is_loop_header) bfs_order; *)
debug "==================================\n";
!loop_info
end
| _ -> ()
) body
in let bodymap = get_loop_bodies code f.fn_entrypoint in
List.iter (fun (_,obody) ->
match obody with
| None -> ()
| Some body -> mark_body body
) (PTree.elements bodymap);
!loop_info
(* Remark - compared to the original Branch Prediction for Free paper, we don't use the store heuristic *)
let get_directions f code entrypoint = begin
......@@ -397,28 +413,59 @@ let get_directions f code entrypoint = begin
(* debug "\n"; *)
List.iter (fun n ->
match (get_some @@ PTree.get n code) with
| Icond (cond, lr, ifso, ifnot, pred) ->
(match pred with Some _ -> debug "RTL node %d already has prediction information\n" (P.to_int n)
| None ->
(* debug "Analyzing %d.." (P.to_int n); *)
let heuristics = [ do_opcode_heuristic;
do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
(* do_store_heuristic *) ] in
let preferred = ref None in
begin
debug "Deciding condition for RTL node %d\n" (P.to_int n);
List.iter (fun do_heur ->
match !preferred with
| None -> preferred := do_heur code cond ifso ifnot is_loop_header
| Some _ -> ()
) heuristics;
directions := PTree.set n !preferred !directions;
(match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
| Some true -> debug "\tBRANCH\n"
| None -> debug "\tUNSURE\n");
debug "---------------------------------------\n"
end
)
| Icond (cond, lr, ifso, ifnot, pred) -> begin
if stats_oc_recording () || not @@ has_some pred then
(* debug "Analyzing %d.." (P.to_int n); *)
let heuristics = [ do_opcode_heuristic;
do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic;
(* do_store_heuristic *) ] in
let preferred = ref None in
let current_heuristic = ref 0 in
begin
debug "Deciding condition for RTL node %d\n" (P.to_int n);
List.iter (fun do_heur ->
match !preferred with
| None -> begin
preferred := do_heur code cond ifso ifnot is_loop_header;
if stats_oc_recording () then begin
(* Getting stats about mispredictions from each heuristic *)
(match !preferred, pred with
| Some false, Some true
| Some true, Some false
(* | Some _, None *) (* Uncomment for overpredicts *)
-> begin
match !current_heuristic with
| 0 -> incr wrong_opcode
| 1 -> incr wrong_return
| 2 -> incr wrong_loop2
| 3 -> incr wrong_loop
| 4 -> incr wrong_call
| _ -> failwith "Shouldn't happen"
end
| Some false, Some false
| Some true, Some true -> begin
match !current_heuristic with
| 0 -> incr right_opcode
| 1 -> incr right_return
| 2 -> incr right_loop2
| 3 -> incr right_loop
| 4 -> incr right_call
| _ -> failwith "Shouldn't happen"
end
| _ -> ()
);
incr current_heuristic
end
end
| Some _ -> ()
) heuristics;
directions := PTree.set n !preferred !directions;
(match !preferred with | Some false -> debug "\tFALLTHROUGH\n"
| Some true -> debug "\tBRANCH\n"
| None -> debug "\tUNSURE\n");
debug "---------------------------------------\n"
end
end
| _ -> ()
) bfs_order;
!directions
......@@ -426,11 +473,28 @@ let get_directions f code entrypoint = begin
end
let update_direction direction = function
| Icond (cond, lr, n, n', pred) ->
| Icond (cond, lr, n, n', pred) -> begin
(* Counting stats from profiling *)
if stats_oc_recording () then begin
incr stats_nb_total;
match pred, direction with
| None, None -> incr stats_nb_correct_predicts
| None, Some _ -> incr stats_nb_overpredict
| Some _, None -> incr stats_nb_missed_opportunities
| Some false, Some false -> incr stats_nb_correct_predicts
| Some false, Some true -> incr stats_nb_mispredicts
| Some true, Some false -> incr stats_nb_mispredicts
| Some true, Some true -> incr stats_nb_correct_predicts
end;
(* only update if there is no prior existing branch prediction *)
(match pred with
| None -> Icond (cond, lr, n, n', direction)
| Some _ -> Icond (cond, lr, n, n', pred) )
| Some _ -> begin
Icond (cond, lr, n, n', pred)
end
)
end
| i -> i
(* Uses branch prediction to write prediction annotations in Icond *)
......@@ -1026,15 +1090,20 @@ let static_predict f =
let entrypoint = f.fn_entrypoint in
let code = f.fn_code in
let revmap = make_identity_ptree code in
let code =
if !Clflags.option_fpredict then
update_directions f code entrypoint
else code in
let code =
if !Clflags.option_fpredict then
invert_iconds code
else code in
((code, entrypoint), revmap)
begin
reset_stats ();
set_stats_oc ();
let code =
if !Clflags.option_fpredict then
update_directions f code entrypoint
else code in
write_stats_oc ();
let code =
if !Clflags.option_fpredict then
invert_iconds code
else code in
((code, entrypoint), revmap)
end
let unroll_single f =
let entrypoint = f.fn_entrypoint in
......
backend/LICMaux.ml
View file @ ac7b7bd5
......@@ -41,24 +41,25 @@ let rtl_successors = function
*
* If we come accross an edge to a Processed node, it's a loop!
*)
let get_loop_headers code entrypoint = begin
debug "get_loop_headers\n";
let get_loop_backedges code entrypoint = begin
debug "get_loop_backedges\n";
let visited = ref (PTree.map (fun n i -> Unvisited) code)
and is_loop_header = ref (PTree.map (fun n i -> false) code)
in let rec dfs_visit code = function
and loop_backedge = ref (PTree.map (fun n i -> None) code)
in let rec dfs_visit code origin = function
| [] -> ()
| node :: ln ->
debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln;
match (get_some @@ PTree.get node !visited) with
| Visited -> begin
debug "\tNode %d is already Visited, skipping\n" (P.to_int node);
dfs_visit code ln
dfs_visit code origin ln
end
| Processed -> begin
debug "Node %d is a loop header\n" (P.to_int node);
is_loop_header := PTree.set node true !is_loop_header;
debug "The backedge is from %d\n" (P.to_int @@ get_some origin);
loop_backedge := PTree.set node origin !loop_backedge;
visited := PTree.set node Visited !visited;
dfs_visit code ln
dfs_visit code origin ln
end
| Unvisited -> begin
visited := PTree.set node Processed !visited;
......@@ -67,19 +68,26 @@ let get_loop_headers code entrypoint = begin
| None -> failwith "No such node"
| Some i -> let next_visits = rtl_successors i in begin
debug "About to visit: %a\n" print_intlist next_visits;
dfs_visit code next_visits
dfs_visit code (Some node) next_visits
end);
debug "Node %d is Visited!\n" (P.to_int node);
visited := PTree.set node Visited !visited;
dfs_visit code ln
dfs_visit code origin ln
end
in begin
dfs_visit code [entrypoint];
debug "LOOP HEADERS: %a\n" print_ptree_bool !is_loop_header;
!is_loop_header
dfs_visit code None [entrypoint];
debug "LOOP BACKEDGES: %a\n" print_ptree_opint !loop_backedge;
!loop_backedge
end
end
let get_loop_headers code entrypoint =
let backedges = get_loop_backedges code entrypoint in
PTree.map (fun _ ob ->
match ob with
| None -> false
| Some _ -> true
) backedges
module Dominator =
struct
......
backend/Linearizeaux.ml
View file @ ac7b7bd5
......@@ -126,400 +126,64 @@ let enumerate_aux_flat f reach =
* This is a slight alteration to the above heuristic, ensuring that any
* superblock will be contiguous in memory, while still following the original
* heuristic
*
* Slight change: instead of taking the minimum pc of the superblock, we just take
* the pc of the first block.
* (experimentally this leads to slightly better performance..)
*)
let get_some = function
| None -> failwith "Did not get some"
| Some thing -> thing
exception EmptyList
let rec last_element = function
| [] -> raise EmptyList
| e :: [] -> e
| e' :: e :: l -> last_element (e::l)
let print_plist l =
let rec f = function
| [] -> ()
| n :: l -> Printf.printf "%d, " (P.to_int n); f l
in begin
if !debug_flag then begin
Printf.printf "[";
f l;
Printf.printf "]"
end
end
(* adapted from the above join_points function, but with PTree *)
let get_join_points code entry =
let reached = ref (PTree.map (fun n i -> false) code) in
let reached_twice = ref (PTree.map (fun n i -> false) code) in
let rec traverse pc =
if get_some @@ PTree.get pc !reached then begin
if not (get_some @@ PTree.get pc !reached_twice) then
reached_twice := PTree.set pc true !reached_twice
end else begin
reached := PTree.set pc true !reached;
traverse_succs (successors_block @@ get_some @@ PTree.get pc code)
end
and traverse_succs = function
| [] -> ()
| [pc] -> traverse pc
| pc :: l -> traverse pc; traverse_succs l
in traverse entry; !reached_twice
let forward_sequences code entry =
let visited = ref (PTree.map (fun n i -> false) code) in
let join_points = get_join_points code entry in
(* returns the list of traversed nodes, and a list of nodes to start traversing next *)
let rec traverse_fallthrough code node =
(* debug "Traversing %d..\n" (P.to_int node); *)
if not (get_some @@ PTree.get node !visited) then begin
visited := PTree.set node true !visited;
match PTree.get node code with
| None -> failwith "No such node"
| Some bb ->
let ln, rem = match (last_element bb) with
| Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
| Lbuiltin _ -> assert false
| Ltailcall _ | Lreturn -> begin (* debug "STOP tailcall/return\n"; *) ([], []) end
| Lbranch n ->
if get_some @@ PTree.get n join_points then ([], [n])
else let ln, rem = traverse_fallthrough code n in (ln, rem)
| Lcond (_, _, ifso, ifnot, info) -> (match info with
| None -> begin (* debug "STOP Lcond None\n"; *) ([], [ifso; ifnot]) end
| Some false ->
if get_some @@ PTree.get ifnot join_points then ([], [ifso; ifnot])
else let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem)
| Some true ->
if get_some @@ PTree.get ifso join_points then ([], [ifso; ifnot])
else let ln, rem = traverse_fallthrough code ifso in (ln, [ifnot] @ rem)
)
| Ljumptable(_, ln) -> begin (* debug "STOP Ljumptable\n"; *) ([], ln) end
in ([node] @ ln, rem)
end
else ([], [])
in let rec f code = function
| [] -> []
| node :: ln ->
let fs, rem_from_node = traverse_fallthrough code node
in [fs] @ ((f code rem_from_node) @ (f code ln))
in (f code [entry])
(** Unused code
module PInt = struct
type t = P.t
let compare x y = compare (P.to_int x) (P.to_int y)
end
module PSet = Set.Make(PInt)
module LPInt = struct
type t = P.t list
let rec compare x y =
match x with
| [] -> ( match y with
| [] -> 0
| _ -> 1 )