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 47eaaa23 authored by Cyril SIX's avatar Cyril SIX
Browse files

Recording of prediction stats with COMPCERT_PROFILING_STATS environment flag

It only works correctly if both profiling and static prediction are
used: it then compares both and gives stats in COMPCERT_PREDICT_STATS
file.

The stats are of the form:
  total correct mispredicts missed

total = number of total CBs encountered
correct = number of correct predictions
mispredicts = times when static prediction did a wrong guess (predicted
    the opposite from profiling, or predicted Some _ when profiling said
    None)
missed = times when static prediction was not able to give a verdict,
       though the profiling gave one
parent d53cc13b
......@@ -24,6 +24,45 @@ 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, or None) *)
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
let reset_stats () = begin
stats_nb_total := 0;
stats_nb_correct_predicts := 0;
stats_nb_mispredicts := 0;
stats_nb_missed_opportunities := 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\n" !stats_nb_total !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities;
close_out oc
end
let get_loop_headers = LICMaux.get_loop_headers
let get_some = LICMaux.get_some
let rtl_successors = LICMaux.rtl_successors
......@@ -397,28 +436,27 @@ 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
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
end
| _ -> ()
) bfs_order;
!directions
......@@ -426,11 +464,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_mispredicts
| 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 +1081,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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment