src/Pure/Concurrent/task_queue.ML
author wenzelm
Mon, 08 Sep 2008 16:08:18 +0200
changeset 28165 26bb048f463c
child 28168 ba410235ff04
permissions -rw-r--r--
Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28165
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/task_queue.ML
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     4
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     5
Ordered queue of grouped tasks.
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     6
*)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     7
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     8
signature TASK_QUEUE =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
     9
sig
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    10
  eqtype task
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    11
  val get_thread_data: unit -> task option
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    12
  val set_thread_data: task option -> unit
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    13
  eqtype group
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    14
  val new_group: unit -> group
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    15
  type queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    16
  val empty: queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    17
  val dequeue: Thread.thread -> queue -> (task * (unit -> unit)) option * queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    18
  val enqueue: group option -> task list -> (unit -> unit) -> queue -> task * queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    19
  val finished: task -> queue -> queue
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    20
  val interrupt: queue -> task -> unit
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    21
  val interrupt_group: queue -> group -> unit
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    22
end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    23
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    24
structure TaskQueue: TASK_QUEUE =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    25
struct
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    26
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    27
(* identified tasks *)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    28
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    29
datatype task = Task of serial;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    30
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    31
local val tag = Universal.tag () : task option Universal.tag in
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    32
  fun get_thread_data () = the_default NONE (Thread.getLocal tag);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    33
  fun set_thread_data x = Thread.setLocal (tag, x);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    34
end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    35
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    36
datatype group = Group of serial;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    37
fun new_group () = Group (serial ());
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    38
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    39
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    40
(* queue of dependent jobs *)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    41
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    42
datatype job =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    43
  Job of unit -> unit |
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    44
  Running of Thread.thread;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    45
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    46
datatype queue = Queue of
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    47
  {jobs: (job * group option) IntGraph.T,             (*job dependency graph*)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    48
   cache: (task * (unit -> unit)) Queue.T option,     (*cache of ready tasks*)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    49
   groups: task list Inttab.table};                   (*active group members*)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    50
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    51
fun make_queue jobs cache groups =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    52
  Queue {jobs = jobs, cache = cache, groups = groups};
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    53
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    54
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    55
(* queue operations *)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    56
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    57
val empty = make_queue IntGraph.empty NONE Inttab.empty;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    58
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    59
fun enqueue group deps job (Queue {jobs, groups, ...}) =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    60
  let
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    61
    val id = serial ();
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    62
    val task = Task id;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    63
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    64
    fun add_dep (Task dep) G = IntGraph.add_edge_acyclic (dep, id) G
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    65
      handle IntGraph.UNDEF _ => G;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    66
    val jobs' = jobs |> IntGraph.new_node (id, (Job job, group)) |> fold add_dep deps;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    67
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    68
    val groups' =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    69
      (case group of
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    70
        NONE => groups
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    71
      | SOME (Group gid) => Inttab.cons_list (gid, task) groups);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    72
  in (task, make_queue jobs' NONE groups') end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    73
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    74
fun dequeue thread (queue as Queue {jobs, cache, groups}) =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    75
  let
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    76
    val ready =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    77
      (case cache of
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    78
        SOME ready => ready
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    79
      | NONE =>
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    80
          let val add = fn (id, ((Job job, _), ([], _))) => Queue.enqueue (Task id, job) | _ => I
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    81
          in IntGraph.fold add jobs Queue.empty end);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    82
  in
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    83
    if Queue.is_empty ready then (NONE, make_queue jobs (SOME ready) groups)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    84
    else
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    85
      let
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    86
        val (task as (Task id, _), ready') = Queue.dequeue ready;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    87
        val jobs' = IntGraph.map_node id (fn (_, group) => (Running thread, group)) jobs;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    88
      in (SOME task, make_queue jobs' (SOME ready') groups) end
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    89
  end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    90
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    91
fun finished (task as Task id) (Queue {jobs, groups, ...}) =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    92
  let
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    93
    val groups' =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    94
      (case #2 (IntGraph.get_node jobs id) of
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    95
        NONE => groups
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    96
      | SOME (Group gid) => Inttab.remove_list (op =) (gid, task) groups);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    97
    val jobs' = IntGraph.del_nodes [id] jobs;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    98
  in make_queue jobs' NONE groups' end;
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
    99
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   100
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   101
(* interrupts *)
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   102
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   103
fun interrupt (Queue {jobs, ...}) (Task id) =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   104
  (case IntGraph.get_node jobs id of
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   105
    (Running thread, _) => (Thread.interrupt thread handle Thread _ => ())
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   106
  | _ => ())
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   107
  handle IntGraph.UNDEF _ => ();
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   108
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   109
fun interrupt_group (queue as Queue {groups, ...}) (Group gid) =
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   110
  List.app (interrupt queue) (Inttab.lookup_list groups gid);
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   111
26bb048f463c Ordered queue of grouped tasks.
wenzelm
parents:
diff changeset
   112
end;