schedule: misc cleanup, more precise task model;
authorwenzelm
Thu Aug 09 23:53:51 2007 +0200 (2007-08-09)
changeset 242098a2c8d623e43
parent 24208 f4cafbaa05e4
child 24210 a865059c4fcb
schedule: misc cleanup, more precise task model;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Aug 09 23:53:50 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Aug 09 23:53:51 2007 +0200
     1.3 @@ -325,6 +325,55 @@
     1.4    end;
     1.5  
     1.6  
     1.7 +(* scheduling loader tasks *)
     1.8 +
     1.9 +datatype task = Task of (unit -> unit) | Finished | Running;
    1.10 +fun task_finished Finished = true | task_finished _ = false;
    1.11 +
    1.12 +local
    1.13 +
    1.14 +fun max_task (name, (Task body, m)) NONE = SOME (name, (body, m))
    1.15 +  | max_task (name, (Task body, m)) (task' as SOME (_, (_, m'))) =
    1.16 +      if m > m' then SOME (name, (body, m)) else task'
    1.17 +  | max_task _ task' = task';
    1.18 +
    1.19 +fun next_task G =
    1.20 +  let
    1.21 +    val tasks = Graph.minimals G |> map (fn name =>
    1.22 +      (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
    1.23 +    val finished = filter (task_finished o fst o snd) tasks;
    1.24 +  in
    1.25 +    if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
    1.26 +    else if null tasks then (Multithreading.Terminate, G)
    1.27 +    else
    1.28 +      (case fold max_task tasks NONE of
    1.29 +        NONE => (Multithreading.Wait, G)
    1.30 +      | SOME (name, (body, _)) =>
    1.31 +         (Multithreading.Task {body = body, cont = Graph.del_nodes [name], fail = K Graph.empty},
    1.32 +          Graph.map_node name (K Running) G))
    1.33 +  end;
    1.34 +
    1.35 +fun schedule_seq tasks =
    1.36 +  Graph.topological_order tasks
    1.37 +  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
    1.38 +
    1.39 +in
    1.40 +
    1.41 +fun schedule_tasks tasks n =
    1.42 +  let val m = ! Multithreading.max_threads in
    1.43 +    if m <= 1 orelse n <= 1 then schedule_seq tasks
    1.44 +    else if Multithreading.self_critical () then
    1.45 +     (warning (loader_msg "no multithreading within critical section" []);
    1.46 +      schedule_seq tasks)
    1.47 +    else
    1.48 +      (case Multithreading.schedule (Int.min (m, n)) next_task tasks of
    1.49 +        [] => ()
    1.50 +      | exns => raise Exn.EXCEPTIONS (exns, ""))
    1.51 +  end;
    1.52 +
    1.53 +end;
    1.54 +
    1.55 +
    1.56  (* require_thy -- checking database entries wrt. the file-system *)
    1.57  
    1.58  local
    1.59 @@ -374,7 +423,7 @@
    1.60      val _ = member (op =) initiators name andalso error (cycle_msg initiators);
    1.61    in
    1.62      (case try (Graph.get_node (fst tasks)) name of
    1.63 -      SOME task => (Task.is_finished task, tasks)
    1.64 +      SOME task => (task_finished task, tasks)
    1.65      | NONE =>
    1.66          let
    1.67            val (current, deps, parents) = check_deps dir' name
    1.68 @@ -394,8 +443,8 @@
    1.69  
    1.70            val upd_time = serial ();
    1.71            val tasks_graph'' = tasks_graph' |> new_deps name parent_names
    1.72 -           (if all_current then Task.Finished
    1.73 -            else Task.Task (fn () => load_thy time upd_time initiators dir' name));
    1.74 +           (if all_current then Finished
    1.75 +            else Task (fn () => load_thy time upd_time initiators dir' name));
    1.76            val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
    1.77          in (all_current, (tasks_graph'', tasks_len'')) end)
    1.78    end;
    1.79 @@ -403,49 +452,13 @@
    1.80  end;
    1.81  
    1.82  
    1.83 -(* variations on use_thy -- scheduling required theories *)
    1.84 +(* use_thy etc. *)
    1.85  
    1.86  local
    1.87  
    1.88 -fun schedule_seq tasks =
    1.89 -  Graph.topological_order tasks
    1.90 -  |> List.app (fn name => (case Graph.get_node tasks name of Task.Task f => f () | _ => ()));
    1.91 -
    1.92 -fun max_task (task as (_, (Task.Task _, _: int))) NONE = SOME task
    1.93 -  | max_task (task as (_, (Task.Task _, m))) (task' as SOME (_, (_, m'))) =
    1.94 -      if m > m' then SOME task else task'
    1.95 -  | max_task _ task' = task';
    1.96 -
    1.97 -fun next_task G =
    1.98 -  let
    1.99 -    val tasks = Graph.minimals G |> map (fn name =>
   1.100 -      (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
   1.101 -    val finished = filter (Task.is_finished o fst o snd) tasks;
   1.102 -  in
   1.103 -    if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
   1.104 -    else if null tasks then ((Task.Finished, I), G)
   1.105 -    else
   1.106 -      (case fold max_task tasks NONE of
   1.107 -        NONE => ((Task.Running, I), G)
   1.108 -      | SOME (name, (task, _)) =>
   1.109 -          ((task, Graph.del_nodes [name]), Graph.map_node name (K Task.Running) G))
   1.110 -  end;
   1.111 -
   1.112 -fun schedule_tasks (tasks, n) =
   1.113 -  let val m = ! Multithreading.max_threads in
   1.114 -    if m <= 1 orelse n <= 1 then schedule_seq tasks
   1.115 -    else if Multithreading.self_critical () then
   1.116 -     (warning (loader_msg "no multithreading within critical section" []);
   1.117 -      schedule_seq tasks)
   1.118 -    else
   1.119 -      (case Multithreading.schedule (Int.min (m, n)) next_task tasks of
   1.120 -        [] => ()
   1.121 -      | exns => raise Exn.EXCEPTIONS (exns, ""))
   1.122 -  end;
   1.123 -
   1.124  fun gen_use_thy' req dir arg =
   1.125 -  let val (_, tasks) = req [] dir arg (Graph.empty, 0)
   1.126 -  in schedule_tasks tasks end;
   1.127 +  let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0)
   1.128 +  in schedule_tasks tasks n end;
   1.129  
   1.130  fun gen_use_thy req str =
   1.131    let val name = base_name str in
   1.132 @@ -458,7 +471,6 @@
   1.133  
   1.134  val use_thys_dir = gen_use_thy' (require_thys false);
   1.135  val use_thys = use_thys_dir Path.current;
   1.136 -
   1.137  val use_thy = gen_use_thy (require_thy false);
   1.138  val time_use_thy = gen_use_thy (require_thy true);
   1.139