From 93f9aa39b2885f98bf2be89583102d5c7f4c6f22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Sep 2020 09:13:59 +0200 Subject: just missing OpWeights for AARCH64 --- scheduling/InstructionScheduler.mli | 113 ++++++++++++++++++++++++++++++++++++ 1 file changed, 113 insertions(+) create mode 100644 scheduling/InstructionScheduler.mli (limited to 'scheduling/InstructionScheduler.mli') diff --git a/scheduling/InstructionScheduler.mli b/scheduling/InstructionScheduler.mli new file mode 100644 index 00000000..85e2a5c6 --- /dev/null +++ b/scheduling/InstructionScheduler.mli @@ -0,0 +1,113 @@ +(** Schedule instructions on a synchronized pipeline +by David Monniaux, CNRS, VERIMAG *) + +(** A latency constraint: instruction number [instr_to] should be scheduled at least [latency] clock ticks before [instr_from]. + +It is possible to specify [latency]=0, meaning that [instr_to] can be scheduled at the same clock tick as [instr_from], but not before. + +[instr_to] can be the special value equal to the number of instructions, meaning that it refers to the final output latency. *) +type latency_constraint = { + instr_from : int; + instr_to : int; + latency : int; + } + +(** A scheduling problem. + +In addition to the latency constraints, the resource constraints should be satisfied: at every clock tick, the sum of vectors of resources used by the instructions scheduled at that tick does not exceed the resource bounds. +*) +type problem = { + max_latency : int; + (** An optional maximal total latency of the problem, after which the problem is deemed not schedulable. -1 means there should be no maximum. *) + + resource_bounds : int array; + (** An array of number of units available indexed by the kind of resources to be allocated. It can be empty, in which case the problem is scheduling without resource constraints. *) + + instruction_usages: int array array; + (** At index {i i} the vector of resources used by instruction number {i i}. It must be the same length as [resource_bounds] *) + + latency_constraints : latency_constraint list + (** The latency constraints that must be satisfied *) + };; + +(** Print problem for human readability. *) +val print_problem : out_channel -> problem -> unit;; + +(** Scheduling solution. For {i n} instructions to schedule, and 0≤{i i}<{i n}, position {i i} contains the time to which instruction {i i} should be scheduled. Position {i n} contains the final output latency. *) +type solution = int array + +(** A scheduling algorithm. +The return value [Some x] is a solution [x]. +[None] means that scheduling failed. *) +type scheduler = problem -> solution option;; + +(* DISABLED +(** Schedule the problem optimally by constraint solving using the Gecode solver. *) +external gecode_scheduler : problem -> solution option + = "caml_gecode_schedule_instr" + *) + +(** Get the number the last scheduling time used for an instruction in a solution. +@return The last clock tick used *) +val maximum_slot_used : solution -> int + +(** Validate that a solution is truly a solution of a scheduling problem. +@raise Failure if validation fails *) +val check_schedule : problem -> solution -> unit + +(** Schedule the problem using a greedy list scheduling algorithm, from the start. +The first (according to instruction ordering) instruction that is ready (according to the latency constraints) is scheduled at the current clock tick. +Once a clock tick is full go to the next. + +@return [Some solution] when a solution is found, [None] if not. *) +val list_scheduler : problem -> solution option + +(** Schedule the problem using the order of instructions without any reordering *) +val greedy_scheduler : problem -> solution option + +(** Schedule a problem using a scheduler applied in the opposite direction, e.g. for list scheduling from the end instead of the start. BUGGY *) +val schedule_reversed : scheduler -> problem -> int array option + +(** Schedule a problem from the end using a list scheduler. BUGGY *) +val reverse_list_scheduler : problem -> int array option + +(** Check that a problem is well-formed. +@raise Failure if validation fails *) +val check_problem : problem -> unit + +(** Apply a scheduler and validate the result against the input problem. +@return The solution found +@raise Failure if validation fails *) +val validated_scheduler : scheduler -> problem -> solution option;; + +(** Get max latency from solution +@return Max latency *) +val get_max_latency : solution -> int;; + +(** Get the length of a maximal critical path +@return Max length *) +val maximum_critical_path : problem -> int;; + +(** Apply line scheduler then advanced solver +@return A solution if found *) +val cascaded_scheduler : problem -> solution option;; + +val show_date_ranges : problem -> unit;; + +type pseudo_boolean_problem_type = + | SATISFIABILITY + | OPTIMIZATION;; + +type pseudo_boolean_mapper +val pseudo_boolean_print_problem : out_channel -> problem -> pseudo_boolean_problem_type -> pseudo_boolean_mapper;; +val pseudo_boolean_read_solution : pseudo_boolean_mapper -> in_channel -> solution;; +val pseudo_boolean_scheduler : pseudo_boolean_problem_type -> problem -> solution option;; + +val smt_print_problem : out_channel -> problem -> unit;; + +val ilp_print_problem : out_channel -> problem -> pseudo_boolean_problem_type -> pseudo_boolean_mapper;; + +val ilp_scheduler : pseudo_boolean_problem_type -> problem -> solution option;; + +(** Schedule a problem using a scheduler given by a string name *) +val scheduler_by_name : string -> problem -> int array option;; -- cgit