Previous  Up  Next

Module Duplicateaux

module Duplicateaux: sig .. end

Oracle for the Duplicate passes

* - Add static prediction information to Icond nodes * - Performs tail duplication on interesting traces to form superblocks * - Unrolls a single iteration of innermost loops * - (TODO: perform partial loop unrolling inside innermost loops)

val stats_oc : Stdlib.out_channel option Stdlib.ref
val set_stats_oc : unit -> unit
val stats_nb_total : int Stdlib.ref
val stats_nb_correct_predicts : int Stdlib.ref
val stats_nb_mispredicts : int Stdlib.ref
val stats_nb_missed_opportunities : int Stdlib.ref
val stats_nb_overpredict : int Stdlib.ref
val wrong_opcode : int Stdlib.ref
val wrong_return : int Stdlib.ref
val wrong_loop2 : int Stdlib.ref
val wrong_call : int Stdlib.ref
val right_opcode : int Stdlib.ref
val right_return : int Stdlib.ref
val right_loop2 : int Stdlib.ref
val right_call : int Stdlib.ref
val reset_stats : unit -> unit
val incr : int Stdlib.ref -> unit
val has_some : 'a option -> bool
val stats_oc_recording : unit -> bool
val write_stats_oc : unit -> unit
val get_loop_headers : RTL.instruction Maps.PTree.tree -> Camlcoq.P.t -> bool Maps.PTree.tree
val rtl_successors : RTL.instruction -> RTL.node list
val bfs_until : RTL.instruction Maps.PTree.tree ->
       RTL.node -> (RTL.node -> bool) -> (RTL.node -> bool) -> RTL.node list
val bfs : RTL.instruction Maps.PTree.tree -> RTL.node -> RTL.node list
val optbool : 'a option -> bool
val ptree_get_some : BinNums.positive -> 'a Maps.PTree.tree -> 'a
val get_predecessors_rtl : RTL.instruction Maps.PTree.t -> BinNums.positive list Maps.PTree.tree
val look_ahead_gen : (RTL.instruction -> Camlcoq.P.t list) ->
       RTL.instruction Maps.PTree.tree ->
       Camlcoq.P.t -> bool Maps.PTree.tree -> (Camlcoq.P.t -> bool) -> bool
val look_ahead : RTL.instruction Maps.PTree.tree ->
       Camlcoq.P.t -> bool Maps.PTree.tree -> (Camlcoq.P.t -> bool) -> bool

* Heuristics mostly based on the paper Branch Prediction for Free

val do_call_heuristic : RTL.instruction Maps.PTree.tree ->
       'a -> Camlcoq.P.t -> Camlcoq.P.t -> bool Maps.PTree.tree -> bool option
val do_opcode_heuristic : 'a -> Op.condition -> 'b -> 'c -> 'd -> bool option
val do_return_heuristic : RTL.instruction Maps.PTree.tree ->
       'a -> Camlcoq.P.t -> Camlcoq.P.t -> bool Maps.PTree.tree -> bool option
val do_store_heuristic : RTL.instruction Maps.PTree.tree ->
       'a -> Camlcoq.P.t -> Camlcoq.P.t -> bool Maps.PTree.tree -> bool option
val do_loop_heuristic : RTL.instruction Maps.PTree.tree ->
       'a -> Camlcoq.P.t -> Camlcoq.P.t -> bool Maps.PTree.tree -> bool option
val do_loop2_heuristic : 'a option Maps.PTree.tree ->
       BinNums.positive -> 'b -> 'c -> 'd -> 'e -> 'f -> 'a option

Innermost loop detection

type innerLoop = {
   preds : RTLcommonaux.OrdPS.t;
   body : RTLcommonaux.OrdPS.t;
   head : Camlcoq.P.t;
   finals : RTLcommonaux.OrdPS.t;
   sb_final : Camlcoq.P.t option;
} 
val print_pset : Stdlib.out_channel -> RTLcommonaux.OrdPS.t -> unit
val rtl_successors_pref : RTL.instruction -> RTL.node list
val find_last_node_before_loop : RTL.instruction Maps.PTree.tree ->
       RTL.node -> RTLcommonaux.OrdPS.t -> bool Maps.PTree.tree -> RTL.node option
