src/Pure/Concurrent/task_queue.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62819 d3ff367a16a0
child 62891 7a11ea5c9626
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      Pure/Concurrent/task_queue.ML
     2     Author:     Makarius
     3 
     4 Ordered queue of grouped tasks.
     5 *)
     6 
     7 signature TASK_QUEUE =
     8 sig
     9   type group
    10   val new_group: group option -> group
    11   val group_id: group -> int
    12   val eq_group: group * group -> bool
    13   val cancel_group: group -> exn -> unit
    14   val is_canceled: group -> bool
    15   val group_status: group -> exn list
    16   val str_of_group: group -> string
    17   val str_of_groups: group -> string
    18   val urgent_pri: int
    19   type task
    20   val dummy_task: task
    21   val group_of_task: task -> group
    22   val name_of_task: task -> string
    23   val pri_of_task: task -> int
    24   val str_of_task: task -> string
    25   val str_of_task_groups: task -> string
    26   val task_statistics: task -> Properties.T
    27   val running: task -> (unit -> 'a) -> 'a
    28   val joining: task -> (unit -> 'a) -> 'a
    29   val waiting: task -> task list -> (unit -> 'a) -> 'a
    30   type queue
    31   val empty: queue
    32   val group_tasks: queue -> group -> task list
    33   val known_task: queue -> task -> bool
    34   val all_passive: queue -> bool
    35   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
    36   val cancel: queue -> group -> Thread.thread list
    37   val cancel_all: queue -> group list * Thread.thread list
    38   val finish: task -> queue -> bool * queue
    39   val enroll: Thread.thread -> string -> group -> queue -> task * queue
    40   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    41   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    42   val extend: task -> (bool -> bool) -> queue -> queue option
    43   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
    44   val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
    45   val dequeue_deps: Thread.thread -> task list -> queue ->
    46     (((task * (bool -> bool) list) option * task list) * queue)
    47 end;
    48 
    49 structure Task_Queue: TASK_QUEUE =
    50 struct
    51 
    52 val new_id = Counter.make ();
    53 
    54 
    55 (** nested groups of tasks **)
    56 
    57 (* groups *)
    58 
    59 abstype group = Group of
    60  {parent: group option,
    61   id: int,
    62   status: exn option Synchronized.var}
    63 with
    64 
    65 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
    66 
    67 fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
    68 
    69 fun group_id (Group {id, ...}) = id;
    70 fun eq_group (group1, group2) = group_id group1 = group_id group2;
    71 
    72 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
    73   | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a);
    74 
    75 
    76 (* group status *)
    77 
    78 fun cancel_group (Group {status, ...}) exn =
    79   Synchronized.change status
    80     (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
    81 
    82 fun is_canceled (Group {parent, status, ...}) =
    83   is_some (Synchronized.value status) orelse
    84     (case parent of NONE => false | SOME group => is_canceled group);
    85 
    86 fun group_status (Group {parent, status, ...}) =
    87   the_list (Synchronized.value status) @
    88     (case parent of NONE => [] | SOME group => group_status group);
    89 
    90 fun str_of_group group =
    91   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
    92 
    93 fun str_of_groups group =
    94   space_implode "/" (map str_of_group (rev (fold_groups cons group [])));
    95 
    96 end;
    97 
    98 
    99 (* tasks *)
   100 
   101 val urgent_pri = 1000;
   102 
   103 type timing = Time.time * Time.time * string list;  (*run, wait, wait dependencies*)
   104 
   105 val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
   106 
   107 fun new_timing () =
   108   if ! Multithreading.trace < 2 then NONE
   109   else SOME (Synchronized.var "timing" timing_start);
   110 
   111 abstype task = Task of
   112  {group: group,
   113   name: string,
   114   id: int,
   115   pri: int option,
   116   timing: timing Synchronized.var option,
   117   pos: Position.T}
   118 with
   119 
   120 val dummy_task =
   121   Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
   122     pos = Position.none};
   123 
   124 fun new_task group name pri =
   125   Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
   126     pos = Position.thread_data ()};
   127 
   128 fun group_of_task (Task {group, ...}) = group;
   129 fun name_of_task (Task {name, ...}) = name;
   130 fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
   131 
   132 fun str_of_task (Task {name, id, ...}) =
   133   if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
   134 
   135 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
   136 
   137 fun update_timing update (Task {timing, ...}) e =
   138   uninterruptible (fn restore_attributes => fn () =>
   139     let
   140       val start = Time.now ();
   141       val result = Exn.capture (restore_attributes e) ();
   142       val t = Time.now () - start;
   143       val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
   144     in Exn.release result end) ();
   145 
   146 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   147   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
   148 
   149 fun task_statistics (Task {name, id, timing, pos, ...}) =
   150   let
   151     val (run, wait, wait_deps) =
   152       (case timing of NONE => timing_start | SOME var => Synchronized.value var);
   153     fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   154   in
   155     [("now", Markup.print_real (Time.toReal (Time.now ()))),
   156      ("task_name", name), ("task_id", Markup.print_int id),
   157      ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
   158     Position.properties_of pos
   159   end;
   160 
   161 end;
   162 
   163 structure Tasks = Table(type key = task val ord = task_ord);
   164 structure Task_Graph = Graph(type key = task val ord = task_ord);
   165 
   166 
   167 (* timing *)
   168 
   169 fun running task =
   170   update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
   171 
   172 fun joining task =
   173   update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
   174 
   175 fun waiting task deps =
   176   update_timing (fn t => fn (a, b, ds) =>
   177     (a - t, b + t,
   178       if ! Multithreading.trace > 0
   179       then fold (insert (op =) o name_of_task) deps ds else ds)) task;
   180 
   181 
   182 
   183 (** queue of jobs and groups **)
   184 
   185 (* known group members *)
   186 
   187 type groups = unit Tasks.table Inttab.table;
   188 
   189 fun get_tasks (groups: groups) gid =
   190   the_default Tasks.empty (Inttab.lookup groups gid);
   191 
   192 fun add_task (gid, task) groups =
   193   Inttab.update (gid, Tasks.update (task, ()) (get_tasks groups gid)) groups;
   194 
   195 fun del_task (gid, task) groups =
   196   let val tasks = Tasks.delete_safe task (get_tasks groups gid) in
   197     if Tasks.is_empty tasks then Inttab.delete_safe gid groups
   198     else Inttab.update (gid, tasks) groups
   199   end;
   200 
   201 
   202 (* job dependency graph *)
   203 
   204 datatype job =
   205   Job of (bool -> bool) list |
   206   Running of Thread.thread |
   207   Passive of unit -> bool;
   208 
   209 type jobs = job Task_Graph.T;
   210 
   211 fun get_job (jobs: jobs) task = Task_Graph.get_node jobs task;
   212 fun set_job task job (jobs: jobs) = Task_Graph.map_node task (K job) jobs;
   213 
   214 fun add_job task dep (jobs: jobs) =
   215   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
   216 
   217 
   218 (* queue *)
   219 
   220 datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int};
   221 
   222 fun make_queue groups jobs urgent = Queue {groups = groups, jobs = jobs, urgent = urgent};
   223 val empty = make_queue Inttab.empty Task_Graph.empty 0;
   224 
   225 fun group_tasks (Queue {groups, ...}) group = Tasks.keys (get_tasks groups (group_id group));
   226 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
   227 
   228 
   229 (* job status *)
   230 
   231 fun ready_job (task, (Job list, (deps, _))) =
   232       if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE
   233   | ready_job (task, (Passive abort, (deps, _))) =
   234       if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task)
   235       then SOME (task, [fn _ => abort ()])
   236       else NONE
   237   | ready_job _ = NONE;
   238 
   239 fun ready_job_urgent false = ready_job
   240   | ready_job_urgent true = (fn entry as (task, _) =>
   241       if pri_of_task task >= urgent_pri then ready_job entry else NONE);
   242 
   243 fun active_job (task, (Running _, _)) = SOME (task, [])
   244   | active_job arg = ready_job arg;
   245 
   246 fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs);
   247 
   248 
   249 (* queue status *)
   250 
   251 fun status (Queue {jobs, urgent, ...}) =
   252   let
   253     val (x, y, z, w) =
   254       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
   255           (case job of
   256             Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w)
   257           | Running _ => (x, y, z + 1, w)
   258           | Passive _ => (x, y, z, w + 1)))
   259         jobs (0, 0, 0, 0);
   260   in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
   261 
   262 
   263 
   264 (** task queue operations **)
   265 
   266 (* cancel -- peers and sub-groups *)
   267 
   268 fun cancel (Queue {groups, jobs, ...}) group =
   269   let
   270     val _ = cancel_group group Exn.Interrupt;
   271     val running =
   272       Tasks.fold (fn (task, _) =>
   273           (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
   274         (get_tasks groups (group_id group)) [];
   275   in running end;
   276 
   277 fun cancel_all (Queue {jobs, ...}) =
   278   let
   279     fun cancel_job (task, (job, _)) (groups, running) =
   280       let
   281         val group = group_of_task task;
   282         val _ = cancel_group group Exn.Interrupt;
   283       in
   284         (case job of
   285           Running t => (insert eq_group group groups, insert Thread.equal t running)
   286         | _ => (groups, running))
   287       end;
   288     val running = Task_Graph.fold cancel_job jobs ([], []);
   289   in running end;
   290 
   291 
   292 (* finish *)
   293 
   294 fun finish task (Queue {groups, jobs, urgent}) =
   295   let
   296     val group = group_of_task task;
   297     val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
   298     val jobs' = Task_Graph.del_node task jobs;
   299     val maximal = Task_Graph.is_maximal jobs task;
   300   in (maximal, make_queue groups' jobs' urgent) end;
   301 
   302 
   303 (* enroll *)
   304 
   305 fun enroll thread name group (Queue {groups, jobs, urgent}) =
   306   let
   307     val task = new_task group name NONE;
   308     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   309     val jobs' = jobs |> Task_Graph.new_node (task, Running thread);
   310   in (task, make_queue groups' jobs' urgent) end;
   311 
   312 
   313 (* enqueue *)
   314 
   315 fun enqueue_passive group abort (Queue {groups, jobs, urgent}) =
   316   let
   317     val task = new_task group "passive" NONE;
   318     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   319     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
   320   in (task, make_queue groups' jobs' urgent) end;
   321 
   322 fun enqueue name group deps pri job (Queue {groups, jobs, urgent}) =
   323   let
   324     val task = new_task group name (SOME pri);
   325     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
   326     val jobs' = jobs
   327       |> Task_Graph.new_node (task, Job [job])
   328       |> fold (add_job task) deps;
   329     val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
   330   in (task, make_queue groups' jobs' urgent') end;
   331 
   332 fun extend task job (Queue {groups, jobs, urgent}) =
   333   (case try (get_job jobs) task of
   334     SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent)
   335   | _ => NONE);
   336 
   337 
   338 (* dequeue *)
   339 
   340 fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent}) =
   341   (case try (get_job jobs) task of
   342     SOME (Passive _) =>
   343       let val jobs' = set_job task (Running thread) jobs
   344       in (SOME true, make_queue groups jobs' urgent) end
   345   | SOME _ => (SOME false, queue)
   346   | NONE => (NONE, queue));
   347 
   348 fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent}) =
   349   if not urgent_only orelse urgent > 0 then
   350     (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of
   351       SOME (result as (task, _)) =>
   352         let
   353           val jobs' = set_job task (Running thread) jobs;
   354           val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
   355         in (SOME result, make_queue groups jobs' urgent') end
   356     | NONE => (NONE, queue))
   357   else (NONE, queue);
   358 
   359 
   360 (* dequeue wrt. dynamic dependencies *)
   361 
   362 fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent}) =
   363   let
   364     fun ready [] rest = (NONE, rev rest)
   365       | ready (task :: tasks) rest =
   366           (case try (Task_Graph.get_entry jobs) task of
   367             NONE => ready tasks rest
   368           | SOME (_, entry) =>
   369               (case ready_job (task, entry) of
   370                 NONE => ready tasks (task :: rest)
   371               | some => (some, fold cons rest tasks)));
   372 
   373     fun ready_dep _ [] = NONE
   374       | ready_dep seen (task :: tasks) =
   375           if Tasks.defined seen task then ready_dep seen tasks
   376           else
   377             let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
   378               (case ready_job (task, entry) of
   379                 NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
   380               | some => some)
   381             end;
   382 
   383     fun result (res as (task, _)) deps' =
   384       let
   385         val jobs' = set_job task (Running thread) jobs;
   386         val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
   387       in ((SOME res, deps'), make_queue groups jobs' urgent') end;
   388   in
   389     (case ready deps [] of
   390       (SOME res, deps') => result res deps'
   391     | (NONE, deps') =>
   392         (case ready_dep Tasks.empty deps' of
   393           SOME res => result res deps'
   394         | NONE => ((NONE, deps'), queue)))
   395   end;
   396 
   397 
   398 (* toplevel pretty printing *)
   399 
   400 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
   401 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
   402 
   403 end;