module InstructionScheduler:`sig`

..`end`

Schedule instructions on a synchronized pipeline by David Monniaux, CNRS, VERIMAG

`type `

latency_constraint = {

` ` |
`instr_from : ` |

` ` |
`instr_to : ` |

` ` |
`latency : ` |

`}`

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 `

problem = {

` ` |
`max_latency : ` |
`(*` | 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 : ` |
`(*` | 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 : ` |
`(*` | The set of live pseudo-registers at entry. | `*)` |

` ` |
`typing : ` |
`(*` | Register type map. | `*)` |

` ` |
`reference_counting : ` |
`(*` | See BTLScheduleraux.reference_counting. | `*)` |

` ` |
`instruction_usages : ` |
`(*` | At index | `*)` |

` ` |
`latency_constraints : ` |
`(*` | The latency constraints that must be satisfied | `*)` |

`}`

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.

`val print_problem : ``Stdlib.out_channel -> problem -> unit`

Print problem for human readability.

`val get_nr_instructions : ``problem -> int`

Get the number of instructions in a problem

`val get_nr_resources : ``problem -> int`

Get the number of resources in a problem

type`solution =`

`int array`

Scheduling solution. For *n* instructions to schedule, and 0≤*i*<*n*, position *i* contains the time to which instruction *i* should be scheduled. Position *n* contains the final output latency.

type`scheduler =`

`problem -> solution option`

A scheduling algorithm.
The return value `Some x`

is a solution `x`

.
`None`

means that scheduling failed.

`val maximum_slot_used : ``solution -> int`

Get the number the last scheduling time used for an instruction in a solution.

**Returns**The last clock tick used

`val check_schedule : ``problem -> solution -> unit`

Validate that a solution is truly a solution of a scheduling problem.

**Raises**`Failure`

if validation fails

`val list_scheduler : ``problem -> solution option`

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.

**Returns**`Some solution`

when a solution is found,`None`

if not.

`val reg_pres_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_bis : ``problem -> solution option`

`val greedy_scheduler : ``problem -> solution option`

Schedule the problem using the order of instructions without any reordering. DOES NOT COMPUTE A CORRECT MAKESPAN, the "times" are logical not cycles.

`val recompute_makespan : ``problem -> solution -> int option`

`val schedule_reversed : ``scheduler ->`

problem -> int array 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 reverse_list_scheduler : ``problem -> int array option`

Schedule a problem from the end using a list scheduler. BUGGY

`val check_problem : ``problem -> unit`

Check that a problem is well-formed.

**Raises**`Failure`

if validation fails

`val validated_scheduler : ``scheduler ->`

problem -> solution option

Apply a scheduler and validate the result against the input problem.

**Raises**`Failure`

if validation fails**Returns**The solution found

`val get_max_latency : ``solution -> int`

Get max latency from solution

**Returns**Max latency

`val maximum_critical_path : ``problem -> int`

Get the length of a maximal critical path

**Returns**Max length

`val cascaded_scheduler : ``problem -> solution option`

Apply line scheduler then advanced solver

**Returns**A solution if found

`val show_date_ranges : ``problem -> unit`

`type `

pseudo_boolean_problem_type =

`|` |
`SATISFIABILITY` |

`|` |
`OPTIMIZATION` |

`type `

pseudo_boolean_mapper

`val pseudo_boolean_print_problem : ``Stdlib.out_channel ->`

problem ->

pseudo_boolean_problem_type ->

pseudo_boolean_mapper

`val pseudo_boolean_read_solution : ``pseudo_boolean_mapper ->`

Stdlib.in_channel -> solution

`val pseudo_boolean_scheduler : ``pseudo_boolean_problem_type ->`

problem -> solution option

`val smt_print_problem : ``Stdlib.out_channel -> problem -> unit`

`val ilp_print_problem : ``Stdlib.out_channel ->`

problem ->

pseudo_boolean_problem_type ->

pseudo_boolean_mapper

`val ilp_scheduler : ``pseudo_boolean_problem_type ->`

problem -> solution option

`val scheduler_by_name : ``string -> problem -> int array option`

Schedule a problem using a scheduler given by a string name