val get_inner_loops : RTL.coq_function ->
       RTL.code -> bool Maps.PTree.tree -> innerLoop list
val get_loop_bodies : RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t -> Camlcoq.P.t list option Maps.PTree.tree
val get_loop_info : RTL.coq_function ->
       'a -> 'b -> RTL.instruction Maps.PTree.t -> bool option Maps.PTree.tree
val get_directions : RTL.coq_function ->
       RTL.instruction Maps.PTree.t -> RTL.node -> bool option Maps.PTree.tree
val update_direction : bool option -> RTL.instruction -> RTL.instruction
val update_directions : RTL.coq_function ->
       RTL.instruction Maps.PTree.t -> RTL.node -> RTL.instruction Maps.PTree.t

Trace selection

val exists_false_rec : ('a * bool) list -> bool
val exists_false : bool Maps.PTree.t -> bool
val dfs : RTL.instruction Maps.PTree.tree -> RTL.node -> RTL.node list
val select_unvisited_node : bool Maps.PTree.tree -> BinNums.positive list -> BinNums.positive
val best_successor_of : BinNums.positive ->
       RTL.instruction Maps.PTree.tree -> bool Maps.PTree.tree -> RTL.node option
val best_predecessor_of : BinNums.positive ->
       RTL.node list Maps.PTree.tree ->
       RTL.instruction Maps.PTree.tree ->
       RTL.node list -> bool Maps.PTree.tree -> RTL.node option
val print_trace : Stdlib.out_channel -> Camlcoq.P.t list -> unit
val print_traces : Stdlib.out_channel -> Camlcoq.P.t list list -> unit
val select_traces_linear : RTL.instruction Maps.PTree.tree -> RTL.node -> RTL.node list list
val select_traces_chang : RTL.instruction Maps.PTree.t -> RTL.node -> Camlcoq.P.t list list
val select_traces : RTL.instruction Maps.PTree.t -> RTL.node -> Camlcoq.P.t list list
val make_identity_ptree_rec : (BinNums.positive * 'a) list -> BinNums.positive Maps.PTree.t
val make_identity_ptree : 'a Maps.PTree.t -> BinNums.positive Maps.PTree.t
val change_pointers : RTL.instruction Maps.PTree.tree ->
       RTL.node ->
       RTL.node -> RTLcommonaux.OrdPS.t -> RTL.instruction Maps.PTree.tree
val duplicate : RTL.instruction Maps.PTree.tree ->
       Camlcoq.P.t Maps.PTree.tree ->
       'a ->
       Camlcoq.P.t ->
       RTLcommonaux.OrdPS.t ->
       Camlcoq.P.t -> RTL.instruction Maps.PTree.tree * Camlcoq.P.t Maps.PTree.tree
val maxint : int list -> int
val next_free_pc : 'a Maps.PTree.t -> int
val is_a_nop : RTL.instruction Maps.PTree.tree -> BinNums.positive -> bool
val tail_duplicate : RTL.coq_function ->
       (RTL.instruction Maps.PTree.t * RTL.node) * Camlcoq.P.t Maps.PTree.t
val superblockify_traces : RTL.instruction Maps.PTree.t ->
       RTLcommonaux.OrdPS.elt list Maps.PTree.tree ->
       bool Maps.PTree.tree ->
       Camlcoq.P.t list list ->
       Camlcoq.P.t Maps.PTree.tree ->
       RTL.instruction Maps.PTree.t * Camlcoq.P.t Maps.PTree.tree
val invert_iconds : RTL.instruction Maps.PTree.t -> RTL.instruction Maps.PTree.t

Partial loop unrolling * * The following code seeks innermost loops, and unfolds the first iteration * Most of the code has been moved from LICMaux.ml to Duplicateaux.ml to solve * cyclic dependencies between LICMaux and Duplicateaux

val print_inner_loop : innerLoop -> unit
val print_inner_loops : innerLoop list -> unit
val cb_exit_node : RTL.instruction -> RTL.node option
val generate_fwmap : BinNums.positive list -> 'a list -> 'a Maps.PTree.tree -> 'a Maps.PTree.tree
val generate_revmap : 'a list -> BinNums.positive list -> 'a Maps.PTree.tree -> 'a Maps.PTree.tree
val apply_map : int Maps.PTree.tree -> BinNums.positive -> Camlcoq.P.t
val apply_map_list : int Maps.PTree.tree -> BinNums.positive list -> Camlcoq.P.t list
val apply_map_opt : int Maps.PTree.tree -> Camlcoq.P.t -> Camlcoq.P.t
val change_nexts : int Maps.PTree.tree -> RTL.instruction -> RTL.instruction
val clone : RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t Maps.PTree.tree ->
       Camlcoq.P.t list ->
       RTL.instruction Maps.PTree.t * Camlcoq.P.t Maps.PTree.tree * int list *
       int Maps.PTree.t

Clone a list of instructions into free pc indexes * * The list of instructions should be contiguous, and not include any loop. * It is assumed that the first instruction of the list is the head. * Also, the last instruction of the list should be the loop backedge. * * Returns: (code', revmap', ln', fwmap) * code' is the updated code, after cloning * revmap' is the updated revmap * ln' is the list of the new indexes used to reference the cloned instructions * fwmap is a map from ln to ln'

val count_ignore_nops : RTL.instruction Maps.PTree.tree -> BinNums.positive list -> int
val unroll_inner_loop_single : RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t Maps.PTree.tree ->
       innerLoop ->
       RTL.instruction Maps.PTree.t * Camlcoq.P.t Maps.PTree.tree
val unroll_inner_loops_single : RTL.coq_function ->
       RTL.code ->
       Camlcoq.P.t Maps.PTree.tree -> RTL.code * Camlcoq.P.t Maps.PTree.tree
val is_some : 'a option -> bool
val go_through_predicted : RTL.instruction Maps.PTree.tree ->
       RTL.node -> RTL.node -> RTL.node list option
val unroll_inner_loop_body : RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t Maps.PTree.tree ->
       innerLoop ->
       RTL.instruction Maps.PTree.t * Camlcoq.P.t Maps.PTree.tree
val unroll_inner_loops_body : RTL.coq_function ->
       RTL.code ->
       Camlcoq.P.t Maps.PTree.tree -> RTL.code * Camlcoq.P.t Maps.PTree.tree
val extract_upto_icond : 'a -> RTL.instruction Maps.PTree.tree -> RTL.node -> RTL.node list
val rotate_inner_loop : 'a ->
       RTL.instruction Maps.PTree.t ->
       Camlcoq.P.t Maps.PTree.tree ->
       innerLoop ->
       RTL.instruction Maps.PTree.t * Camlcoq.P.t Maps.PTree.tree
val rotate_inner_loops : RTL.coq_function ->
       RTL.code ->
       Camlcoq.P.t Maps.PTree.tree -> RTL.code * Camlcoq.P.t Maps.PTree.tree
val loop_rotate : RTL.coq_function -> (RTL.code * RTL.node) * Camlcoq.P.t Maps.PTree.t
val static_predict : RTL.coq_function ->
       (RTL.instruction Maps.PTree.t * RTL.node) * BinNums.positive Maps.PTree.t
val unroll_single : RTL.coq_function -> (RTL.code * RTL.node) * Camlcoq.P.t Maps.PTree.t
val unroll_body : RTL.coq_function -> (RTL.code * RTL.node) * Camlcoq.P.t Maps.PTree.t
val tail_duplicate : RTL.coq_function ->
       (RTL.instruction Maps.PTree.t * RTL.node) * Camlcoq.P.t Maps.PTree.t