diff options
Diffstat (limited to 'kvx/InstructionScheduler.ml')
| -rw-r--r-- | kvx/InstructionScheduler.ml | 1263 |
1 files changed, 0 insertions, 1263 deletions
diff --git a/kvx/InstructionScheduler.ml b/kvx/InstructionScheduler.ml deleted file mode 100644 index eab0b21a..00000000 --- a/kvx/InstructionScheduler.ml +++ /dev/null @@ -1,1263 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -let with_destructor dtor stuff f = - try let ret = f stuff in - dtor stuff; - ret - with exn -> dtor stuff; - raise exn;; - -let with_out_channel chan f = with_destructor close_out chan f;; -let with_in_channel chan f = with_destructor close_in chan f;; - -(** Schedule instructions on a synchronized pipeline -@author David Monniaux, CNRS, VERIMAG *) - -type latency_constraint = { - instr_from : int; - instr_to : int; - latency : int };; - -type problem = { - max_latency : int; - resource_bounds : int array; - instruction_usages : int array array; - latency_constraints : latency_constraint list; - };; - -let print_problem channel problem = - (if problem.max_latency >= 0 - then Printf.fprintf channel "max makespan: %d\n" problem.max_latency); - output_string channel "resource bounds:"; - (Array.iter (fun b -> Printf.fprintf channel " %d" b) problem.resource_bounds); - output_string channel ";\n"; - (Array.iteri (fun i v -> - Printf.fprintf channel "instr%d:" i; - (Array.iter (fun b -> Printf.fprintf channel " %d" b) v); - output_string channel ";\n") problem.instruction_usages); - List.iter (fun instr -> - Printf.printf "t%d - t%d >= %d;\n" - instr.instr_to instr.instr_from instr.latency) - problem.latency_constraints;; - -let get_nr_instructions problem = Array.length problem.instruction_usages;; -let get_nr_resources problem = Array.length problem.resource_bounds;; - -type solution = int array -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";; - *) - -let maximum_slot_used times = - let maxi = ref (-1) in - for i=0 to (Array.length times)-2 - do - maxi := max !maxi times.(i) - done; - !maxi;; - -let check_schedule (problem : problem) (times : solution) = - let nr_instructions = get_nr_instructions problem in - (if Array.length times <> nr_instructions+1 - then failwith - (Printf.sprintf "check_schedule: %d times expected, got %d" - (nr_instructions+1) (Array.length times))); - (if problem.max_latency >= 0 && times.(nr_instructions)> problem.max_latency - then failwith "check_schedule: max_latency exceeded"); - (Array.iteri (fun i time -> - (if time < 0 - then failwith (Printf.sprintf "time[%d] < 0" i))) times); - let slot_resources = Array.init ((maximum_slot_used times)+1) - (fun _ -> Array.copy problem.resource_bounds) in - for i=0 to nr_instructions -1 - do - let remaining_resources = slot_resources.(times.(i)) - and used_resources = problem.instruction_usages.(i) in - for resource=0 to (Array.length used_resources)-1 - do - let after = remaining_resources.(resource) - used_resources.(resource) in - (if after < 0 - then failwith (Printf.sprintf "check_schedule: instruction %d exceeds resource %d at slot %d" i resource times.(i))); - remaining_resources.(resource) <- after - done - done; - List.iter (fun ctr -> - if times.(ctr.instr_to) - times.(ctr.instr_from) < ctr.latency - then failwith (Printf.sprintf "check_schedule: time[%d]=%d - time[%d]=%d < %d" - ctr.instr_to times.(ctr.instr_to) - ctr.instr_from times.(ctr.instr_from) - ctr.latency) - ) problem.latency_constraints;; - -let bound_max_time problem = - let total = ref(Array.length problem.instruction_usages) in - List.iter (fun ctr -> total := !total + ctr.latency) problem.latency_constraints; - !total;; - -let vector_less_equal a b = - try - Array.iter2 (fun x y -> - if x>y - then raise Exit) a b; - true - with Exit -> false;; - -let vector_subtract a b = - assert ((Array.length a) = (Array.length b)); - for i=0 to (Array.length a)-1 - do - b.(i) <- b.(i) - a.(i) - done;; - -(* The version with critical path ordering is much better! *) -type list_scheduler_order = - | INSTRUCTION_ORDER - | CRITICAL_PATH_ORDER;; - -let int_max (x : int) (y : int) = - if x > y then x else y;; - -let int_min (x : int) (y : int) = - if x < y then x else y;; - -let get_predecessors problem = - let nr_instructions = get_nr_instructions problem in - let predecessors = Array.make (nr_instructions+1) [] in - List.iter (fun ctr -> - predecessors.(ctr.instr_to) <- - (ctr.instr_from, ctr.latency)::predecessors.(ctr.instr_to)) - problem.latency_constraints; - predecessors;; - -let get_successors problem = - let nr_instructions = get_nr_instructions problem in - let successors = Array.make nr_instructions [] in - List.iter (fun ctr -> - successors.(ctr.instr_from) <- - (ctr.instr_to, ctr.latency)::successors.(ctr.instr_from)) - problem.latency_constraints; - successors;; - -let critical_paths successors = - let nr_instructions = Array.length successors in - let path_lengths = Array.make nr_instructions (-1) in - let rec compute i = - if i=nr_instructions then 0 else - match path_lengths.(i) with - | -2 -> failwith "InstructionScheduler: the dependency graph has cycles" - | -1 -> path_lengths.(i) <- -2; - let x = List.fold_left - (fun cur (j, latency)-> int_max cur (latency+(compute j))) - 1 successors.(i) - in path_lengths.(i) <- x; x - | x -> x - in for i = nr_instructions-1 downto 0 - do - ignore (compute i) - done; - path_lengths;; - -let maximum_critical_path problem = - let paths = critical_paths (get_successors problem) in - Array.fold_left int_max 0 paths;; - -let get_earliest_dates predecessors = - let nr_instructions = (Array.length predecessors)-1 in - let path_lengths = Array.make (nr_instructions+1) (-1) in - let rec compute i = - match path_lengths.(i) with - | -2 -> failwith "InstructionScheduler: the dependency graph has cycles" - | -1 -> path_lengths.(i) <- -2; - let x = List.fold_left - (fun cur (j, latency)-> int_max cur (latency+(compute j))) - 0 predecessors.(i) - in path_lengths.(i) <- x; x - | x -> x - in for i = 0 to nr_instructions - do - ignore (compute i) - done; - for i = 0 to nr_instructions - 1 - do - path_lengths.(nr_instructions) <- int_max - path_lengths.(nr_instructions) (1 + path_lengths.(i)) - done; - path_lengths;; - -exception Unschedulable - -let get_latest_dates deadline successors = - let nr_instructions = Array.length successors - and path_lengths = critical_paths successors in - Array.init (nr_instructions + 1) - (fun i -> - if i < nr_instructions then - let path_length = path_lengths.(i) in - assert (path_length >= 1); - (if path_length > deadline - then raise Unschedulable); - deadline - path_length - else deadline);; - -let priority_list_scheduler (order : list_scheduler_order) - (problem : problem) : - solution option = - let nr_instructions = get_nr_instructions problem in - let successors = get_successors problem - and predecessors = get_predecessors problem - and times = Array.make (nr_instructions+1) (-1) in - - let priorities = match order with - | INSTRUCTION_ORDER -> None - | CRITICAL_PATH_ORDER -> Some (critical_paths successors) in - - let module InstrSet = - Set.Make (struct type t=int - let compare = match priorities with - | None -> (fun x y -> x - y) - | Some p -> (fun x y -> - (match p.(y)-p.(x) with - | 0 -> x - y - | z -> z)) - end) in - - let max_time = bound_max_time problem in - let ready = Array.make max_time InstrSet.empty in - Array.iteri (fun i preds -> - if i<nr_instructions && preds=[] - then ready.(0) <- InstrSet.add i ready.(0)) predecessors; - - let current_time = ref 0 - and current_resources = Array.copy problem.resource_bounds - and earliest_time i = - try - let time = ref (-1) in - List.iter (fun (j, latency) -> - if times.(j) < 0 - then raise Exit - else let t = times.(j) + latency in - if t > !time - then time := t) predecessors.(i); - assert(!time >= 0); - !time - with Exit -> -1 - - in - let advance_time() = - begin - (if !current_time < max_time-1 - then - begin - Array.blit problem.resource_bounds 0 current_resources 0 - (Array.length current_resources); - ready.(!current_time + 1) <- - InstrSet.union (ready.(!current_time)) (ready.(!current_time + 1)); - ready.(!current_time) <- InstrSet.empty; - end); - incr current_time - end in - - let attempt_scheduling ready usages = - let result = ref (-1) in - try - InstrSet.iter (fun i -> - (* Printf.printf "trying scheduling %d\n" i; - pr int_vector usages.(i); - print _vector current_resources; *) - if vector_less_equal usages.(i) current_resources - then - begin - vector_subtract usages.(i) current_resources; - result := i; - raise Exit - end) ready; - -1 - with Exit -> !result in - - while !current_time < max_time - do - if (InstrSet.is_empty ready.(!current_time)) - then advance_time() - else - match attempt_scheduling ready.(!current_time) - problem.instruction_usages with - | -1 -> advance_time() - | i -> - begin - assert(times.(i) < 0); - times.(i) <- !current_time; - ready.(!current_time) <- InstrSet.remove i (ready.(!current_time)); - List.iter (fun (instr_to, latency) -> - if instr_to < nr_instructions then - match earliest_time instr_to with - | -1 -> () - | to_time -> - ready.(to_time) <- InstrSet.add instr_to ready.(to_time)) - successors.(i); - successors.(i) <- [] - end - done; - try - let final_time = ref (-1) in - for i=0 to nr_instructions-1 - do - (if times.(i) < 0 then raise Exit); - (if !final_time < times.(i)+1 then final_time := times.(i)+1) - done; - List.iter (fun (i, latency) -> - let target_time = latency + times.(i) in - if target_time > !final_time - then final_time := target_time - ) predecessors.(nr_instructions); - times.(nr_instructions) <- !final_time; - Some times - with Exit -> None;; - -let list_scheduler = priority_list_scheduler CRITICAL_PATH_ORDER;; - -(* dummy code for placating ocaml's warnings *) -let _ = fun x -> priority_list_scheduler INSTRUCTION_ORDER x;; - -type bundle = int list;; - -let rec extract_deps_to index = function - | [] -> [] - | dep :: deps -> let extracts = extract_deps_to index deps in - if (dep.instr_to == index) then - dep :: extracts - else - extracts - -exception InvalidBundle;; - -let dependency_check problem bundle index = - let index_deps = extract_deps_to index problem.latency_constraints in - List.iter (fun i -> - List.iter (fun dep -> - if (dep.instr_from == i) then raise InvalidBundle - ) index_deps - ) bundle;; - -let rec make_bundle problem resources bundle index = - let resources_copy = Array.copy resources in - let nr_instructions = get_nr_instructions problem in - if (index >= nr_instructions) then (bundle, index+1) else - let inst_usage = problem.instruction_usages.(index) in - try match vector_less_equal inst_usage resources with - | false -> raise InvalidBundle - | true -> ( - dependency_check problem bundle index; - vector_subtract problem.instruction_usages.(index) resources_copy; - make_bundle problem resources_copy (index::bundle) (index+1) - ) - with InvalidBundle -> (bundle, index);; - -let rec make_bundles problem index : bundle list = - if index >= get_nr_instructions problem then - [] - else - let (bundle, new_index) = make_bundle problem problem.resource_bounds [] index in - bundle :: (make_bundles problem new_index);; - -let bundles_to_schedule problem bundles : solution = - let nr_instructions = get_nr_instructions problem in - let schedule = Array.make (nr_instructions+1) (nr_instructions+4) in - let time = ref 0 in - List.iter (fun bundle -> - begin - List.iter (fun i -> - schedule.(i) <- !time - ) bundle; - time := !time + 1 - end - ) bundles; schedule;; - -let greedy_scheduler (problem : problem) : solution option = - let bundles = make_bundles problem 0 in - Some (bundles_to_schedule problem bundles);; - -(* alternate implementation -let swap_array_elements a i j = - let x = a.(i) in - a.(i) <- a.(j); - a.(j) <- x;; - -let array_reverse_slice a first last = - let i = ref first and j = ref last in - while i < j - do - swap_array_elements a !i !j; - incr i; - decr j - done;; - -let array_reverse a = - let a' = Array.copy a in - array_reverse_slice a' 0 ((Array.length a)-1); - a';; - *) - -(* unneeded -let array_reverse a = - let n=Array.length a in - Array.init n (fun i -> a.(n-1-i));; - *) - -let reverse_constraint nr_instructions ctr = - { instr_to = nr_instructions -ctr.instr_from; - instr_from = nr_instructions - ctr.instr_to; - latency = ctr.latency };; - -(* unneeded -let rec list_map_filter f = function - | [] -> [] - | h::t -> - (match f h with - | None -> list_map_filter f t - | Some x -> x :: (list_map_filter f t));; - *) - -let reverse_problem problem = - let nr_instructions = get_nr_instructions problem in - { - max_latency = problem.max_latency; - resource_bounds = problem.resource_bounds; - instruction_usages = Array.init (nr_instructions + 1) - (fun i -> - if i=0 - then Array.map (fun _ -> 0) problem.resource_bounds else problem.instruction_usages.(nr_instructions - i)); - latency_constraints = List.map (reverse_constraint nr_instructions) - problem.latency_constraints - };; - -let max_scheduled_time solution = - let time = ref (-1) in - for i = 0 to ((Array.length solution) - 2) - do - time := max !time solution.(i) - done; - !time;; - -(* -let recompute_makespan problem solution = - let n = (Array.length solution) - 1 and ms = ref 0 in - List.iter (fun cstr -> - if cstr.instr_to = n - then ms := max !ms (solution.(cstr.instr_from) + cstr.latency) - ) problem.latency_constraints; - !ms;; - *) - -let schedule_reversed (scheduler : problem -> solution option) - (problem : problem) = - match scheduler (reverse_problem problem) with - | None -> None - | Some solution -> - let nr_instructions = get_nr_instructions problem in - let makespan = max_scheduled_time solution in - let ret = Array.init (nr_instructions + 1) - (fun i -> makespan-solution.(nr_instructions-i)) in - ret.(nr_instructions) <- max ((max_scheduled_time ret) + 1) - (ret.(nr_instructions)); - Some ret;; - -(** Schedule the problem using a greedy list scheduling algorithm, from the end. *) -let reverse_list_scheduler = schedule_reversed list_scheduler;; - -let check_problem problem = - (if (Array.length problem.instruction_usages) < 1 - then failwith "length(problem.instruction_usages) < 1");; - -let validated_scheduler (scheduler : problem -> solution option) - (problem : problem) = - check_problem problem; - match scheduler problem with - | None -> None - | (Some solution) as ret -> check_schedule problem solution; ret;; - -let get_max_latency solution = - solution.((Array.length solution)-1);; - -let show_date_ranges problem = - let deadline = problem.max_latency in - assert(deadline >= 0); - let successors = get_successors problem - and predecessors = get_predecessors problem in - let earliest_dates : int array = get_earliest_dates predecessors - and latest_dates : int array = get_latest_dates deadline successors in - assert ((Array.length earliest_dates) = - (Array.length latest_dates)); - Array.iteri (fun i early -> - let late = latest_dates.(i) in - Printf.printf "t[%d] in %d..%d\n" i early late) - earliest_dates;; - -type pseudo_boolean_problem_type = - | SATISFIABILITY - | OPTIMIZATION;; - -type pseudo_boolean_mapper = { - mapper_pb_type : pseudo_boolean_problem_type; - mapper_nr_instructions : int; - mapper_nr_pb_variables : int; - mapper_earliest_dates : int array; - mapper_latest_dates : int array; - mapper_var_offsets : int array; - mapper_final_predecessors : (int * int) list -};; - -(* Latency constraints are: - presence of instr-to at each t <= sum of presences of instr-from at compatible times - - if reverse_encoding - presence of instr-from at each t <= sum of presences of instr-to at compatible times *) - -(* Experiments show reverse_encoding=true multiplies time by 2 in sat4j - without making hard instances easier *) -let direct_encoding = false -and reverse_encoding = false -and delta_encoding = true - -let pseudo_boolean_print_problem channel problem pb_type = - let deadline = problem.max_latency in - assert (deadline > 0); - let nr_instructions = get_nr_instructions problem - and nr_resources = get_nr_resources problem - and successors = get_successors problem - and predecessors = get_predecessors problem in - let earliest_dates = get_earliest_dates predecessors - and latest_dates = get_latest_dates deadline successors in - let var_offsets = Array.make - (match pb_type with - | OPTIMIZATION -> nr_instructions+1 - | SATISFIABILITY -> nr_instructions) 0 in - let nr_pb_variables = - (let nr = ref 0 in - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - var_offsets.(i) <- !nr; - nr := !nr + latest_dates.(i) - earliest_dates.(i) + 1 - done; - !nr) - and nr_pb_constraints = - (match pb_type with - | OPTIMIZATION -> nr_instructions+1 - | SATISFIABILITY -> nr_instructions) + - - (let count = ref 0 in - for t=0 to deadline-1 - do - for j=0 to nr_resources-1 - do - try - for i=0 to nr_instructions-1 - do - let usage = problem.instruction_usages.(i).(j) in - if t >= earliest_dates.(i) && t <= latest_dates.(i) - && usage > 0 then raise Exit - done - with Exit -> incr count - done - done; - !count) + - - (let count=ref 0 in - List.iter - (fun ctr -> - if ctr.instr_to < nr_instructions - then count := !count + 1 + latest_dates.(ctr.instr_to) - - earliest_dates.(ctr.instr_to) - + (if reverse_encoding - then 1 + latest_dates.(ctr.instr_from) - - earliest_dates.(ctr.instr_from) - else 0) - ) - problem.latency_constraints; - !count) + - - (match pb_type with - | OPTIMIZATION -> (1 + deadline - earliest_dates.(nr_instructions)) * nr_instructions - | SATISFIABILITY -> 0) - and measured_nr_constraints = ref 0 in - - let pb_var i t = - assert(t >= earliest_dates.(i)); - assert(t <= latest_dates.(i)); - let v = 1+var_offsets.(i)+t-earliest_dates.(i) in - assert(v <= nr_pb_variables); - Printf.sprintf "x%d" v in - - let end_constraint () = - begin - output_string channel ";\n"; - incr measured_nr_constraints - end in - - let gen_latency_constraint i_to i_from latency t_to = - Printf.fprintf channel "* t[%d] - t[%d] >= %d when t[%d]=%d\n" - i_to i_from latency i_to t_to; - for t_from=earliest_dates.(i_from) to - int_min latest_dates.(i_from) (t_to - latency) - do - Printf.fprintf channel "+1 %s " (pb_var i_from t_from) - done; - Printf.fprintf channel "-1 %s " (pb_var i_to t_to); - Printf.fprintf channel ">= 0"; - end_constraint() - - and gen_dual_latency_constraint i_to i_from latency t_from = - Printf.fprintf channel "* t[%d] - t[%d] >= %d when t[%d]=%d\n" - i_to i_from latency i_to t_from; - for t_to=int_max earliest_dates.(i_to) (t_from + latency) - to latest_dates.(i_to) - do - Printf.fprintf channel "+1 %s " (pb_var i_to t_to) - done; - Printf.fprintf channel "-1 %s " (pb_var i_from t_from); - Printf.fprintf channel ">= 0"; - end_constraint() - in - - Printf.fprintf channel "* #variable= %d #constraint= %d\n" nr_pb_variables nr_pb_constraints; - Printf.fprintf channel "* nr_instructions=%d deadline=%d\n" nr_instructions deadline; - begin - match pb_type with - | SATISFIABILITY -> () - | OPTIMIZATION -> - output_string channel "min:"; - for t=earliest_dates.(nr_instructions) to deadline - do - Printf.fprintf channel " %+d %s" t (pb_var nr_instructions t) - done; - output_string channel ";\n"; - end; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - let early = earliest_dates.(i) and late= latest_dates.(i) in - Printf.fprintf channel "* t[%d] in %d..%d\n" i early late; - for t=early to late - do - Printf.fprintf channel "+1 %s " (pb_var i t) - done; - Printf.fprintf channel "= 1"; - end_constraint() - done; - - for t=0 to deadline-1 - do - for j=0 to nr_resources-1 - do - let bound = problem.resource_bounds.(j) - and coeffs = ref [] in - for i=0 to nr_instructions-1 - do - let usage = problem.instruction_usages.(i).(j) in - if t >= earliest_dates.(i) && t <= latest_dates.(i) - && usage > 0 - then coeffs := (i, usage) :: !coeffs - done; - if !coeffs <> [] then - begin - Printf.fprintf channel "* resource #%d at t=%d <= %d\n" j t bound; - List.iter (fun (i, usage) -> - Printf.fprintf channel "%+d %s " (-usage) (pb_var i t)) !coeffs; - Printf.fprintf channel ">= %d" (-bound); - end_constraint(); - end - done - done; - - List.iter - (fun ctr -> - if ctr.instr_to < nr_instructions then - begin - for t_to=earliest_dates.(ctr.instr_to) to latest_dates.(ctr.instr_to) - do - gen_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_to - done; - if reverse_encoding - then - for t_from=earliest_dates.(ctr.instr_from) to latest_dates.(ctr.instr_from) - do - gen_dual_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_from - done - end - ) problem.latency_constraints; - - begin - match pb_type with - | SATISFIABILITY -> () - | OPTIMIZATION -> - let final_latencies = Array.make nr_instructions 1 in - List.iter (fun (i, latency) -> - final_latencies.(i) <- int_max final_latencies.(i) latency) - predecessors.(nr_instructions); - for t_to=earliest_dates.(nr_instructions) to deadline - do - for i_from = 0 to nr_instructions -1 - do - gen_latency_constraint nr_instructions i_from final_latencies.(i_from) t_to - done - done - end; - assert (!measured_nr_constraints = nr_pb_constraints); - { - mapper_pb_type = pb_type; - mapper_nr_instructions = nr_instructions; - mapper_nr_pb_variables = nr_pb_variables; - mapper_earliest_dates = earliest_dates; - mapper_latest_dates = latest_dates; - mapper_var_offsets = var_offsets; - mapper_final_predecessors = predecessors.(nr_instructions) - };; - -type pb_answer = - | Positive - | Negative - | Unknown - -let line_to_pb_solution sol line nr_pb_variables = - let assign s v = - begin - let i = int_of_string s in - sol.(i-1) <- v - end in - List.iter - begin - function "" -> () - | item -> - (match String.get item 0 with - | '+' -> - assert ((String.length item) >= 3); - assert ((String.get item 1) = 'x'); - assign (String.sub item 2 ((String.length item)-2)) Positive - | '-' -> - assert ((String.length item) >= 3); - assert ((String.get item 1) = 'x'); - assign (String.sub item 2 ((String.length item)-2)) Negative - | 'x' -> - assert ((String.length item) >= 2); - assign (String.sub item 1 ((String.length item)-1)) Positive - | _ -> failwith "syntax error in pseudo Boolean solution: epected + - or x" - ) - end - (String.split_on_char ' ' (String.sub line 2 ((String.length line)-2)));; - -let pb_solution_to_schedule mapper pb_solution = - Array.mapi (fun i offset -> - let first = mapper.mapper_earliest_dates.(i) - and last = mapper.mapper_latest_dates.(i) - and time = ref (-1) in - for t=first to last - do - match pb_solution.(t - first + offset) with - | Positive -> - (if !time = -1 - then time:=t - else failwith "duplicate time in pseudo boolean solution") - | Negative -> () - | Unknown -> failwith "unknown value in pseudo boolean solution" - done; - (if !time = -1 - then failwith "no time in pseudo boolean solution"); - !time - ) mapper.mapper_var_offsets;; - -let pseudo_boolean_read_solution mapper channel = - let optimum = ref (-1) - and optimum_found = ref false - and solution = Array.make mapper.mapper_nr_pb_variables Unknown in - try - while true do - match input_line channel with - | "" -> () - | line -> - begin - match String.get line 0 with - | 'c' -> () - | 'o' -> - assert ((String.length line) >= 2); - assert ((String.get line 1) = ' '); - optimum := int_of_string (String.sub line 2 ((String.length line)-2)) - | 's' -> (match line with - | "s OPTIMUM FOUND" -> optimum_found := true - | "s SATISFIABLE" -> () - | "s UNSATISFIABLE" -> close_in channel; - raise Unschedulable - | _ -> failwith line) - | 'v' -> line_to_pb_solution solution line mapper.mapper_nr_pb_variables - | x -> Printf.printf "unknown: %s\n" line - end - done; - assert false - with End_of_file -> - close_in channel; - begin - let sol = pb_solution_to_schedule mapper solution in - sol - end;; - -let recompute_max_latency mapper solution = - let maxi = ref (-1) in - for i=0 to (mapper.mapper_nr_instructions-1) - do - maxi := int_max !maxi (1+solution.(i)) - done; - List.iter (fun (i, latency) -> - maxi := int_max !maxi (solution.(i) + latency)) mapper.mapper_final_predecessors; - !maxi;; - -let adjust_check_solution mapper solution = - match mapper.mapper_pb_type with - | OPTIMIZATION -> - let max_latency = recompute_max_latency mapper solution in - assert (max_latency = solution.(mapper.mapper_nr_instructions)); - solution - | SATISFIABILITY -> - let max_latency = recompute_max_latency mapper solution in - Array.init (mapper.mapper_nr_instructions+1) - (fun i -> if i < mapper.mapper_nr_instructions - then solution.(i) - else max_latency);; - -(* let pseudo_boolean_solver = ref "/local/monniaux/progs/naps/naps" *) -(* let pseudo_boolean_solver = ref "/local/monniaux/packages/sat4j/org.sat4j.pb.jar CuttingPlanes" *) - -(* let pseudo_boolean_solver = ref "java -jar /usr/share/java/org.sat4j.pb.jar CuttingPlanes" *) -(* let pseudo_boolean_solver = ref "java -jar /usr/share/java/org.sat4j.pb.jar" *) -(* let pseudo_boolean_solver = ref "clasp" *) -(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/open-wbo/open-wbo_static -formula=1" *) -(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/naps/naps" *) -(* let pseudo_boolean_solver = ref "/home/monniaux/progs/CP/minisatp/build/release/bin/minisatp" *) -(* let pseudo_boolean_solver = ref "java -jar sat4j-pb.jar CuttingPlanesStar" *) -let pseudo_boolean_solver = ref "pb_solver" - -let pseudo_boolean_scheduler pb_type problem = - try - let filename_in = "problem.opb" in - (* needed only if not using stdout and filename_out = "problem.sol" *) - let mapper = - with_out_channel (open_out filename_in) - (fun opb_problem -> - pseudo_boolean_print_problem opb_problem problem pb_type) in - Some (with_in_channel - (Unix.open_process_in (!pseudo_boolean_solver ^ " " ^ filename_in)) - (fun opb_solution -> adjust_check_solution mapper (pseudo_boolean_read_solution mapper opb_solution))) - with - | Unschedulable -> None;; - -let rec reoptimizing_scheduler (scheduler : scheduler) (previous_solution : solution) (problem : problem) = - if (get_max_latency previous_solution)>1 then - begin - Printf.printf "reoptimizing < %d\n" (get_max_latency previous_solution); - flush stdout; - match scheduler - { problem with max_latency = (get_max_latency previous_solution)-1 } - with - | None -> previous_solution - | Some solution -> reoptimizing_scheduler scheduler solution problem - end - else previous_solution;; - -let smt_var i = Printf.sprintf "t%d" i - -let is_resource_used problem j = - try - Array.iter (fun usages -> - if usages.(j) > 0 - then raise Exit) problem.instruction_usages; - false - with Exit -> true;; - -let smt_use_quantifiers = false - -let smt_print_problem channel problem = - let nr_instructions = get_nr_instructions problem in - let gen_smt_resource_constraint time j = - output_string channel "(<= (+"; - Array.iteri - (fun i usages -> - let usage=usages.(j) in - if usage > 0 - then Printf.fprintf channel " (ite (= %s %s) %d 0)" - time (smt_var i) usage) - problem.instruction_usages; - Printf.fprintf channel ") %d)" problem.resource_bounds.(j) - in - output_string channel "(set-option :produce-models true)\n"; - for i=0 to nr_instructions - do - Printf.fprintf channel "(declare-const %s Int)\n" (smt_var i); - Printf.fprintf channel "(assert (>= %s 0))\n" (smt_var i) - done; - for i=0 to nr_instructions-1 - do - Printf.fprintf channel "(assert (< %s %s))\n" - (smt_var i) (smt_var nr_instructions) - done; - (if problem.max_latency > 0 - then Printf.fprintf channel "(assert (<= %s %d))\n" - (smt_var nr_instructions) problem.max_latency); - List.iter (fun ctr -> - Printf.fprintf channel "(assert (>= (- %s %s) %d))\n" - (smt_var ctr.instr_to) - (smt_var ctr.instr_from) - ctr.latency) problem.latency_constraints; - for j=0 to (Array.length problem.resource_bounds)-1 - do - if is_resource_used problem j - then - begin - if smt_use_quantifiers - then - begin - Printf.fprintf channel - "; resource #%d <= %d\n(assert (forall ((t Int)) " - j problem.resource_bounds.(j); - gen_smt_resource_constraint "t" j; - output_string channel "))\n" - end - else - begin - (if problem.max_latency < 0 - then failwith "quantifier explosion needs max latency"); - for t=0 to problem.max_latency - do - Printf.fprintf channel - "; resource #%d <= %d at t=%d\n(assert " - j problem.resource_bounds.(j) t; - gen_smt_resource_constraint (string_of_int t) j; - output_string channel ")\n" - done - end - end - done; - output_string channel "(check-sat)(get-model)\n";; - - -let ilp_print_problem channel problem pb_type = - let deadline = problem.max_latency in - assert (deadline > 0); - let nr_instructions = get_nr_instructions problem - and nr_resources = get_nr_resources problem - and successors = get_successors problem - and predecessors = get_predecessors problem in - let earliest_dates = get_earliest_dates predecessors - and latest_dates = get_latest_dates deadline successors in - - let pb_var i t = - Printf.sprintf "x%d_%d" i t in - - let gen_latency_constraint i_to i_from latency t_to = - Printf.fprintf channel "\\ t[%d] - t[%d] >= %d when t[%d]=%d\n" - i_to i_from latency i_to t_to; - Printf.fprintf channel "c_%d_%d_%d_%d: " - i_to i_from latency t_to; - for t_from=earliest_dates.(i_from) to - int_min latest_dates.(i_from) (t_to - latency) - do - Printf.fprintf channel "+1 %s " (pb_var i_from t_from) - done; - Printf.fprintf channel "-1 %s " (pb_var i_to t_to); - output_string channel ">= 0\n" - - and gen_dual_latency_constraint i_to i_from latency t_from = - Printf.fprintf channel "\\ t[%d] - t[%d] >= %d when t[%d]=%d\n" - i_to i_from latency i_to t_from; - Printf.fprintf channel "d_%d_%d_%d_%d: " - i_to i_from latency t_from; - for t_to=int_max earliest_dates.(i_to) (t_from + latency) - to latest_dates.(i_to) - do - Printf.fprintf channel "+1 %s " (pb_var i_to t_to) - done; - Printf.fprintf channel "-1 %s " (pb_var i_from t_from); - Printf.fprintf channel ">= 0\n" - - and gen_delta_constraint i_from i_to latency = - if delta_encoding - then Printf.fprintf channel "l_%d_%d_%d: +1 t%d -1 t%d >= %d\n" - i_from i_to latency i_to i_from latency - - in - - Printf.fprintf channel "\\ nr_instructions=%d deadline=%d\n" nr_instructions deadline; - begin - match pb_type with - | SATISFIABILITY -> output_string channel "Minimize dummy: 0\n" - | OPTIMIZATION -> - Printf.fprintf channel "Minimize\nmakespan: t%d\n" nr_instructions - end; - output_string channel "Subject To\n"; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - let early = earliest_dates.(i) and late= latest_dates.(i) in - Printf.fprintf channel "\\ t[%d] in %d..%d\ntimes%d: " i early late i; - for t=early to late - do - Printf.fprintf channel "+1 %s " (pb_var i t) - done; - Printf.fprintf channel "= 1\n" - done; - - for t=0 to deadline-1 - do - for j=0 to nr_resources-1 - do - let bound = problem.resource_bounds.(j) - and coeffs = ref [] in - for i=0 to nr_instructions-1 - do - let usage = problem.instruction_usages.(i).(j) in - if t >= earliest_dates.(i) && t <= latest_dates.(i) - && usage > 0 - then coeffs := (i, usage) :: !coeffs - done; - if !coeffs <> [] then - begin - Printf.fprintf channel "\\ resource #%d at t=%d <= %d\nr%d_%d: " j t bound j t; - List.iter (fun (i, usage) -> - Printf.fprintf channel "%+d %s " (-usage) (pb_var i t)) !coeffs; - Printf.fprintf channel ">= %d\n" (-bound) - end - done - done; - - List.iter - (fun ctr -> - if ctr.instr_to < nr_instructions then - begin - gen_delta_constraint ctr.instr_from ctr.instr_to ctr.latency; - begin - if direct_encoding - then - for t_to=earliest_dates.(ctr.instr_to) to latest_dates.(ctr.instr_to) - do - gen_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_to - done - end; - begin - if reverse_encoding - then - for t_from=earliest_dates.(ctr.instr_from) to latest_dates.(ctr.instr_from) - do - gen_dual_latency_constraint ctr.instr_to ctr.instr_from ctr.latency t_from - done - end - end - ) problem.latency_constraints; - - begin - match pb_type with - | SATISFIABILITY -> () - | OPTIMIZATION -> - let final_latencies = Array.make nr_instructions 1 in - List.iter (fun (i, latency) -> - final_latencies.(i) <- int_max final_latencies.(i) latency) - predecessors.(nr_instructions); - for i_from = 0 to nr_instructions -1 - do - gen_delta_constraint i_from nr_instructions final_latencies.(i_from) - done; - for t_to=earliest_dates.(nr_instructions) to deadline - do - for i_from = 0 to nr_instructions -1 - do - gen_latency_constraint nr_instructions i_from final_latencies.(i_from) t_to - done - done - end; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - Printf.fprintf channel "ct%d : -1 t%d" i i; - let early = earliest_dates.(i) and late= latest_dates.(i) in - for t=early to late do - Printf.fprintf channel " +%d %s" t (pb_var i t) - done; - output_string channel " = 0\n" - done; - output_string channel "Bounds\n"; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - let early = earliest_dates.(i) and late= latest_dates.(i) in - begin - Printf.fprintf channel "%d <= t%d <= %d\n" early i late; - if true then - for t=early to late do - Printf.fprintf channel "0 <= %s <= 1\n" (pb_var i t) - done - end - done; - output_string channel "Integer\n"; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - Printf.fprintf channel "t%d " i - done; - output_string channel "\nBinary\n"; - for i=0 to (match pb_type with - | OPTIMIZATION -> nr_instructions - | SATISFIABILITY -> nr_instructions-1) - do - let early = earliest_dates.(i) and late= latest_dates.(i) in - for t=early to late do - output_string channel (pb_var i t); - output_string channel " " - done; - output_string channel "\n" - done; - output_string channel "End\n"; - { - mapper_pb_type = pb_type; - mapper_nr_instructions = nr_instructions; - mapper_nr_pb_variables = 0; - mapper_earliest_dates = earliest_dates; - mapper_latest_dates = latest_dates; - mapper_var_offsets = [| |]; - mapper_final_predecessors = predecessors.(nr_instructions) - };; - -(* Guess what? Cplex sometimes outputs 11.000000004 instead of integer 11 *) - -let positive_float_round x = truncate (x +. 0.5) - -let float_round (x : float) : int = - if x > 0.0 - then positive_float_round x - else - (positive_float_round (-. x)) - -let rounded_int_of_string x = float_round (float_of_string x) - -let ilp_read_solution mapper channel = - let times = Array.make - (match mapper.mapper_pb_type with - | OPTIMIZATION -> 1+mapper.mapper_nr_instructions - | SATISFIABILITY -> mapper.mapper_nr_instructions) (-1) in - try - while true do - let line = input_line channel in - ( if (String.length line) < 3 - then failwith (Printf.sprintf "bad ilp output: length(line) < 3: %s" line)); - match String.get line 0 with - | 'x' -> () - | 't' -> let space = - try String.index line ' ' - with Not_found -> - failwith "bad ilp output: no t variable number" - in - let tnumber = - try int_of_string (String.sub line 1 (space-1)) - with Failure _ -> - failwith "bad ilp output: not a variable number" - in - (if tnumber < 0 || tnumber >= (Array.length times) - then failwith (Printf.sprintf "bad ilp output: not a correct variable number: %d (%d)" tnumber (Array.length times))); - let value = - let s = String.sub line (space+1) ((String.length line)-space-1) in - try rounded_int_of_string s - with Failure _ -> - failwith (Printf.sprintf "bad ilp output: not a time number (%s)" s) - in - (if value < 0 - then failwith "bad ilp output: negative time"); - times.(tnumber) <- value - | '#' -> () - | '0' -> () - | _ -> failwith (Printf.sprintf "bad ilp output: bad variable initial, line = %s" line) - done; - assert false - with End_of_file -> - Array.iteri (fun i x -> - if i<(Array.length times)-1 - && x<0 then raise Unschedulable) times; - times;; - -let ilp_solver = ref "ilp_solver" - -let problem_nr = ref 0 - -let ilp_scheduler pb_type problem = - try - let filename_in = Printf.sprintf "problem%05d.lp" !problem_nr - and filename_out = Printf.sprintf "problem%05d.sol" !problem_nr in - incr problem_nr; - let mapper = with_out_channel (open_out filename_in) - (fun opb_problem -> ilp_print_problem opb_problem problem pb_type) in - - begin - match Unix.system (!ilp_solver ^ " " ^ filename_in ^ " " ^ filename_out) with - | Unix.WEXITED 0 -> - Some (with_in_channel - (open_in filename_out) - (fun opb_solution -> - adjust_check_solution mapper - (ilp_read_solution mapper opb_solution))) - | Unix.WEXITED _ -> failwith "failed to start ilp solver" - | _ -> None - end - with - | Unschedulable -> None;; - -let current_utime_all () = - let t = Unix.times() in - t.Unix.tms_cutime +. t.Unix.tms_utime;; - -let utime_all_fn fn arg = - let utime_start = current_utime_all () in - let output = fn arg in - let utime_end = current_utime_all () in - (output, utime_end -. utime_start);; - -let cascaded_scheduler (problem : problem) = - let (some_initial_solution, list_scheduler_time) = - utime_all_fn (validated_scheduler list_scheduler) problem in - match some_initial_solution with - | None -> None - | Some initial_solution -> - let (solution, reoptimizing_time) = utime_all_fn (reoptimizing_scheduler (validated_scheduler (ilp_scheduler SATISFIABILITY)) initial_solution) problem in - begin - let latency2 = get_max_latency solution - and latency1 = get_max_latency initial_solution in - Printf.printf "postpass %s: %d, %d, %d, %g, %g\n" - (if latency2 < latency1 then "REOPTIMIZED" else "unchanged") - (get_nr_instructions problem) - latency1 latency2 - list_scheduler_time reoptimizing_time; - flush stdout - end; - Some solution;; - -let scheduler_by_name name = - match name with - | "ilp" -> validated_scheduler cascaded_scheduler - | "list" -> validated_scheduler list_scheduler - | "revlist" -> validated_scheduler reverse_list_scheduler - | "greedy" -> greedy_scheduler - | s -> failwith ("unknown scheduler: " ^ s);; |