diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-12-20 17:50:36 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-12-20 17:50:36 +0100 |
commit | 253d955435aa5f71a2772da65f810d7ad532d152 (patch) | |
tree | 3b4686efcabb61692e3707ccfbf20e1822ec027b /mppa_k1c/InstructionScheduler.mli | |
parent | ff1a4a32676fad3a78aad69d963f9f94bb07615c (diff) | |
download | compcert-kvx-253d955435aa5f71a2772da65f810d7ad532d152.tar.gz compcert-kvx-253d955435aa5f71a2772da65f810d7ad532d152.zip |
[BROKEN] Début d'oracle
Diffstat (limited to 'mppa_k1c/InstructionScheduler.mli')
-rw-r--r-- | mppa_k1c/InstructionScheduler.mli | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/mppa_k1c/InstructionScheduler.mli b/mppa_k1c/InstructionScheduler.mli new file mode 100644 index 00000000..507a4cac --- /dev/null +++ b/mppa_k1c/InstructionScheduler.mli @@ -0,0 +1,93 @@ +(** 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 = { + (** An optional maximal total latency of the problem, after which the problem is deemed not schedulable. -1 means there should be no maximum. *) + max_latency : int; + + (** 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. *) + resource_bounds : int array; + + (** At index {i i} the vector of resources used by instruction number {i i}. It must be the same length as [resource_bounds] *) + instruction_usages: int array array; + latency_constraints : latency_constraint list + };; + +(** 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 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;; + +(** 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;; |