1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(** 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. *)
live_regs_entry : Registers.Regset.t;
(** The set of live pseudo-registers at entry. *)
typing : RTLtyping.regenv;
(** Register type map. *)
reference_counting : ((Registers.reg, int * int) Hashtbl.t
* ((Registers.reg * bool) list array)) option;
(** See BTLScheduleraux.reference_counting. *)
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;;
(** Get the number of instructions in a problem *)
val get_nr_instructions : problem -> int;;
(** Get the number of resources in a problem *)
val get_nr_resources : problem -> int;;
(** 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
(** WIP : Same as list_scheduler, but schedules instructions which decrease
register pressure when it gets too high. *)
val reg_pres_scheduler : problem -> solution option
val reg_pres_scheduler_bis : 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;;
|
